Verification of X86 Binary-Level Programs

Presented as part of the 2013 HCSS conference.

ABSTRACT

Verification of binary programs is required to assure their correct execution.  However, correctness verification of binary programs often involves significant user expertise and time-consuming manual effort. We present an approach for automatically verifying some x86 binary programs using symbolic execution on a formal model of the x86 instruction set architecture.  Our approach can reduce the work involved in the proof development process by automating the verification of program fragments and sometimes even complete subroutines.