PaperlayerView exact revision on arXiv

Source-linked AI summary

Behavior Specification-Guided Program Synthesis for Binary Deobfuscation

Kangchen Zhu, Shangwen Wang, Zhiliang Tian, Zhouyang Jia, Xiaoling Li, Jun Ma, Jie Yu, Xiaoguang Mao

arXiv:2608.20628v1cs.SE

TL;DR

Binary deobfuscation is difficult because source-level information is often unavailable and decompiler-based transformations provide limited assurance of behavioral preservation. BINMIRROR uses dynamic execution traces and interaction snapshots to guide source synthesis, achieving strong recovery and downstream security-analysis results while remaining bounded by observed executions and platform scope.

  • Problem

    Source-oriented methods and decompiler-based binary workflows struggle when compilation removes high-level semantics, limiting reliable recovery from stripped binaries.

  • Method

    BINMIRROR reformulates binary deobfuscation as behavior-specification-guided synthesis using dynamic traces, interaction snapshots, and runtime-guided constraints.

  • Results

    BINMIRROR improves robustness and analyzability under heavy obfuscation, including 68.4% CodeBLEU, 76.2% lower cyclomatic complexity, and higher malware-detection accuracy and F1.

  • Takeaways & Limitations

    Behavior-constrained synthesis offers a practical direction for binary deobfuscation when static structure and decompiler output are unreliable.

  • Takeaways & Limitations

    Validation is bounded by observed executions and available tests, and the current implementation targets Linux binaries across x86, x64, ARM, and MIPS.

Abstract

from arXiv · show

Deobfuscation is critical to reverse engineering and security analysis because it restores the readability and analyzability of obfuscated code. However, existing research primarily focuses on source-code deobfuscation, while binary-level deobfuscation remains largely underexplored despite its practical importance when source code is unavailable. Existing binary deobfuscation methods typically decompile binaries into pseudocode and then apply structural transformations. However, because compilation discards high-level semantics such as precise type information and source-level structures, this decompilation-based paradigm often produces low-quality code and provides limited assurance that the recovered code preserves the runtime behavior of the original program. To address these limitations, we propose a paradigm shift from structural transformation to behavior-driven synthesis. Our core insight is that although obfuscation distorts a program's internal structure, semantics-preserving transformations must retain its observable execution behavior. Based on this insight, we introduce BinMirror, an approach that reformulates binary deobfuscation as a behavior-specification-guided program synthesis task. By treating dynamic execution traces and interaction snapshots as behavioral specifications, BinMirror synthesizes high-quality source code and validates it against runtime observations collected from heavily obfuscated binaries. Extensive evaluations on 1.5 million synthetically obfuscated binaries show that BinMirror significantly outperforms state-of-the-art baselines, achieving a unit-test Pass@1 of 74.5% under extreme obfuscation. These results demonstrate the practical utility of BinMirror in restoring semantic clarity for real-world security analysis.

1. Introduction

Binary deobfuscation is needed for security analysis, but source-oriented methods and decompiler-based workflows struggle when compilation removes high-level structure. BINMIRROR instead synthesizes source code from observed behavior and evaluates its recovery effectiveness and practical utility.

  • Motivation: Obfuscation preserves intended functionality while making program structure opaque, creating demand for deobfuscation in reverse engineering and security analysis.Applications include malware analysis and software plagiarism detection.
  • Problem: Existing methods rely on source-level information that is often unavailable in stripped binaries, leading practitioners to decompile binaries before applying source-level transformations.Decompilation can discard or obscure precise types, meaningful identifiers, and structured syntax.
  • Evaluation: 1.5 million synthetic obfuscated binaries and real-world obfuscated malware were used to evaluate recovery effectiveness, readability, and downstream malware-detection utility.The synthetic benchmark spans four obfuscators, four architectures, and four compiler optimization levels.
  • Results: 68.4% CodeBLEU and a 76.2% reduction in cyclomatic complexity were achieved under extreme obfuscation, while malware-detection accuracy and F1 improved by 33.3% and 37.1%.The validation is bounded by available tests and observed executions rather than proving semantic equivalence for all possible inputs.
  • Approach: BINMIRROR shifts binary deobfuscation from syntax-driven transformation to behavior-specification-guided program synthesis.The framework uses dynamic traces and interaction snapshots as behavioral specifications for an LLM-based source reconstruction process.
  • Approach: BINMIRROR combines syscall-guided behavior capture, trace-enhanced slicing, LLM-based synthesis, and differential testing to validate reconstructed source against observed runtime behavior.The pipeline is presented as an end-to-end reconstruction framework.

2. Background and Related Work

