Unit + integration coverage for the session's work: incremental project
graph/index, pcode encoder, unreachable/dead-branch, equiv/cross-TU,
div-by-zero/sign-conversion/int-truncation, use-after-free, quality-precision,
scan-router profile, source TU runner, detector plan, and the eval fixtures.
Phase 5: detect stack buffer overflows in binaries through the P-Code
pipeline, value-aware against recovered buffer capacities.
- ir::pcode::PcodeOp gains in_buffer_sizes (parallel to in): per-pointer-arg
recovered stack-buffer capacity, SSA-only (-1 = unknown).
- ghidra_lifter: inject locked prototypes for known copy/input sinks at their
call-target addresses BEFORE the SSA action pipeline, so parameter recovery
attaches the destination pointer; resolveStackBufferBytes traces the
PTRSUB/PTRADD/INT_ADD spacebase+const def chain to a stack address and reads
the recovered local's type size via getScopeLocal()->findOverlap().
- pcode_encoder: recognize copy/input sinks (unbounded: gets/strcpy/strcat/
sprintf/...; bounded: fgets/read/memcpy/strncpy/snprintf/...) and fire
onBufferCopy with the write length when the dst capacity was recovered.
- BinaryBBObserver::onBufferCopy: ugt(size, cap) bounds check -> OOBAccess
finding (binary-buffer-overflow). Unbounded sinks -> Heuristic; bounded with
provable len>cap -> Proved (checkAndEmit gains a confidence parameter).
- router: SSA rewrites CALL targets to synthesized addresses, so resolve callee
names from the raw stream by target address and carry them to the SSA stream
by call-site instruction address (annotateByTarget / annotateBySite).
- r2_backend: extractCallTargetNames maps stub/func addresses -> normalized
callee names; scan_runner activates the lane for oob/oob-access detectors.
Validated on bench/corpora/ctf-challenges: 3 TPs in libbof_overflow
(gets->32B, strcpy->64B, sprintf->128B), genuine TPs in libcmd_injection
(sprintf->256B) and libvuln_demo (strcpy->16B), zero false positives across
the corpus; safe_version and the bounded __strncpy_chk path are not flagged.
Unit tests cover unbounded/bounded/safe/no-size/non-sink cases.
meson test: 74/74. div-by-zero and null-deref P-Code findings unchanged.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds a second hazard to the P-Code encoder. LOAD/STORE now fire onPointerDerefIr
when the dereferenced address provably folds to 0, backed by a small stack-slot
memory model (address-value -> stored value) so a `store 0,[slot]; load r,[slot];
deref r` chain proves r==0. Gated on a provably-zero address (no path forking
yet) → zero-FP: ordinary stack accesses (sp+const) and heap pointers don't fold
to 0. The value map keys on (space,offset) so sub-register reads alias the
full-register write the lifter emits.
Validated end-to-end (ghidra-enabled) on the CTF corpus: libnull_deref.dylib ->
2 null-deref TPs (sym._null_deref_direct AND sym._null_deref_conditional — the
const-0 pointer flows linearly so the conditional case is caught without path
forking), matching the source detector's 2 proved null-derefs; div-by-zero still
2 on libdiv_by_zero; zero null/div FP across the other corpus dylibs. Unit tests
(test_pcode_encoder): store-0->load->deref fires; ordinary stack-slot deref does
not. Full suite 71 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Wires the whole pipeline together: binary bytes -> raw+SSA lift -> P-Code
encoder -> Z3 -> BinaryBBObserver -> merged finding.
- include/fold/binary/pcode_router.{hpp} + src/binary/pcode_router.cpp:
routeFunctionToFindings() lifts a function both ways (liftRaw + liftSSA),
encodes each into a fresh Z3 context/observer, tags findings with the lift
level (evidence.backend = binary-pcode-raw|ssa), and merges + dedups by
(kind, line, detector) — raw wins on collision (more direct hazard evidence).
- meson: gated `fold-ghidra` static lib (ghidra_lifter + pcode_router) linking
fold_core_dep + ghidra_decompiler_dep (first fold_core <-> Ghidra link), and
the `pcode_scan` smoke driver. Defined after fold_core so both deps are in
scope; built only when -Dghidra=enabled.
- pcode_encoder fix: value map now keys on (space, offset) without size and
coerces on read, so a sub-register divisor read (w9, size 4) sees the
full-register zero write (x9, size 8) the lifter emits for `mov w9,#0`
(ARM64 zero-extend). New unit test locks this aliasing.
Validated end-to-end: pcode_scan on arm64 sym._div_by_zero_direct emits exactly
one finding — `[binary-pcode-raw] division by zero proven by Z3` — with the SSA
stream correctly contributing nothing (it folds x/0 -> 0) and the router
merging. Full suite 71 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
src/symbolic/pcode_encoder.{hpp,cpp}: a register-machine symbolic executor over
fold::ir::pcode (provenance-agnostic — consumes Raw or SSA). Assigns a Z3 BV per
varnode, propagates values through COPY / INT_ADD/SUB/MULT / AND/OR/XOR /
ZEXT/SEXT/SUBPIECE, and fires the existing SafetyObserver::onBinaryArith(Div)
hook for INT_SDIV/UDIV/SREM/UREM so BinaryBBObserver proves the hazard. Lives in
fold_core (no Ghidra dep); it is the real encoder the dead abstract-block path
never was.
MVP precision: the Div hook fires only when the divisor constant-folds to 0
(zero-FP without path forking — a bare symbolic divisor would make SAT(rhs==0)
trivially true and FP on every `a/b`). NEXT: CBRANCH path-forking drops this
gate (catches data-dependent zero divisors); null-deref (LOAD/STORE + stack
memory model, const-0 address gating) and guarded int-overflow follow.
tests/unit/test_pcode_encoder.cpp (no Ghidra/r2): constant-zero divisor and
COPY-chained zero are flagged; non-zero and bare-symbolic divisors are not.
Full suite 71 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
