Towards a Formalization of the X86 Instruction Set Architecture
University of Texas at Austin Austin United States
Pagination or Media Count:
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 correct-ness 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 dene security policies. we discuss the use of our approach in developing trusted applications.
- Computer Systems