Quelle  README

Submission to Archive of Formal Proofs

------------------------------------------------------------
X86 instruction semantics and basic block symbolic execution
------------------------------------------------------------

This AFP entry provides semantics for roughly 120 different X86-64 assembly instructions. These instructions include various moves, arithmetic/logical operations, jumps, call/return, SIMD extensions and others. External functions are supported by allowing a user to provide custom semantics for these calls. Floating-point operations are mapped to uninterpreted functions. The model provides semantics for register aliasing and a byte-level little-endian memory model. The semantics are purposefully incomplete, but overapproximative. For example, the precise effect of flags may be undefined for certain instructions, or instructions may simply have no semantics at all. In those cases, the semantics are mapped to universally quantified uninterpreted terms from a locale. Second, this entry provides a method to symbolic execution of basic blocks. The method, called ''se_step'' (for: symbolic execution step) fetches an instruction and updates the current symbolic state while keeping track of assumptions made over the memory model. A key component is a set of theorems that prove how reads from memory resolve after writes have occurred. Thirdly, this entry provides a parser that allows the user to copy-paste the output of the standard disassembly tool objdump into Isabelle/HOL. A couple small and explanatory examples are included, including functions from the word count program. Several examples can be supplied upon request (they are not included due to the running time of verification): functions from the floating-point modulo function from FDLIBM, the GLIBC strlen function and the CoreUtils SHA256 implementation.

-------
CONTACT
-------
Authors:     Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran
Year:        2021
Maintainer:  Freek Verbeek (freek@vt.edu)


For any questions, feedback, remarks but also for requested extensions (e.g., more instructions) do not hesitate to contact Freek Verbeek.



-----
USAGE
-----
For usage, open the file Examples.thy in the Isabelle theorem prover (Isabelle2020/HOL). More examples can be found by opening the files Example_*.thy. Specifically, the file Example_WC.thy contains explanations on how to use the objdump parser, the symbolic execution engine, how to deal with external function calls, and demonstrates how a memory model is created on the-fly, using one simple example.

For building a PDF document, run from a command-line:

isabelle build -v -D X86

from the top directory.


--------
CONTENTS
--------
./X86_Semantics               Main dir, containing the .thy files.
./X86_Semantics/document/     Files for document generation by Isabelle.
./X86_Semantics/output/       Auto-generated by Isabelle document generation.


---------------
ACKNOWLEDGMENTS
---------------
Distribution statement: Approved for public release; distribution is unlimited. This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR.00112090028, ONR under grant N00014-17-1-2297, and NAVSEA/NEEC under grant N00174-16-C-0018.