Towards a Formalization of the X86 Instruction Set Architecture

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 27, 2008
Accession Number
AD1024607

Entities

People

  • Sandip Ray

Organizations

  • University of Texas at Austin

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Computer Science
  • Computers
  • Computing System Architectures
  • Decoupling
  • Encapsulation
  • Guarantees
  • Instruction Set Architecture
  • Instructions
  • Logic
  • Reasoning
  • Resistance
  • Security
  • Simulations
  • Simulators
  • Specifications
  • Verification

Fields of Study

  • Computer science

Readers

  • Cybersecurity.
  • Mathematical Modeling and Probability Theory.
  • Software Engineering.