Synthesis of machine code from semantics
Abstract
In this paper, we present a technique to synthesize machine-code instructions from a semantic specification, given as a Quantifier-Free Bit-Vector (QFBV) logic formula. Our technique uses an instantiation of the Counter-Example Guided Inductive Synthesis (CEGIS) framework, in combination with search-space pruning heuristics to synthesize instruction-sequences. To counter the exponential cost inherent in enumerative synthesis, our technique uses a divide-and-conquer strategy to break the input QFBV formula into independent sub-formulas, and synthesize instructions for the sub-formulas. Synthesizers created by our technique could be used to create semantics-based binary rewriting tools such as optimizers, partial evaluators, program obfuscators/de-obfuscators, etc. Our experiments for Intel's IA-32 instruction set show that, in comparison to our baseline algorithm, our search-space pruning heuristics reduce the synthesis time by a factor of 473, and our divide-and-conquer strategy reduces the synthesis time by a further 3 to 5 orders of magnitude.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jun 03, 2015
- Source ID
- 10.1145/2813885.2737960
Entities
People
- Thomas Reps
- Venkatesh Srinivasan
Organizations
- Air Force Research Laboratory
- Defense Advanced Research Projects Agency
- National Science Foundation
- University of Wisconsin–Madison
- Wisconsin Alumni Research Foundation