Symbolic Execution Over Native X86
Loading...
Authors
Hom, Michael
Subjects
Program Analysis
Symbolic Execution
Theorem Proving
x86
SMT
SAT
Symbolic Execution
Theorem Proving
x86
SMT
SAT
Advisors
Eagle, Chris S.
Date of Issue
2012-06
Date
12-Jun
Publisher
Monterey, California. Naval Postgraduate School
Language
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.
Type
Thesis
Description
Series/Report No
Department
Computer Science
Organization
Naval Postgraduate School