2016 Poster Sessions : Stratified Synthesis: Automatically Learning the x86-64 Instruction Set

Student Name : Stefan Heule
Advisor : Alex Aiken
Research Areas: Computer Systems
The x86-64 ISA sits at the bottom of the software stack of most desktop and server software. Because of its importance, many software analysis and verification tools depend, either explicitly or implicitly, on correct modeling of the semantics of x86-64 instructions. However, formal semantics for the x86-64 ISA are difficult to obtain and often written manually through great effort. We describe an automatically synthesized formal semantics of the input/output behavior for a large fraction of the x86-64 Haswell ISA’s many thousands of instruction variants. The key to our results is stratified synthesis, where we use a set of instructions whose semantics are known to synthesize the semantics of additional instructions whose semantics are unknown. As the set of formally described instructions increases, the synthesis vocabulary expands, making it possible to synthesize the semantics of increasingly complex instructions. Using this technique we automatically synthesized formal semantics for 1,751 instruction variants of the x86-64 Haswell ISA. We evaluate the learned semantics against manually written semantics (where available) and find that they are formally equivalent with the exception of 58 instructions, where the manually written semantics contain an error. We further find the learned formulas to be largely as precise as manually written ones and of similar size.

Stefan Heule is a third year PhD student in the Computer Science Department at Stanford University. Broadly speaking, his interests include program synthesis, programming languages and their design, software verification, type systems, static analysis, and formal methods in general. More specifically, he wants to find ways to build correct software, where tools provide guarantees about the desired behavior of a system. With computer systems becoming more and more widely used, specifically also in situations where their malfunction can have severe consequences, there is an increasing demand for software with very high reliability. He is interested in finding ways to statically reason about various correctness criteria as well as building automated tools that employ these techniques.