Specification and verification of x86 machine-level code

Warren Hunt, The University of Texas, USA

We are using theorem-proving techniques to model and analyze x86 software for the purpose of increasing the accuracy and reliability of x86-based products. We have developed an ISA-level x86 emulator in the ACL2 logic; this emulator serves as a precise specification for x86 software. Using the ACL2 theorem-proving system, we describe how our x86 ISA model is used to prove the correctness of x86 binary-level programs.