ACL2 Seminar, April 30, 2013

         Formal Specification of the X86 ISA
      (and Using it to Verify X86 Binary Programs)

Nathalie Beavers, Soumava Ghosh, Shilpi Goel, Marijn J. H. Heule,
Warren A. Hunt, Jr., Matt Kaufmann, J Strother Moore, Nathan Wetzler

Speaker: Warren Hunt

Abstract:

Analysis of binary programs is necessary to check that distributed X86
programs (e.g., Windows, MacOS, Linux) indeed perform the work
desired.  We approach this problem by formalizing a subset of the X86
instruction-set architecture (ISA) using the ACL2 theorem-proving
system.  We have specified the integer portion of the X86 ISA as an
executable simulator.  We are validating this simulator by comparing
its results with physical X86 processors.  We are able to symbolically
execute X86 programs, and we use this capability, along with other
ACL2 mechanisms, to investigate the correctness of X86 binary
programs.  We will present example verifications of X86 programs using
our ACL2 symbolic-simulation framework.  We are integrating SAT
techniques into ACL2 to help strengthen our system for performing
X86-binary-code verifications.