Formal Verification of Memory Preservation of x86-64 Binaries

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Authors:
  • Joshua A. Bockenek
  • Freek Verbeek
  • Peter Lammich
  • Binoy Ravindran

Abstract

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.

Bibliographical metadata

Original languageEnglish
Title of host publication38th International Conference on Computer Safety, Reliability and Security
Publication statusAccepted/In press - 30 Apr 2019
Event38th International Conference on Computer Safety, Reliability and Security - Turku , Finland
Event duration: 10 Sep 201913 Sep 2019

Conference

Conference38th International Conference on Computer Safety, Reliability and Security
Abbreviated titleSAFECOMP 2019
CountryFinland
CityTurku
Period10/09/1913/09/19