Synthesis of Machine Code from Semantics
Venkatesh Srinivasan and Thomas Reps
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.
(Click here to access the paper:
PDF.)
University of Wisconsin