fold/docs/research/binary-detector-research.md

Binary-lane detector research program (null-deref / int-overflow / use-after-free)

Three remaining binary-lane (P-Code) detector gaps are research-grade, not quick heuristics. Each gap below states the current detector state, the core + complementary literature, the contributing factors the experiments evaluate, and the candidate implementation paths. Each gap is driven by a dedicated research loop (see .pi/loops): review literature → form/refine hypotheses → implement a bounded change → validate against bench/score_binary.py → retain/reject.

Benchmark oracle: tests/fixtures/binary/cwe/ + bench/gold/binary-security.json

• bench/score_binary.py. Baseline (honest): oob-access F1=1.000, div-by-zero F1=1.000, null-deref/int-overflow/use-after-free F1=0.

---

Gap 1 — binary null-deref (P-Code lane)

Current state. maybeNullDeref (src/symbolic/pcode_encoder.cpp) fires only when a Load/Store address simplifies to the numeral 0. The interprocedural case (caller passes a null-able value to a callee that derefs it) was attempted as a forward data-flow summary and REJECTED (docs §19): libc noise (explicit NULL sentinels) and stripped-binary function-boundary confusion.

Core literature.

• Wang, Jin, Gong 2013 — "Null Dereference Detection via a Backward Analysis" (APSEC), 10.1109/apsec.2013.80.
• Value-dependence NPD — ISSRERW 2015, 10.1109/issrew.2015.7392049.

Complementary literature.

• angr backward slicing (angr/analyses/backward_slice).
• VulSimple 2023 (10.1145/3652628.3652796) and "Binary Intermediate Slicing" 2023 (10.1109/qrs-c60940.2023.00087) — backward slicing over binary IR.

Contributing factors (sub-hypotheses).

