Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Fri 19 Jun 2020 10:40 - 11:00 at PLDI Research Papers live stream - Verification II Chair(s): Manu Sridharan

Validating the correctness of binary lifters is pivotal to gain
trust in binary analysis, especially when used in scenarios
where correctness is important. Existing approaches focus
on validating the correctness of lifting instructions or basic
blocks in isolation and do not scale to full programs. In this
work, we show that formal translation validation of single instructions
for a complex ISA like x86-64 is not only practical,
but can be used as a building block for scalable full-program
validation. Our work is the first to do translation validation of
single instructions on an architecture as extensive as x86-64,
uses the most precise formal semantics available, and has
the widest coverage in terms of the number of instructions
tested for correctness. Next, we develop a novel technique
that uses validated instructions to enable program-level validation,
without resorting to performance-heavy semantic
equivalence checking. Specifically, we compose the validated
IR sequences using a tool we develop called Compositional
Lifter to create a reference standard. The semantic equivalence
check between the reference and the lifter output is then
reduced to a graph-isomorphism check through the use of semantic
preserving transformations. The translation validation
of instructions in isolation revealed 29 new bugs in McSema
– a mature open-source lifter from x86-64 to LLVM IR. Towards
the validation of full programs, our approach was able
to prove the translational correctness of 2254/2348 functions
taken from LLVM’s single-source benchmark test-suite.

Conference Day
Fri 19 Jun

Displayed time zone: Pacific Time (US & Canada) change

10:40 - 12:00
Verification IIPLDI Research Papers at PLDI Research Papers live stream
Chair(s): Manu SridharanUniversity of California Riverside

YouTube lightning session video

Scalable Validation of Binary Lifters
PLDI Research Papers
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Sushant DineshUniversity of Illinois at Urbana-Champaign, USA, Deepan VenkateshUniversity of Illinois at Urbana-Champaign, USA, Vikram S. AdveUniversity of Illinois at Urbana-Champaign, USA, Christopher W. FletcherUniversity of Illinois at Urbana-Champaign, USA
Polynomial Invariant Generation for Non-deterministic Recursive Programs
PLDI Research Papers
Krishnendu ChatterjeeIST Austria, Austria, Hongfei FuShanghai Jiao Tong University, China, Amir Kafshdar GoharshadyIST Austria, Austria, Ehsan Kafshdar GoharshadyFerdowsi University of Mashhad, Iran
Templates and Recurrences: Better Together
PLDI Research Papers
Jason BreckUniversity of Wisconsin-Madison, USA, John CyphertUniversity of Wisconsin-Madison, USA, Zachary KincaidPrinceton University, USA, Thomas RepsUniversity of Wisconsin-Madison, USA
First-Order Quantified Separators
PLDI Research Papers
Jason R. KoenigStanford University, USA, Oded PadonStanford University, USA, Neil ImmermanUniversity of Massachusetts at Amherst, USA, Alex AikenStanford University, USA