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: | 05 Nov 2024 10:37 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/51097 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):