Binary deobfuscation targets stripped executables where source-level information is unreliable, while prior systems often focus on localized simplification or depend on costly search. BINMIRROR distinguishes itself by converting runtime behavior into constraints for end-to-end source reconstruction.

  • Background: Binary deobfuscation seeks readable, analyzable source from stripped binaries while validating consistency with observed runtime behaviors and available tests.The validation is observation-bounded rather than a proof of semantic equivalence over all inputs.
  • Resources: The paper's evaluation materials are publicly available through the cited Zenodo record.The passage identifies the code and data repository.
  • Related Work: Existing synthesis-based systems can simplify obfuscated expressions but are often limited by predefined rules, path coverage, state explosion, and symbolic or enumerative search costs.Heavy control-flow flattening, bogus branches, MBA transformations, and decompiler type loss can make static representations misleading.
  • Related Work: Dynamic approaches provide behavioral evidence, but their results remain bounded by observed executions because untriggered paths cannot be captured.This bounds what behavior-based methods can establish.
  • BINMIRROR: BINMIRROR turns runtime behavior into state-transfer constraints, extracts behavior-relevant binary slices, and synthesizes compilable C validated on held-out executions.This differentiates it from expression-level synthesis and decompiler-plus-LLM pipelines that mainly rely on recovered pseudocode.

3. Motivation Example

Decompiler-based transformations can misinterpret security-relevant behavior when compilation obscures high-level semantics such as precise integer types. BINMIRROR uses concrete runtime states and branch outcomes to constrain synthesis instead.

  • Limitation of decompilation: Decompiler-based pipelines may produce low-quality code or remove security-relevant behavior when compilation obscures function names, control structures, and precise variable types.The resulting pseudocode may lack the context needed to interpret program logic accurately.
  • Pipeline: BINMIRROR follows four stages that capture behavior, filter trace noise, synthesize readable source, and validate candidates through differential testing.The pipeline transforms observed runtime behavior into behavior-constrained source-code synthesis and test-based validation.
  • Motivating example: An 8-bit overflow check depends on uint8_t wraparound, but decompilation may promote the value to a wider signed integer and make the check appear impossible.The original value wraps from 255 to 0, whereas the recovered signed-integer expression no longer represents that behavior.
  • Behavioral specification: BINMIRROR records runtime memory state and branch outcomes from an overflow-triggering input to form an execution-derived behavioral specification.For input 255, the captured initial memory state and observed branch outcome provide factual evidence for synthesis.

4. Approach

BINMIRROR captures observable runtime behavior, filters traces to behavior-relevant instructions, synthesizes source code under behavioral constraints, and validates candidates through differential testing.

  • 4.2. Behavior Specification Capture: BINMIRROR uses syscall-guided exploration and dynamic binary instrumentation to capture execution traces and interaction snapshots from obfuscated binaries.The snapshots record syscall identity, initial register state, and relevant memory regions at monitored interaction points.
  • 4.5. Test-Based Behavioral Validation: Candidate code is executed in a context-aware harness and compared with the original binary, with discrepancies fed back for closed-loop refinement.Validation checks observed syscall identifiers, arguments, and relevant memory payloads rather than proving equivalence over all inputs.
  • 4.2. Behavior Specification Capture: Inputs are retained when they produce novel syscall sequences, prioritizing externally observable interaction behavior over source-level coverage.The exploration feedback is based on interaction novelty rather than artificial control-flow coverage or type information.
  • 4.3. Specification-Driven Noise Filtering: Trace-enhanced backward slicing removes executed instructions that do not influence the monitored interaction state, including dispatcher updates, opaque predicates, and MBA junk.The slice is computed from register and memory dependencies and can skip scheduling-related dispatcher noise.
  • 4.4. Specification-Guided Program Synthesis: An LLM lifts the behavior-relevant slice and snapshot into candidate source code by maximizing the candidate's probability under those execution constraints.The synthesis input is Lext together with Bspec, and the output is candidate source code.

5. Experimental Setup

The evaluation combines a controlled synthetic benchmark, a real-world malware benchmark, multiple correctness and readability metrics, and comparisons against diverse deobfuscation baselines.

  • Evaluation Scope: The study evaluates effectiveness, architectural and optimization robustness, component contributions, readability, and downstream malware-detection utility.These five perspectives are organized as research questions RQ1–RQ5.
  • Datasets: The Synthetic Benchmark contains 1.5 million unique obfuscated binaries generated across four obfuscators, four architectures, and compiler optimization levels O0–O3.The benchmark is constructed from selected CodeNet C/C++ programs with available source-level tests.
  • Datasets: MalBench provides a real-world malware benchmark for practical security evaluation while retaining metadata without redistributing live malware.The metadata includes hashes, family labels, first-seen dates, sandbox policy, and benign provenance.
  • Evaluation Metrics: The evaluation uses Compilation Rate, Unit Test Pass Rate, Execution Success Rate, CodeBLEU, and cyclomatic complexity to assess correctness and readability.Pass@1 measures source-test success on the Synthetic Benchmark, while ESR compares monitored syscall and I/O behavior on MalBench.
  • Evaluation Metrics: Validation inputs cover 95% of target-region basic blocks and 90% of branch edges on the Synthetic Benchmark, versus 88% and 70% on MalBench.The reported statistics do not imply complete path coverage or semantic equivalence for all inputs.
  • Baselines and Protocol: BINMIRROR is compared with static, symbolic/dynamic, hybrid synthesis, and LLM-based baselines, with LLM baselines receiving decompiler-generated pseudocode.Experiments use fixed versions, settings, prompt templates, and repeated independent seeds for LLM-based methods.

