Accession Number:

AD1024607

Title:

Towards a Formalization of the X86 Instruction Set Architecture

Descriptive Note:

Technical Report

Corporate Author:

University of Texas at Austin Austin United States

Personal Author(s):

Report Date:

2008-03-27

Pagination or Media Count:

10.0

Abstract:

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.

Subject Categories:

  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE