{"id":{"repo_id":"nps","oai_identifier":"oai:calhoun.nps.edu:10945/7360"},"canonical_url":"https://search.dev.ndltd.org/etd/nps/oai:calhoun.nps.edu:10945/7360","repository":{"repo_id":"nps","name":"Naval Postgraduate School","base_url":"https://calhoun.nps.edu/server/oai/request"},"display":{"title":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Hom, Michael"],"institution":"Monterey, CA; Naval Postgraduate School","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Computer Science (CS)","school":null,"contributors":[],"advisors":["Eagle, Chris S."],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012-06","date_published":"2012-06","updated_at":"2026-07-27T20:26:50Z","subjects":[],"languages":[],"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."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/10945/7360","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Eagle, Chris S."]},{"key":"dc:contributor.department","label":"Department","values":["Computer Science (CS)"]},{"key":"dc:creator","label":"Author","values":["Hom, Michael"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2012-07-30T23:15:56Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2012-07-30T23:15:56Z"]},{"key":"dc:date.issued","label":"Date","values":["2012-06"]},{"key":"dc:publisher","label":"Institution","values":["Monterey, CA; Naval Postgraduate School"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["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."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/10945/7360"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Symbolic Execution Over Native X86"]}]}],"canonical_facts":{"dc:contributor.advisor":["Eagle, Chris S."],"dc:contributor.department":["Computer Science (CS)"],"dc:creator":["Hom, Michael"],"dc:date.accessioned":["2012-07-30T23:15:56Z"],"dc:date.available":["2012-07-30T23:15:56Z"],"dc:date.issued":["2012-06"],"dc:description.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."],"dc:identifier.uri":["https://hdl.handle.net/10945/7360"],"dc:publisher":["Monterey, CA; Naval Postgraduate School"],"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."],"dc:title":["Symbolic Execution Over Native X86"],"dc:type":["Thesis"]},"updated_at":"2026-07-27T20:26:50Z"}