From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
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 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 16:00
|Fully-Abstract Compilation by Approximate Back-Translation|
Dominique Devriese iMinds - Distrinet, KU Leuven, Marco Patrignani KU Leuven, Frank Piessens iMinds - Distrinet, KU LeuvenPre-print Media Attached
|Lightweight Verification of Separate Compilation|
Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Chung-Kil Hur Seoul National University, Derek Dreyer MPI-SWS, Viktor Vafeiadis MPI-SWS, GermanyMedia Attached File Attached
|From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes|
Research PapersMedia Attached
|Sound Type-dependent Syntactic Language Extension|
Research PapersPre-print Media Attached File Attached