|
|
|---|
|
|
|
|---|
S. Goel, Formal
Verification of Application and System Programs Based on a Validated x86 ISA
Model, University of Texas at Austin, Ph.D. dissertation, 2016.
Relevance: details of the x86 model
Goel writes on page viii of the dissertation
This dissertation demonstrates that formal verification of complex program properties can be made practical, without any loss of accuracy or expressiveness, by employing a machine-code analysis framework implemented using a mechanical theorem prover. To this end, we constructed a formal and executable model of the x86 Instruction-Set Architecture using the ACL2 theorem-proving system. This model includes a specification of 400+ x86 opcodes and architectural features like segmentation and paging. The model's high execution speed allows it to be validated routinely by performing co-simulations against a physical x86 processor — thus, formal analysis based on this model is reliable. We also developed a general framework for x86 machine-code analysis that can lower the overhead associated with the verification of a broad range of program properties, including correctness with respect to behavior, security, and resource requirements. We illustrate the capabilities of our framework by describing the verification of two application programs, population count and word count, and one system program, zero copy.
Because of the concern for validating the ACL2 x86 model against x86 hardware by various manufacturers it was important the ACL2 x86 execute efficiently. When running in the application-level mode the ACL2 model executes at about 3.3 million x86 instructions per second (ips); in the system-level mode it executes at about 912,000 ips.
See the collection ACL2 books and files at