Symbolic Execution Over Native x86

Abstract

Current approaches to program analysis largely rely on the use of an intermediate language to derive intermediate representations of source code or binaries under evaluation. This can simplify semantics when dealing with a complex instruction set such as the Intel Industry Standard Architecture (ISA) instruction set. However, a question that remains is whether these intermediate languages truly retain semantic fidelity or whether elements of the ISA instruction set get lost in translation. This thesis describes a framework that is being developed at NPS that accomplishes symbolic execution without the use of an intermediate language and symbolically executes ELF and WinPE binary programs over the native x86 ISA instruction set, and specifically discusses an approach to describing state mathematically using a formal algebra.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2012
Accession Number
ADA562909

Entities

People

  • Michael Hom

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • Cyber

DTIC Thesaurus Topics

  • Algorithms
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Cybersecurity
  • Debugging
  • Governments
  • Instruction Set Architecture
  • Malware
  • Operating Systems
  • Programming Languages
  • Software Development
  • Software Testing
  • Test And Evaluation
  • United States Government
  • Word Processors

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Parallel and Distributed Computing.