Symbolic Execution Over Native X86

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.

Department dc:contributor.department

Computer Science (CS)

Grantor dc:publisher

Monterey, CA; Naval Postgraduate School

Year dc:date.issued

2012

Author dc:creator

• Hom, Michael

Advisor dc:contributor.advisor

• Eagle, Chris S.

Statement dc:rights

• This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.

Handle dc:identifier.uri

https://hdl.handle.net/10945/7360

OAI identifier oai:identifier

oai:calhoun.nps.edu:10945/7360