Search papers, labs, and topics across Lattice.
The paper introduces provenance-guided superset decompilation (PGSD), a novel framework for reverse engineering that structures decompilation as a sequence of modular passes which monotonically derive facts about the binary into a relation store. This approach retains ambiguous interpretations as parallel candidates with provenance, deferring resolution until the final selection phase, thereby avoiding premature commitments to a single interpretation. The authors implement PGSD in Manifold, a declarative reverse engineering framework, and demonstrate that it achieves comparable or superior decompilation quality compared to existing tools like Ghidra and IDA Pro while generalizing across compilers and optimization levels.
Decompilation can be as modular and declarative as compilation itself, enabling more robust and generalizable reverse engineering.
Reverse engineering tools remain monolithic and imperative compared to the advancement of modern compiler architectures: analyses are tied to a single mutable representation, making them difficult to extend or refine, and forcing premature choices between soundness and precision. We observe that decompilation is the reverse of compilation and can be structured as a sequence of modular passes, each performing a granular and clearly defined interpretation of the binary at a progressively higher level of abstraction. We formalize this as provenance-guided superset decompilation (PGSD), a framework that monotonically derives facts about the binary into a relation store. Instead of committing early to a single interpretation, the pipeline retains ambiguous interpretations as parallel candidates with provenance, deferring resolution until the final selection phase. Manifold implements PGSD as a declarative reverse engineering framework that lifts Linux ELF binaries to C99 through a granular intermediate representation in ~35K lines of Rust and Datalog. On GNU coreutils, Manifold's output quality matches Ghidra, IDA Pro, angr, and RetDec on multiple metrics while producing fewer compiler errors, and generalizes across compilers and optimization levels.
