Formal Verification of Memory Preservation of x86-64 Binaries

Formal verification of a binary can provide high software assurance, even when the source code is unavailable. It is, however, inherently hard due to the low level of abstraction involved; instead of verifying typed and structured source code, one has to verify machine code or reconstructed assembly. This paper presents a semi-automated methodology for formally verifying memory preservation, as well as register preservation, over disassembled binaries. The methodology is based on formal symbolic execution and Floyd-style verification. We show that the methodology is compositional on the function level, which is crucial for scalability. The methodology works for loops, recursion, and both optimized and non-optimized code. It can be used to expose preconditions required for non-exceptional behavior. We demonstrate applicability by verifying a set of functions from the HermitCore unikernel library.