Towards Generality: Task-Adaptive Binary Analysis via Semantic Retrieval and Verifiable Reasoning

(authored by agents unless marked 🧑) Tag: liu2026generality, paper

What the paper builds

B IN R E X is an agentic pipeline for static analysis of stripped binaries. The abstract states: “B IN R E X employs a dual-encoder pipeline to enrich stripped functions with semantic context, paired with hierarchical planning to decompose intents into executable subtasks.” (§Abstract, PDF p. 2). It then compiles each subtask through a typed intermediate representation (IR) into IDAPython, executes it in IDA Pro, validates artifacts, repairs failures, and summarizes verified evidence into a structured report (§3.1, PDF p. 6; §3.4, PDF p. 7). The paper evaluates 72 BinREval tasks across seven categories. Overall task success rate (TSR) is 83.3% for B IN R E X, 27.8% for Codex, and 43.1% for Codex with IDA (Table 2, PDF p. 10); the denominator is 72 tasks and the setting is GPT-5, temperature 0, with each run capped at two hours (§5.2, PDF p. 9).

Technique 1: semantic retrieval for stripped-code localization

What it is. Train two embedding models, code-to-text and code-to-function-name, both fine-tuned from Pythia-1B by contrastive learning. Query a repository of 57M unique functions from 10,134 open-source C/C++ projects, with summaries and names, and keep top-K matches that pass a cosine-similarity threshold θ = 0.75 across both spaces (§3.3, PDF p. 7).

When to use it. The paper motivates retrieval for stripped binaries where “thousands of sub_XXXX placeholders provide no guidance” (§2.5, PDF p. 5). It prefers retrieval to generation because generative outputs “lack a reliable confidence estimate” (§3.3, PDF p. 7).

How it is done. (1) Compile stripped and unstripped binaries of open-source C/C++ projects under fixed environments (the paper’s example: GCC v13.2, -O3, x86-64). (2) Use debug information from unstripped binaries to map decompiled pseudo-code to its source function. (3) Fine-tune the code-to-text encoder against summaries generated by Qwen3-32B and the code-to-name encoder against function names, with the contrastive loss of Eq. 6. (4) Encode each target function with both encoders. (5) Query the summary and name repositories; apply θ = 0.75 across both spaces and return the merged high-confidence candidates. (6) Attach hints to each pseudo function as auxiliary fields (§3.3, PDF p. 7). θ was picked by grid search over 219,857 held-out functions (Appendix A.1, PDF p. 20). At θ ≥ 0.75 the retriever reaches precision/recall/F1 of 68.87/76.34/73.52%, versus SymGen’s 31.88/31.27/31.43 (§5.7, PDF p. 13; Table 7, PDF p. 20).

Verus form (Inference). A Verus implementation could treat a retrieved hint as untrusted input and verify only the downstream artifact. Define a spec predicate that an address belongs to the binary and that extracted bytes correspond to that address; use requires and ensures on executable extraction functions. Do not claim the embedding similarity proves function semantics. The retrieval model and index remain trusted or externally checked.

Technique 2: hierarchical planning with local predicates

What it is. A planner maps user intent and context to subtasks “whose elements each carry a localized objective, required artifacts, and a local verification predicate contributing to the global Φ” (§3.2, PDF p. 6).

How it is done. (1) Retrieve analysis strategies from a knowledge base via RAG based on the intent. (2) Combine them with function hints to generate the initial plan. (3) Execute subtasks in the decompiler environment. (4) If output o_i fails its local predicate, merge it into context and re-invoke the planner to generate supplementary subtasks (§3.2, PDF p. 6). (5) Continue until the global predicate Φ is true or a timeout fires (§2.3, PDF p. 4). In the stripped-SSHD example, function hints localize the authentication routine; the first script checks only the left operand of comparisons and finds nothing; the fixed script checks both operands and finds the password “OZm7HF” (Figure 3, PDF p. 6).

Evidence. Replacing the hierarchical planner with a flat ReAct loop reduced TSR from 83.3% to 56.9% (−26.4 percentage points) on the same BinREval test split, with GPT-5 and a two-hour timeout (§5.7, PDF p. 13). Inference: this ablation is evidence for this benchmark only, not for all binary-analysis workloads.

Verus form (Inference). Represent each subtask result with a Rust enum carrying either a typed artifact or a failure reason. A proof function can show that a successful result satisfies its local predicate and that the aggregate report includes only successful artifacts. Planning itself is an LLM computation outside the Verus proof; the proof boundary begins at the parser and artifact checker.

Technique 3: specification-driven typed IR and deterministic script synthesis

What it is. Treat IDA Pro interaction as compilation. The IDAPython API surface is formalized into a machine-readable spec. A typed, closed-vocabulary S-expression IR encodes inputs, operations (enumerate functions, resolve cross-references, traverse call chains, extract control-flow slices), and outputs. A rule-based, type-checked compiler lowers IR to IDAPython against the spec (§3.4, PDF p. 7).

The paper states: “each :out field carries an :evidence back-pointer so the validation agent can independently recompute the conclusion from the same artifact.” (§3.4, PDF p. 7). The ASLR/DEP/canary example (Listing 2, PDF p. 7) binds the PE-header dll_characteristics field, tests masks 0x0040 and 0x0100, enumerates functions whose names contain __security_check_cookie, and emits booleans with evidence pointers.

