Automated synthesis of symbolic instruction encodings from i/o samples

Symbolic execution is a key component of precise binary program analysis tools. We discuss how to automatically boot-strap the con-struction of a symbolic execution engine for a processor instruction set such as x86, x64 or ARM. We show how to automatically syn-thesize symbolic representations of individual processor instruc-tions from input/output examples and express them as bit-vector constraints. We present and compare various synthesis algorithms and instruction sampling strategies. We introduce a new synthesis algorithm based on smart sampling which we show is one to two orders of magnitude faster than previous synthesis algorithms in our context. With this new algorithm, we can automatically synthe-size bit-vector circuits for over 500 x86 instructions (8/16/32-bits, outputs, EFLAGS) using only 6 synthesis templates and in less than two hours using the Z3 SMT solver on a regular machine. During this work, we also discovered several inconsistencies across x86 processors, errors in the x86 Intel spec, and several bugs in previ-ous manually-written x86 instruction handlers. 1