# 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.