Write a Blog >>
Wed 20 Jan 2016 15:10 - 15:35 at Grand Bay South - Track 2: Correct Compilation Chair(s): Jens Palsberg

Reconstructing the meaning of a program from its binary executable is known as reverse engineering; it has a wide range of applications in software security, exposing piracy, legacy systems, etc. Since reversing is ultimately a search for meaning, there is much interest in inferring a type (a meaning) for the elements of a binary in a consistent way. Unfortunately existing approaches do not guarantee any semantic relevance for their reconstructed types.

This paper presents a new and semantically-founded approach that provides strong guarantees about the reconstructed types. Key to our approach is the derivation of a witness program in a high-level language alongside the reconstructed types. This witness has the same semantics as the binary, is type correct by construction, and it induces a (justifiable) type assignment on the binary. Moreover, the approach effectively yields a type-directed decompiler.

We formalise and implement the approach for reversing MinX, an abstraction of x86, to MinC, a type-safe dialect of C with recursive datatypes. Our evaluation compiles a range of textbook C algorithms to MinX and then recovers the original structures.

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00: Track 2: Correct CompilationResearch Papers at Grand Bay South
Chair(s): Jens PalsbergUniversity of California, Los Angeles
14:20 - 14:45
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven
Pre-print Media Attached
14:45 - 15:10
Lightweight Verification of Separate Compilation
Research Papers
Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Media Attached File Attached
15:10 - 15:35
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Media Attached
15:35 - 16:00
Sound Type-dependent Syntactic Language Extension
Research Papers
Florian LorenzenTU Berlin, Sebastian ErdwegTU Darmstadt, Germany
Pre-print Media Attached File Attached