Skip to main content

From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes

Robbins, Ed and King, Andy and Schrijvers, Tom (2016) From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes. In: Guha, Arjun and Chong, Steve, eds. Symposium on Principles of Programming Languages. ACM Press, St. Petersburg, Florida, USA, pp. 191-203. (doi:10.1145/2837614.2837633)


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 for 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.

Item Type: Book section
DOI/Identification number: 10.1145/2837614.2837633
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Andy King
Date Deposited: 20 Oct 2015 11:08 UTC
Last Modified: 29 May 2019 16:10 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year