Towards a Formalization of the X86 Instruction Set Architecture

S. Ray

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.

Relevant files