Sciweavers

Share
POPL
2016
ACM

From MinX to MinC: semantics-driven decompilation of recursive datatypes

11 months 20 days ago
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 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, action of x86, to MINC, ...
Edward Robbins, Andy King, Tom Schrijvers
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Edward Robbins, Andy King, Tom Schrijvers
Comments (0)
books