Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 14:00 - 14:30 at Sala XII - Research Papers: Program Verification Chair(s): Chris Hawblitzel

This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.

Mon 14 Jan

CPP-2019
14:00 - 15:30: CPP 2019 - Research Papers: Program Verification at Sala XII
Chair(s): Chris HawblitzelMicrosoft Research
CPP-201914:00 - 14:30
Research paper
Ian RoessleVirginia Tech, USA, Freek VerbeekOpen University of the Netherlands, The Netherlands, Binoy RavindranVirginia Tech
DOI
CPP-201914:30 - 15:00
Research paper
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes
DOI
CPP-201915:00 - 15:30
Research paper
Nicolas Koh, Yao LiUniversity of Pennsylvania, Yishuai LiUniversity of Pennsylvania, Li-yao Xia, Lennart BeringerPrinceton University, Wolf Honore, William ManskyUniversity of Illinois at Chicago, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
DOI