6. Evaluation

BINMIRROR remains effective under severe obfuscation, across architectures and optimization levels, while producing readable reconstructions and improving downstream malware detection. Ablations indicate that behavior-relevant slicing, I/O constraints, and iterative refinement each contribute to performance.

  • RQ1: Effectiveness: 74.5% Pass@1 at L6, outperforming ChatDEOB by 54.3 percentage points while achieving an 81.4% compilation rate.BINMIRROR maintains higher effectiveness under severe obfuscation than the strongest evaluated baseline.
  • RQ1: Effectiveness: BINMIRROR succeeds alone on 1,331 of 3,000 sampled cases, or 44.4%, recovering samples missed by representative baselines.These cases mainly involve control-flow flattening, opaque predicates, MBA transformations, and decompiler-induced type or structure loss.
  • RQ2: Robustness: At L6, BINMIRROR achieves 78.57% success on X64-O0 and 68.92% on ARM-O0, versus ChatDEOB’s 25.51% and 22.90%.The comparison covers robustness across instruction-set architectures under extreme obfuscation.
  • RQ3: Ablation Study: At L6, removing backward slicing reduces Pass@1 from 74.5% to 28.5%, removing I/O constraints to 48.4%, and removing iterative refinement to 60.5%.The ablation attributes complementary contributions to filtering obfuscation noise, grounding generation, and improving behavioral consistency.
  • RQ4: Code Quality and Readability: Under L6, BINMIRROR sustains 68.4% CodeBLEU, 76.2% cyclomatic complexity reduction, and 72.8% Halstead Effort Reduction.The reconstructed code is reported as more compact and readable than outputs from comparison methods.
  • RQ5: Downstream Utility: The BINMIRROR-enhanced malware detector achieves 91.5% accuracy and 91.2% F1-score, improving over direct binary analysis by 33.3 and 37.1 percentage points.The improvement is attributed to behavior-consistent reconstructed artifacts that preserve behaviorally relevant control-flow patterns.

7. Discussion

BINMIRROR’s discussion identifies convergence, slice length, and observation quality as practical boundaries on behavior-guided synthesis. Iterative feedback improves recovery but exhibits diminishing returns, while long slices and incomplete observations remain important failure sources.

  • Sensitivity and Convergence: 60.5% Pass@1 without refinement rises to 74.5% after five iterations, while overhead reaches 55.2 seconds at ten iterations.The authors therefore set Nmax = 5 to balance recovery effectiveness and computational efficiency.
  • Observation and Slicing Boundaries: Incomplete behavior-relevant slices can prevent the LLM from inferring missing logic when implicit dependencies, pointer aliases, or memory effects are omitted.This limitation persists despite refinement prompts.
  • Slice Length and Context Boundaries: 92.4% and 85.1% Pass@1 are achieved for slices of at most 100 instructions, but success falls to 45.2% beyond 250 and 21.6% beyond 500 instructions.Short-to-medium slices constitute 60% of the dataset, whereas long dense assembly sequences degrade low-level data-flow context.
  • Slice Length and Context Boundaries: Long assembly slices can cause omitted dependencies, truncated outputs, or inconsistent control/data-flow structures, motivating hierarchical chunking for future extensions.The proposed direction recursively partitions large dependency graphs into smaller behavior-preserving subtasks.
  • Internal Validity: Validation is bounded by captured executions because instrumentation, emulation, and slicing inaccuracies can produce incomplete states or false positives.The paper explicitly does not claim semantic equivalence over all possible inputs.
  • Internal Validity: BINMIRROR’s effectiveness depends on observable interaction boundaries and behavior-relevant state transitions; dormant or CPU-local computations may receive weak specifications.Uncovered behavior remains outside the observation-bounded oracle.
  • External Validity: The current implementation targets Linux and evaluates x86, x64, ARM, and MIPS, while other operating systems require additional engineering.The authors also identify possible benchmark contamination as a validity threat.

8. Conclusion