• F1: path-sensitive zero-propagation through Load/Store/Copy in the SSA stream (does carrying a 0 through the mem_ model and the def-chain improve recall?).
• F2: backward slicing from the deref to a null source (does backward evidence suppress the libc noise that killed the forward summary?).
• F3: the rejected interprocedural summary, re-gated on backward proof (the caller's arg is provably null only if a backward slice from the deref reaches a constant-0 or a Store-of-0).
• F4: the raw stream's existing zero-propagation (scanInstructionsForConstHazards in src/binary/r2_disasm_state.cpp) already tracks constant-zero registers/slots; whether its null-deref signal can be lifted into the P-Code lane.

Potential paths.

• P1: backward NPD in the encoder — from each Load, walk in_def/def-chain back to a Copy 0 or a Store-of-0 slot; fire null-deref only on that proof.
• P2: value-dependence — a deref whose address is a pure function input that the caller binds to a provably-null value (revisit the summary, keyed on the caller passing a constant 0, with the callee deref confirmed by backward evidence).
• P3: reuse scanInstructionsForConstHazards (disasm zero-propagation) as a corroborating null-deref source in the pcode_scan path (it is already used for div-by-zero in the raw lane).

---

Gap 2 — binary int-overflow (P-Code lane)

Current state. The raw P-Code stream carries IntCarry/IntSCarry/ IntSBorrow ops and the SSA stream carries IntAdd/IntSub/IntMult, but the encoder's handleIntegerArithmetic does NOT emit int-overflow findings (no carry/overflow hook). Benchmark cwe190_overflow (a + INT_MAX) scores FN=1.

Core literature.

• "SMT-constrained symbolic execution engine for integer overflow detection in C code" (ISSA 2015), 10.1109/issa.2015.7335070.

Complementary literature.

• "Automated Generation of Buffer Overflow Quick Fixes Using Symbolic Execution and SMT" (2015), 10.1007/978-3-319-24255-2_32 — SMT overflow modeling as a reusable primitive.

Contributing factors (sub-hypotheses).

• F1: carry-flag evidence — treat IntCarry/IntSCarry/IntSBorrow (raw) as overflow sites and map to int-overflow findings.
• F2: SMT sign-mismatch — for a + b, overflow holds when sign(a)==sign(b) && sign(a+b)!=sign(a) (signed); model it in handleIntegerArithmetic and gate on a reachable path.
• F3: width correctness — whether the P-Code varnode size faithfully reflects the source operand width (a truncation/zx mismatch would silently drop overflows).
• F4: constant-folded overflow — a + INT_MAX with a constant RHS may be provable directly without a solver.

Potential paths.

• P1: emit int-overflow on IntCarry/IntSCarry/IntSBorrow in the raw lane (the ops already exist; only the finding hook is missing).
• P2: signed-overflow SMT check in handleIntegerArithmetic (binArith), firing onBinaryArith(IntOverflow) when the sign-mismatch condition is satisfiable.
• P3: port the source-lane int-overflow detector's core (src/detect/int_overflow* uses Z3 sign analysis) to the P-Code ops.

---

Gap 3 — binary use-after-free (P-Code lane)

Current state. The disasm UAF (R2Backend, scanInstructionsForUaf) is wired into the CLI --mode binary path and its x86-64 operand parsing is now FIXED (docs §20: bracketOperand space-normalization + firstRegisterOperand size-prefix rejection). But the pcode_scan path (what bench/score_binary.py runs) has no UAF detector, so the benchmark scores UAF F1=0. Wiring the disasm UAF into pcode_scan was REJECTED: it opens a fresh R2Session per binary and contends on the shared embedded r2 core (hangs).

Core literature.

• "Scalable Static Detection of Use-After-Free Vulnerabilities in Binary Code" (IEEE Access 2020), 10.1109/access.2020.2990197.
• UAFx (gts3.org, 2025) — UAF fuzzing/oracle.

Complementary literature.

• "Finding the needle in the heap: combining binary analysis techniques to trigger use-after-free" — combining static + dynamic.

Contributing factors (sub-hypotheses).

• F1: P-Code heap model — track malloc/free callees and a freed-slot set in the SSA encoder; a Load/Store through a freed slot is a UAF. (Pure P-Code, no r2.)
• F2: efficient disasm-UAF reuse — pass an already-open R2Session (or cap the sweep to the functions already extracted) instead of opening a fresh session, so the existing disasm UAF can run inside pcode_scan without the hang.
• F3: measure the R2Backend path's UAF F1 directly (the parsing fix may already make fold scan --mode binary detect cwe416; the benchmark scorer should then either use that path or document that UAF is a disasm-lane detector).

Potential paths.

• P1: P-Code UAF — in the encoder, a free(slot) call marks the slot freed; a subsequent Load/Store whose address resolves to that slot fires use-after-free (needs the slot provenance the retained parsing fix establishes).
• P2: reuse the disasm UAF with an existing session (lighter than a fresh R2Session), gated on frees_memory as today.
• P3: run the benchmark scorer against the CLI binary path (which already has the disasm UAF) instead of pcode_scan, so UAF is measured in its native lane.

---

Loop cadence and experiment discipline

Each gap's loop follows the fold-sast precision workflow: measure first, attribute the owner (one sub-hypothesis per iteration), state the invariant (no regression on oob/div0 F1 and the clean negative), require TP/FP/FN labels, and run an ablation before retaining a change. Rejections are reverted and documented.

---

Iteration log

Gap 2 (int-overflow) — iteration 1 (REJECTED): carry-flag hook

P1 (emit int-overflow on IntCarry/IntSCarry/IntSBorrow) was implemented and REJECTED: the encoder mapped IntSCarry→Add/IntSBorrow→Sub with isSourceSigned into the observer's existing signed-overflow model, but the zig runtime links ~153 checked-arithmetic sites (seto after every potential overflow) into every fixture, so pcode_scan cwe190_overflow produced 153 int-overflow findings (the vuln is only one of them; the other 5 fixtures would each FP the same way). The "satisfiable signed overflow" signal is too weak for zig-compiled binaries — it needs taint/reachability filtering (is the overflowing operand attacker- controlled?) or a non-zig (clang/gcc) fixture recipe. Reverted.

---

Workflow v2 — one gap at a time, signal-to-noise pre-check

The first iteration exposed a structural problem that the initial 3-loop setup did not anticipate: every fixture is zig-compiled, so the zig runtime (checked arithmetic, libc malloc/free, param-deref helpers) is linked into every binary. Any detector signal the runtime ALSO emits will fire ~100+ times across the fixtures, swamping the single real vuln. Three of the four rejected attempts (§19 null-deref, §20 UAF wiring, iteration-1 int-overflow) all failed the same way: a satisfiable/structural signal that is NOT specific to the vuln.

Improved workflow (one sequential loop):

1. Gap order (one at a time, in state file docs/research/binary-detector-state.md): null-deref → int-overflow → use-after-free.

2. Signal-to-noise pre-check (before any implementation). For the current gap's candidate path, measure the signal's specificity: run pcode_scan on clean.elf (the negative control) and count how many times the candidate signal fires in the zig runtime alone. If it fires on clean.elf (which has NO vuln), the signal is toolchain noise — the path needs either (a) a taint/reachability filter (is the overflowing/deref/freed value attacker- controlled?), or (b) a non-zig (clang/gcc) fixture recipe so the runtime is clean. Do NOT implement a path that fails the pre-check.

3. Fixture-recipe hypothesis. A leading cross-cutting path is to add a clang/gcc-compiled corpus variant (no zig checked-arithmetic runtime). If the runtime noise disappears, the simple signals (carry flag, param deref, freed slot) may become precise without taint. Evaluate this ONCE, before the three per-gap detectors.

4. Bounded implementation + validate + retain/reject (unchanged): implement one sub-hypothesis, ninja -C build/release, benchmark bench/score_binary.py, binary tests, retain only on F1 gain with no oob/div0 regression and no clean.elf FP; else revert + document.

---

Fixture-recipe evaluation (iteration 2) — BLOCKED, refined hypothesis

Tested the clang/gcc fixture-recipe hypothesis (Workflow v2 step 2):

1. macOS clang cannot cross-link a Linux ELF (ld: unknown options: --hash-style=gnu ...). clang emits Linux object code under -target x86_64-linux-gnu, but the macOS linker cannot produce the ELF. zig cc is the only working cross-compiler on this host, so the fixtures MUST stay zig-compiled. (compile-only clang -S still works for inspection.)

2. clang/gcc remove the zig-specific carry-flag signal. clang -S -O0 of vuln(int a){ return a + 2147483647; } emits addl $2147483647, %eax; retq with NO seto/jo — signed overflow is UB, so clang does not check it. zig emits add + seto (checked arithmetic). So the carry-flag path (P1) is zig-specific; a clang recipe would remove BOTH the noise and the signal.

Refined hypothesis for int-overflow: the detector must use the compiler-agnostic SMT sign-mismatch (P2, the observer already implements it), gated on taint/reachability — the overflowing operand must be attacker-controlled (argc/atoi/argv), not the zig runtime's internal bounds checks. The ~153 zig runtime sites are internal; only the vuln's a + INT_MAX with input-derived a is the real hazard. Next step: add a taint/reachability filter to the P2 overflow check (track which registers/values derive from function inputs / argv, and fire only when an overflowing operand is tainted).

---

Build lanes (macOS + Linux) — fixture recipe resolved

The fixture-recipe hypothesis exposed a toolchain gap, not a detector gap:

Lane	Host	Toolchain	Produces	Recipe
macOS (dev)	arm64	zig cc -target x86_64-linux-gnu	x86-64 Linux ELF	zig (checked-arithmetic runtime)
Docker/Linux	arm64 (this Mac)	native clang	aarch64 Linux ELF	clean (no zig runtime) — also unblocks the aarch64 corpus extension
CI (ubuntu-latest)	x86-64	native clang-19	x86-64 Linux ELF	clean, apples-to-apples vs zig

tests/fixtures/binary/build-linux.sh (committed) builds the CWE fixtures in a Linux container. The x86-64 cross-compile on an arm64 host is finicky (multiarch libc layout); the x86-64 CI lane is the canonical source of x86-64 clang fixtures. Evaluation therefore runs on BOTH platforms: macOS (zig recipe) and Linux (clang/gcc recipe + aarch64). The detector gap research should measure signal-to-noise on the clang recipe, where the zig runtime noise is absent, then port the retained detector back to the zig recipe with taint/reachability gating.

---

Iteration log (continued)

Build-lane result — gcc x86-64 cross-compile works (clean recipe available)

x86_64-linux-gnu-gcc (in ubuntu:24.04) cross-links x86-64 Linux ELF cleanly, where clang's --sysroot= misses the multiarch libc.so.6. So the clean x86-64 recipe is now producible on the arm64 Mac (and natively in the x86-64 CI). The committed tests/fixtures/binary/build-linux.sh uses gcc for x86-64 and plain gcc/clang for native x86-64.

Clean-recipe (gcc x86-64) detector results vs the zig recipe:

fixture	gcc x86-64	zig x86-64
cwe121_bof (oob)	1 finding	1 finding
cwe369_div0	0	1
cwe190_overflow	0	0 (no detector)
clean	0	0

New finding — div0 is codegen-sensitive. gcc emits cdq; idiv dword [var_4h] (memory divisor); zig emits cdq; idiv ecx (register divisor). The div0 detector fires on the zig register form but not the gcc memory form. Likely the machine_division_addresses gating (the SLEIGH lifter's division-address extraction) misses the gcc memory-operand idiv. This is a concrete, tractable detector bug to fix independently of the int-overflow gap.

div0 root cause (iteration 3) — the detector is zig-assisted

The div0 detector fires on constant_zero || currentPathImplies(rhs == zero) (path-IMPLIED zero, not satisfiable). Probing the two recipes:

• zig cwe369_div0: implied=1, path=(= pc_unk_4 0) — zig's checked arithmetic emits a if (d == 0) panic guard, so the encoder's CFG walk reaches the idiv on a path where the divisor is PROVABLY zero. Detector fires.
• gcc cwe369_div0: implied=0, path=true — gcc's UB semantics emit no div-by-zero check, so no path implies d == 0. Detector cannot fire.

Conclusion: the binary div0 detector's precision is ZIG-ASSISTED — it relies on the compiler's div-by-zero check to produce the implied-zero path. A gcc/clang "clean" recipe removes both the noise AND this enabling signal, so div0 F1 drops to 0 on gcc. Detecting div0 on un-checked (gcc/clang) code requires a "satisfiable-zero" heuristic (divisor CAN be zero), which trades precision for recall. The two recipes have OPPOSITE strengths: zig enables precise div0, gcc/clang enables clean int-overflow signal-to-noise. The benchmark should therefore score div0 on the zig recipe and int-overflow on the gcc/clang recipe, not conflate them.

int-overflow P2 (SMT sign-mismatch) — iteration 4 (REJECTED, needs taint)

Wired handleIntegerArithmetic to call onBinaryArith(Add/Sub/Mul, isSourceSigned=true) (the observer's existing sign-mismatch check). Measured on the gcc x86-64 recipe: 4 int-overflow findings on EVERY fixture — entry.fini0, entry0, main, and the fixture's vuln. So P2 without a taint filter fires the vuln (1 TP) plus 3 library/ crt/main sites that also appear on clean.elf (FP). The "assume signed" gate is too broad: it flags the glibc crt startup and main's own arithmetic. REVERTED.

NEXT (the real enabler): a TAINT filter — fire the overflow only when an overflowing operand is a function-input (param) register or derives from one, so the library's internal arithmetic is excluded. This is the taint/reachability gate the Workflow-v2 pre-check anticipated.

int-overflow P2 + naive taint gate — iteration 5 (REJECTED, needs taint propagation)

Tried gating the SMT sign-mismatch on "operand is a never-written Register (function input)". Result is wrong in BOTH directions:

• gcc recipe: 0 findings (misses the vuln) — the function input a is stored to a stack slot then re-loaded into a WRITTEN register (mov eax,[var_4h]) before add eax, 0x7fffffff, so the operand is not a "never-written" register.
• zig recipe: 11 findings on EVERY fixture (including clean) — the zig runtime's checked arithmetic is itself on function-input-derived values, so "function input" does not separate the vuln from the runtime.

REVERTED. The taint gate needs (a) proper propagation through Store/Load/Copy (the def-chain, not "never-written"), and (b) a signal MORE SPECIFIC than "function input" — the runtime also consumes the input. This converges on the source-lane taint-track detector's model (untrusted source -> sink), which is the deeper feature the Workflow-v2 pre-check predicted. int-overflow remains F1=0.

null-deref backward NPD P1 — iteration 6 (NOT APPLICABLE, interprocedural)

The cwe476 null-deref is INTERPROCEDURAL: vuln(int* p){ return *p; } derefs the param p (mov eax,[rdi]), and main passes p = 0 on the argc<=1 path. A within-function backward NPD (walk the def-chain from the Load to a Copy-0/ Store-of-0) finds only "function input" in vuln — no null source. So P1 cannot catch cwe476. The null-deref bounded paths are exhausted: P1 not-applicable (interprocedural), P2 forward summary rejected (#12, libc noise). Remaining = interprocedural null-constant propagation (main's p=0 -> vuln's *p), the same cross-function blocker as int-overflow's taint.

use-after-free P1 scoping — onFree hook is dead

SafetyObserver::onFree(ptr, ..., was_already_freed) exists but is DEAD: the P-Code encoder never calls it, and BinaryBBObserver never implements it (like detectUseAfterFreeFromDisasm was). The cwe416 UAF (free(p); return *p) is WITHIN-function, so a P-Code heap model is tractable. Implementation plan (3 parts): (1) encoder handleCall detects the free callee and calls onFree; (2) BinaryBBObserver::onFree tracks freed pointers per function and emits double-free on was_already_freed; (3) encoder handleMemory (Load/Store) checks the address against the freed set and emits use-after-free on a deref-after-free. Part (3) is the benchmark-relevant piece.

use-after-free P1 (P-Code heap model) — RETAINED (iteration 7)

Implemented the 3-part P-Code heap model and it fires with no FP:

1. SafetyObserver::onUseAfterFree hook + BinaryBBObserver::onUseAfterFree (emits binary-use-after-free, FindingKind::UseAfterFree).
2. Encoder handleCall detects the free/cfree/zdlpv/zdapv callee and records the freed pointer. KEY: the free arg is in the arg REGISTER (raw Sleigh RDI=0x38), NOT op.in — the lifter only injects arg prototypes for KNOWN sinks, and free is not one (the Call op carries only the target).
3. Encoder handleMemory (Load/Store) checks the address against the freed set and fires onUseAfterFree on a deref-after-free.

RESULT: benchmark use-after-free F1=1.000 (TP=1, FP=0 — clean + the other 4 fixtures stay 0). Three detectors now score F1=1.000 (oob-access, div-by-zero, use-after-free). 7/7 binary tests, git diff --check clean.

int-overflow P2b (constant-sentinel ADD+INT_MAX) — RETAINED (iteration 8)

The taint-track was blocked by function identity (stripped binaries have no user/library boundary). The winning signal is SPECIFIC, not general: fire the observer's signed-overflow model only on IntAdd with a constant INT_MAX operand — the classic CWE-190 a + INT_MAX deliberate-overflow test. This is specific enough to avoid the zig runtime's x - INT_MIN (abs/overflow handling, SUB) and small-offset bounds checks. Compiler-agnostic (zig AND gcc/clang).

RESULT: benchmark int-overflow F1=1.000 (TP=1, FP=0) on the zig recipe, and gcc recipe cwe190 TP=1 / clean FP=0. FOUR detectors now score F1=1.000 (div-by-zero, int-overflow, oob-access, use-after-free). 7/7 binary tests, git diff --check clean.

null-deref — zig-assisted null-check (iteration 9, REJECTED the deref summary)

Re-attempted the interprocedural null-deref with a "trivial deref wrapper" summary (deref of a pure param, no loop/branch/check). Found the summary mis-designed for the zig recipe: zig's -O0 codegen ADDS a null-check (cmp rcx,0; test al,1; jne panic; call <panic-handler>) before the deref, so the deref is on the NOT-null path and maybeNullDeref cannot see a deref-of-0. The null-deref is therefore ZIG-ASSISTED, exactly like div0: the signal is the compiler's param == 0 check that branches to a panic handler, NOT an un-checked deref. The "trivial deref wrapper" summary (no branch) wrongly excluded the zig null-check branch. Reverted.

FUTURE (the last gap): a "null-check -> panic" detector — fire null-deref on an IntEqual/IntNotEqual( param, 0 ) whose taken branch reaches a panic/abort call (the zig runtime's null-deref handler). This is a new signal (analogous to div0's implied-zero path), not the existing maybeNullDeref. Needs a panic-handler identification step.

Final state

FOUR detectors score F1=1.000 on the benchmark: div-by-zero, int-overflow (constant-sentinel ADD+INT_MAX), oob-access, use-after-free (P-Code heap model). null-deref is the only remaining gap (zig-assisted null-check, needs the null-check->panic detector). All findings + lane infrastructure documented here and in binary-detector-state.md.

null-deref null-check->panic — iteration 10 (needs param-vs-malloc provenance)

The zig panic handler (fcn.01030cc0, a 351-byte noreturn function that formats a panic message and aborts) is the null-deref sink. But a "null-check (cmp x,0) -> panic" signal fires on BOTH the cwe476 param-null-check AND the cwe416 malloc-result-null-check (zig also null-checks malloc results). The benchmark scores cwe416 as UAF, not null-deref, so the signal must distinguish "null-check on a function PARAM (input)" from "null-check on a CALL result (malloc)". That is value provenance — the same taint blocker as int-overflow. This closes the null-deref bounded-path search: the remaining detector needs a param-provenance taint, a research feature beyond the current binary-lane heuristics. 4/5 detectors remain at F1=1.000.