Loading...
Please wait, while we are loading the content...
Similar Documents
Automated synthesis of symbolic instruction encodings from i/o samples (2012)
| Content Provider | CiteSeerX |
|---|---|
| Author | Taly, Ankur Godefroid, Patrice |
| Abstract | 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. |
| File Format | |
| Publisher Date | 2012-01-01 |
| Access Restriction | Open |
| Subject Keyword | Bit-vector Circuit Compare Various Synthesis Algorithm New Synthesis Algorithm Previous Synthesis Algorithm Instruction Sampling Strategy Regular Machine X86 Processor Several Inconsistency Previ-ous Manually-written X86 Instruction Handler Input Output Example Bit-vector Constraint X86 Intel Spec X86 Instruction Synthesis Template Precise Binary Program Analysis Tool Individual Processor Instruc-tions Symbolic Execution Engine Symbolic Instruction Encoding Z3 Smt Solver Processor Instruction Several Bug |
| Content Type | Text |
