2024 · Conference paper
D-Helix: A Generic Decompiler Testing Framework Using Symbolic Differentiation
Tests decompilers function by function on binaries without needing source code. RECOMPILER repairs decompiled C so individual functions recompile, SYMDIFF compares symbolic models of the original binary function and the recompiled decompiled function using patched angr and PROMPT symbolic executors, and TUNER toggles decompiler heuristic rules to locate, and sometimes work around, the rule behind an inaccuracy. On Ghidra 10.0 and angr 9.2.30, 2,004 binaries and object files from coreutils, util-linux and six popular GitHub C projects yield 93K decompiled functions; the authors report 4,515 incorrectly decompiled functions, 8 reproduced known bugs, 17 previously unknown bugs and 7 bugs fixed automatically.
Scope and limitations
Only Ghidra and angr were tested; Hex-Rays, Binary Ninja, RetDec and LLM-based decompilers were not, and the authors estimate that supporting a decompiler with an unsupported IR would take at least 40 days of symbolic-engine work. Results are function-level symbolic equivalence checks on the authors’ 2,004 x86-64 Linux inputs, built with GCC 11.1.0 and Clang 16.0.0 at each project’s default optimization and excluding binaries over 30 MiB. Coverage is partial: RECOMPILER recompiled 72.4% of Ghidra’s and 45.0% of angr’s decompiled functions, and SYMDIFF analyzed 91.3% and 93.9% of those. Symbolic execution bounds loops, uses a two-minute default timeout, treats global variables as constants and does not parse floating-point constraints; accuracy trade-offs cause false positives, measured on 100-function samples per decompiler. TUNER automatically fixed 72 of the 443 inaccuracies it examined. A function passing the check is not proof of whole-program correctness.
Why it fits this collection
Adds automated, binary-level correctness testing for decompilers, complementing output benchmarks such as DecompileBench and qualitative studies of decompiler fidelity.
Publication and review details
- Venue
- USENIX Security 2024
- Status
- Conference paper
- Publication / posting date
- August 2024
- Date source
- Publication month from the official USENIX BibTeX (month = aug) and the final PDF cover for the 33rd USENIX Security Symposium, August 14–16, 2024; no exact publication day is asserted.
No paper DOI or arXiv identifier was verified; the record uses the reviewed USENIX Security 2024 presentation-page and usenixsecurity24-zou.pdf profile. The USENIX BibTeX gives the 33rd USENIX Security Symposium, pages 397–414, USENIX Association and month August; the presentation page also links an appendix PDF, slides and a prepublication PDF. The paper prints github.com/purseclab/Dhelix, which the GitHub API reports as not found; the code link uses purseclab/D-helix, whose README cites this paper. At reviewed commit fda23ef (2024-09-12), the repository declares BSD-3-Clause. Its README pins angr, claripy and pyvex commits for P-code and VEX variants, supplies patches for angr, claripy, PROMPT (built with clang 3.8) and Ghidra commit 15d22e8, and uses Z3 4.9.1. A dataset directory holds 2,004 compiled input files, which remain subject to their upstream projects’ licenses. Only source and documentation files were read; no binaries were downloaded and no code or experiments were run.
Sources reviewed
Source review only; experiments were not rerun for this collection. Cite the original authors using the linked paper or BibTeX.
Primary sources
- https://www.usenix.org/conference/usenixsecurity24/presentation/zou
- https://www.usenix.org/system/files/usenixsecurity24-zou.pdf
- README.md GitHub · purseclab/D-helix · Revision fda23ef
- LICENSE GitHub · purseclab/D-helix · Revision fda23ef
- dataset GitHub · purseclab/D-helix · Revision fda23ef