Towards a Formalization of the X86 Instruction Set Architecture
Technical Report TR-08-15, Department of Computer Sciences, University
of Texas at Austin, March 2008.
We present a preliminary approach to defining a formal specification
of the semantics of the X86 Instruction Set Architecture. The goal of
the formalization is to support the dual requirements of analyzing the
correctness of binaries executing on the architecture and
investigating different safety and security properties of the
architecture itself. In particular, we focus on the security
properties of protection rings available in the X86. A simplified
version of the specification has been developed in the formal logic of
the ACL2 theorem prover together with a generic approach to
operationally define security policies. we discuss the use of our
approach in developing trusted applications.