Thu 16 Jun 2016 10:30 - 11:00 at Grand Ballroom Santa Ynez - Down to the Metal II Chair(s): Hans-J. Boehm

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 a mechanically synthesized formal semantics 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.

We describe an automatically synthesized formal semantics for 1,620 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.

Thu 16 Jun

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Down to the Metal IIResearch Papers at Grand Ballroom Santa Ynez
Chair(s): Hans-J. Boehm Google
10:30
30m
Talk
Stratified Synthesis: Automatically Learning the x86-64 Instruction Set
Research Papers
Stefan Heule Stanford University, Eric Schkufza VMware Research Group, Rahul Sharma Stanford University, Alex Aiken Stanford University
DOI Pre-print Media Attached
11:00
30m
Talk
Remix: Online Detection and Repair of Cache Contention for the JVM
Research Papers
Ariel Eizenberg University of Pennsylvania, Shiliang Hu Intel Corporation, Gilles Pokam Intel Corporation, Joseph Devietti University of Pennsylvania
Media Attached
11:30
30m
Talk
Statistical Similarity of Binaries
Research Papers
Yaniv David Technion, Nimrod Partush Technion, Eran Yahav Technion
Media Attached