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:https://doi.org/10.1145/2837614.2837633) (Full text available)

Abstract

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
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: 27 Jun 2017 02:58 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/51097 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year