Skip to main content
Kent Academic Repository

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

Robbins, Edward, King, Andy, Schrijvers, Tom (2016) From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes. In: Guha, Arjun and Chong, Steve, eds. POPL '16. . pp. 191-203. ACM Press, St. Petersburg, Florida, USA ISBN 978-1-4503-3549-2. (doi:10.1145/2837614.2837633) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:51097)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://dx.doi.org/10.1145/2837614.2837633

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: Conference or workshop item (Paper)
DOI/Identification number: 10.1145/2837614.2837633
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 20 Oct 2015 11:08 UTC
Last Modified: 17 Aug 2022 12:20 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/51097 (The current URI for this page, for reference purposes)

University of Kent Author Information

Robbins, Edward.

Creator's ORCID:
CReDIT Contributor Roles:

King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.