The conclusion presents BINMIRROR as behavior-specification-guided synthesis for binary deobfuscation, using runtime observations to constrain and validate source reconstruction. The evaluation supports its robustness under heavy obfuscation and utility for downstream malware analysis.

  • Conclusion: BINMIRROR uses dynamic execution traces and interaction snapshots to constrain source-level reconstruction and validate recovered code against observed runtime behavior.The approach targets cases where static structure and decompiler output are unreliable.
  • Conclusion: The evaluation reports improved robustness under heavy obfuscation, more analyzable reconstructions, and useful executable artifacts for downstream malware analysis.The conclusion characterizes behavior-constrained synthesis as a practical direction for binary deobfuscation.

Appendix A. Synthetic Benchmark Audit

The synthetic benchmark audit documents filtering, expansion, security-data handling, and controlled evaluation procedures. The retained programs and malware corpus support reproducible protocols while imposing explicit representativeness and distribution constraints.

  • Filtering: The retained 1,573 CodeNet programs are executable, testable, and obfuscatable, but are not intended to represent the full CodeNet distribution.Table 10 assigns each excluded program one mutually exclusive first-failed filtering reason.
  • Benchmark Construction: 1,585,584 binaries result from expanding 1,573 retained programs across 63 obfuscation configurations, four architectures, and four optimization levels.The recorded metadata include source hashes, compiler settings, test metadata, seeds, and partition identifiers.
  • MalBench: MalBench contains 500 Linux malware samples collected during 2023–2025 and is released through hashes and audit metadata rather than live binaries.Samples require Linux executability, at least 10 VirusTotal detections, and unique SHA-256 hashes.
  • Evaluation Controls: All RQ5 pipelines share detector settings, graph extraction, model configuration, training seed, validation split, and threshold-selection rules.Reported 95% confidence intervals use 10,000 bootstrap resamples with seed 42.

Appendix C. Baseline Information Budgets

The baseline audit controls information exposure and generation settings so comparisons distinguish runtime evidence and feedback from method design. Held-out inputs remain excluded from prompts and refinement.

  • Information Budgets: Static-only baselines receive raw binaries or tool-specific IR, while decompiler- and LLM-based baselines receive pseudocode under matched prompt and token budgets.The comparison assigns each baseline an explicit information budget and limits decompiler-based variants to one compile-error repair round.
  • Controlled Comparisons: LLM-based variants use temperature 0.2 and top-p 1.0, with dynamic evidence serialized identically across controlled variants and BINMIRROR.The design tests whether runtime evidence or feedback alone explains gains, while BINMIRROR adds its full behavior-guided pipeline.
  • Evaluation Isolation: Held-out inputs are excluded from prompt construction, repair, feedback generation, and iterative refinement across LLM-based variants.This preserves the separation between available refinement evidence and held-out evaluation inputs.

Appendix D. Implementation Details

The implementation fixes evaluation and generation settings across BINMIRROR and its baselines, while recording artifacts and controlling context truncation.

  • Experimental Environment: All experiments ran on a dual-Xeon workstation with 512GB RAM and four RTX 4090 GPUs under Ubuntu 22.04 LTS.Malware execution was isolated using Docker and QEMU.
  • LLM Configuration: BINMIRROR and LLM-based baselines used fixed prompts, temperature 0.2, top-p 1.0, and a 4K output-token cap.Evidence-augmented variants and BINMIRROR received a 32K/4K input-output budget, while pseudocode-only variants used 16K/4K.
  • LLM Configuration: BINMIRROR and dynamic-feedback variants allowed up to Nmax = 5 refinement rounds, while other LLM variants allowed at most one compile-error repair round.
  • Reproducibility: Exact model identifiers, provider or checkpoint information, seeds, prompt hashes, serialized evidence, and request logs were recorded in the artifact.
  • Evaluation Controls: Held-out inputs were excluded from prompts, repairs, feedback, truncation decisions, and refinement traces.When context exceeded the budget, signatures, call sites, monitored snapshot fields, and recent behavior-relevant traces were preserved first.

D.3. Evaluation Scale and Resource Usage

The evaluation spans a large synthetic benchmark, targeted architecture and optimization subsets, and a malware benchmark, with rates computed over each evaluated denominator.

  • Evaluation Scale: 1,585,584 synthetic binaries comprise the full obfuscated benchmark expansion, not the denominator for every experiment.RQ1 uses the x64-O0 subset including L0, RQ2 uses the architecture/optimization sweep, and MalBench uses 500 malware samples under family-aware splits.
  • Reporting: All reported rates use the corresponding evaluated denominator, retaining completed non-timeout pass and fail validation outcomes.Timeout or unsupported runs are not silently removed.
  • Resource Usage: Runtime is reported as median [IQR] per evaluated sample, and LLM calls are counted over synthesis-invoking runs.
  • Resource Usage: CPU time includes dataset construction, binary execution, baseline execution, slicing, synthesis orchestration, and validation.LLM token counts include prompt and generated tokens across LLM-based baselines, controlled variants, and BINMIRROR.
Loading 2608.20628v1…