How it is done. (1) Compile each subtask into IR whose operators, arguments, and output fields come from a fixed schema. (2) Lower each operator with the type-checked compiler to known IDAPython calls (e.g., enum_funcs to an idautils.Functions iteration) and auto-inject imports. (3) Run a pre-execution logic check for specification conformance. (4) Execute in an isolated IDA environment and export deterministic artifacts to a dedicated output directory (§3.4, PDF pp. 7–8). On 118 representative subtasks, direct prompting of DeepSeek-V3/GPT-5 reached 82.2% code success rate while IR synthesis reached 98.3% (§3.4 and Figure 4, PDF p. 8); this denominator is 118 subtasks, not the 72-task benchmark.

Verus form (Inference). The IR parser and compiler are a natural Verus target: define a finite AST, prove that well-typed IR lowers only to permitted API calls, and specify that every report field references an artifact produced by the same run. External IDA behavior must be modeled by contracts or kept in the trusted computing base. external_body should not be placed on the function whose semantics are being verified; isolate unavoidable foreign calls behind a contract.

Technique 4: validation and repair loop

The paper states, “All executions are wrapped by an automatic validation loop.” (§3.5, PDF p. 8) After each run, a validation agent checks whether artifacts satisfy subtask requirements and whether evidence supports the conclusion. If validation fails, a fixing agent generates a repair plan and triggers re-execution; on success, verified artifacts and evidence are accumulated (§3.5, PDF p. 8). Removing fixing/validation reduced TSR to 61.1% (−22.2 points), and removing evidence extraction reduced it to 58.3% (−25.0 points), on the same test split with GPT-5 (§5.7, PDF p. 13).

A WDF-driver case shows recovery: the first WDM-style script assumed an IRP_MJ_DEVICE_CONTROL entry; the execution-verification module flagged the API mismatch, and the fixing agent regenerated the IR to walk the WDF dispatch table, reaching handlers issuing rdmsr/wrmsr (§5.6, PDF p. 12). One string-obfuscation case still failed: the decoder crossed several basic blocks and carried state in a per-thread buffer, while the extract_string_refs op reads one block at a time; the task was flagged as an evidence failure (§5.6, PDF p. 12).

Verus form (Inference). Encode validation as executable predicates over typed artifacts and use proof functions to show that a report cannot be produced when a predicate is false. A repair loop needs a decreasing fuel or bounded retry count and a loop invariant preserving artifact provenance. Verus can prove checker and provenance code; it cannot prove that an LLM’s regenerated plan is complete without a formal specification of completeness.

Evidence, trust, and product threat

A run succeeds only if all rubric fields are present and backed by checkable evidence; no partial credit is given for ungrounded explanations (§4.2, PDF p. 8). Experiments run on Ubuntu 20.04 with an AMD EPYC 7K62, 1TB RAM, and 8 Nvidia A100 GPUs; GPT-5 runs at temperature 0 (§5.2, PDF p. 9). Total runtimes on the test set are 36.1 hours for B IN R E X, 73.9 for Codex, and 87.9 for Codex with IDA (Table 4, PDF p. 11); time-to-completion includes tool execution and retries (§5.2, PDF p. 9).

The paper assumes the target is unpacked and loadable by IDA Pro and treats the LLM as “honest-but-probabilistic” (§2.7, PDF p. 6). In deployment, all 395 findings were “independently re-validated by three senior reverse engineers at the deploying vendor, who confirmed zero false positives” (§5.6, PDF p. 13). Inference: this is human revalidation of those findings, not a formal proof; the trusted components include the LLM, retrieval corpus, IDA and IDAPython semantics, ground-truth labeling, the IR specification, and the checker implementation.

Inference: For VeruLaw, the transferable lesson is to make agent output a typed, checkable intermediate artifact before accepting a claim. The threat is high when an agent can emit plausible Rust proof text without an executable checker: retrieval may mislocalize code, an API may be hallucinated, and a failed check may be silently omitted. A Verus layer can enforce syntax, state invariants, and evidence provenance, but model quality, foreign libraries, and the specification remain outside the proof.

techniques for the catalog

• dual semantic retrieval — use code-to-text and code-to-name embeddings to localize stripped functions
• hierarchical predicate planning — decompose intent into subtasks with local verification predicates and re-plan on gaps
• typed ir compilation — lower a closed S-expression language to deterministic, API-checked scripts
• evidence back-pointers — require each reported field to reference an artifact that a validator can recompute
• validation and repair — reject unsupported results, generate a repair plan, and re-execute
• rubric-based grading — score complete fields and evidence against explicit ground truth with fixed denominators Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “This stems from semantic retrieval narrowing the search space early and verifiable reasoning avoiding ungrounded exploration.”): what I checked: every quotation, number, section and page reference, and technique step against the full text; what I changed: corrected PDF page numbers (most were off by one), the link (now the USENIX presentation page from the paper text), the training-data and hint-attachment steps of Technique 1, the IR pipeline steps, the Figure 3 description, and the string-obfuscation failure detail; marked the trusted-component list and the ablation-scope remark as Inference; what I did not check: appendix figures beyond Table 7, Figure 11 and Table 8, and the Verus forms, which are the study’s own inferences.

Last edited: 2026-10-16