Completes the symbolic gadget solver. When the binary has no "/bin/sh" string,
the planner now plants one via a write-what-where gadget into scratch memory and
points execve's arg0 at it; conditional gadgets are excluded from chains (prefer
unconditional, never assume a branch).
- r2_backend: writableSectionAddr returns a writable (.bss/.data preferred)
scratch address via iSj.
- rop_chain: synthesizeChain refactored around a reusable `satisfy` register-
setup helper; for execve with no /bin/sh it finds a mem-write gadget
(addr=reg, value=reg, ret-terminated; findWriteGadget), sets the address reg to
scratch and the value reg to the "/bin/sh\0" qword, lands on the write gadget,
then builds execve with arg0 = scratch. Caveat records the planted string.
- binary_pcode_scan: passes the writable scratch address into the planner.
Conditional gadgets are skipped in pickPopGadget/findWriteGadget (term must be
Ret, not Cond) — safe by construction.
Validated: unit test_rop_chain — write-what-where plants /bin/sh and uses the
write gadget (21 assertions); execve/win/multi-pop cases unchanged. Corpus BOF
parity (3/1/1); meson test 78/78. Part 3 (3a effects + 3b planner + 3c
write-what-where) complete.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace the text-heuristic chain builder with a planner over per-gadget symbolic
effects (3a). Because effects are concrete classifications (stack-slot@offset /
const / reg / sp-relative + sp_delta), the payload layout is deterministic stack
arithmetic — each chain step carries its exact byte offset relative to the
overwritten return address.
- ghidra_lifter: liftRegisterInfo resolves the arch's register file by name from
the SLEIGH spec (getAllRegisters) — used to build the gadget RegModel
arch-correctly (no hardcoded offsets).
- r2_backend: extractRopGadgets returns each gadget's byte length and (opt-in)
its bytes, so gadgets can be re-lifted; RopGadgetRaw struct.
- binary_pcode_scan: discoverGadgetEffects lifts each gadget (liftRaw) and runs
analyzeGadgetEffect; buildRegModel maps SLEIGH names → the solver model;
attachExploitPrimitives now feeds effects + win targets + /bin/sh to the planner.
- rop_chain: synthesizeChain consumes GadgetEffects — greedily satisfies each
goal register with a ret-terminated pop gadget (multi-pop gadgets fill several
at once; clobber-aware), threads sp_delta to place values at exact payload
offsets, and lands on a win function or syscall gadget. Auto target (win else
execve). Conditional gadgets are excluded (prefer unconditional); ChainStep
gains stack_offset, serialized in JSON (round-trip) + SARIF.
Validated: libbof_overflow chain is solver-produced (target + offsets); unit
test_rop_chain — win+arg, execve with 4 pops + syscall at correct offsets,
multi-pop coverage, no-target → none (17 assertions); test_gadget_semantics
(22). Corpus BOF parity (3/1/1); meson test 78/78.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
analyzeGadgetEffect symbolically executes one gadget's raw P-Code (reusing the
pcode_encoder register-machine modeling) and reports a context-free transfer
function: each changed register's final source (stack-slot@offset / const /
register / sp-relative), the sp delta, memory writes, and the terminator. Z3 is
used only inside the executor to fold/identify sources — GadgetEffect holds no
z3::expr, so it crosses the fold_core/fold_ghidra boundary cleanly and the
analyzer is unit-testable on synthetic P-Code.
Inputs are seeded as recognizable Z3 consts (in_<off> registers, stk_<k> stack
slots loaded relative to the initial SP); classification simplifies each final
value and matches it back. Register offsets come from a GadgetRegModel resolved
by name at lift time (no hardcoded offsets in the analyzer).
This is the foundation for the Z3 chain planner (3b); not yet wired into chains,
so no finding behavior changes. Design references (not deps): Triton's
per-instruction symbolic state, angrop/ropper gadget controllability.
Unit: test_gadget_semantics — pop rdi;ret → rdi=stack[0], sp_delta 16; mov
rax,0x3b;syscall → rax=const, Syscall; pop rsi/pop rdx → stack[0]/stack[8],
sp_delta 24; mov [rdi],rsi → write-what-where reg→reg; bare ret → sp_delta 8
(22 assertions). meson test 78/78.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Propagate "writes-unbounded into pointer-param k" across call hops so a buffer
passed through a wrapper (2+ levels) is still flagged — no third-party call
graph needed; the raw P-Code stream already gives resolved call edges.
- pcode_summary: PointerWriteSummary gains forwarding edges — a Call that passes
one of the function's own pure-input pointer params straight through to a
callee argument (my_param → callee:arg), detected via in_def + paramIndexOf.
Forwards are computed regardless of the loop/size-bound gates (a non-looping
wrapper still forwards).
- pcode_router: expose annotateCallTargets(ssa, raw, names) — factor the
raw→site→SSA name correlation so the summary pre-pass can resolve callee names
for forwarding edges.
- binary_pcode_scan: the pre-pass now annotates each function's SSA call targets
(via a raw lift) before summarizing, collects direct + forwarding summaries,
then runs a worklist fixpoint: a function forwarding a pure-param pointer to an
unbounded-writer parameter becomes an unbounded writer on that param. The
closure feeds both the interprocedural detector and the write-loop prototype
set (so multi-hop callers recover the buffer arg).
Validated: baby_bof (AArch64 + x86-64) still fires; corpus BOF counts unchanged
(3/1/1); the x86-64 static stays at 1 finding (the transitive closure adds no
FP). Unit: test_pcode_summary +forwarding cases (14 assertions). meson test 77/77.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Unlocks the x86 family end-to-end and makes the write-loop detector precise
enough for statically-linked binaries.
x86 SLEIGH:
- Vendor Ghidra's x86 language specs (specs/x86, x86:LE:64:default + :32:default);
add x86-64/x86 .sla build targets. archSpecFor maps x86/64 + x86/32.
- ghidra_lifter: set the x86-64 decode context (longMode/addrsize/opsize) in the
raw path, and bound decompiler flow at the function end (0xC3 tail fill) so
variable-length x86 does not run away into zero padding.
Precise SSA def-use (benefits all arches):
- ir::pcode::PcodeOp gains in_def (defining-op index per input); the SSA lifter
records real def-use. summarizePointerWrites now resolves the store-address
base via def-use instead of a last-write heuristic — essential on x86 where
arg registers are reused as scratch (RAX) and sub-registers are written (SIL).
- paramIndexOf is arch-aware (AArch64 x0–x7; SysV x86-64 RDI/RSI/RDX/RCX/R8/R9).
Precision (the key fix at scale):
- A copy bounded by a size *parameter* (memcpy-like `for i<n`) is suppressed:
if the loop index is `<`-compared against a pure parameter input, the function
is size-bounded and not flagged. baby_bof's decode_base64 bounds on
strlen(input) (a computed value, not a param) so it still fires. This cut a
statically-linked x86-64 binary from 101 findings (≈100 glibc/libstdc++ FPs)
to 1 — the real decode_base64 → 264-byte overflow.
Perf + reach:
- Cache the pre-pass SSA lift and reuse it in the main pass (re-lifting only the
few callers of a write-loop callee that need the injected prototype).
- Give whole-binary r2 analysis a generous timeout (FOLD_R2_ANALYSIS_TIMEOUT_MS,
default 120s) so large static binaries actually analyze (the 3s per-command
watchdog left them with an empty function list).
Validated: decode_base64 overflow fires on x86-64 (index_amd64.cgi) and AArch64
(index_nocanary.cgi); AArch64 corpus BOF counts unchanged (3/1/1); x86-64 static
FP 101→1. Unit: test_pcode_summary +x86-64 case (9 assertions). meson test 77/77.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Turn a detected overflow + gadget inventory into a candidate ROP chain
scaffold (auto target) attached to the finding.
- rop_chain (pure, fold::binary, unit-tested): synthesizeChain auto-selects a
target — a recovered "win" function (system/execve/puts/printf), else an
execve("/bin/sh") syscall chain assembled from syscall + register-control
gadgets (x0/x1/x2/x8 on AArch64, rdi/rsi/rdx/rax on x86-64). Emits ordered
pad/gadget/value/target steps + explicit caveats (PIE/ASLR base, canary, and
that padding_len is the buffer capacity — the exact saved-return-address
offset is target-frame-dependent and must be verified).
- ghidra_lifter: expose each pointer arg's recovered stack-frame offset
(in_buffer_offsets) alongside its size; signed-offset helper. (Exact RA-slot
recovery is left for future work — the saved return address for these
overflows lives in the caller's frame, which a single-function lift can't see;
honest caveats cover this rather than emit a wrong padding.)
- r2_backend: findStringAddress ("/bin/sh" via r2 /j) to seed execve chains.
- report: ExploitContext gains an optional RopChainInfo (padding_len, target,
steps, caveats); serialized in JSON (write + read round-trip) and SARIF.
- binary_pcode_scan: attachExploitPrimitives now also synthesizes a chain per
buffer-overflow finding from the gadget inventory + recovered capacity.
Validated: baby_bof's decode_base64 overflow carries a chain (target win:printf,
padding 256, steps + caveats). Unit: test_rop_chain (17 assertions). Corpus BOF
counts unchanged; meson test 77/77.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Detect custom (non-libc) routines that fill a caller's fixed-size stack
buffer in an unbounded loop — the bug class fold previously missed because
the destination array decays to a pointer across the call boundary.
- pcode_summary (pure, fold::symbolic, unit-tested): summarizePointerWrites
flags a pointer parameter the function writes via a loop-carried index.
Robust over flattened SSA: base must be a *pure-input* param register (never
reassigned as scratch), index must be non-constant, and the function must
contain a loop (MultiEqual).
- ghidra_lifter: generalize prototype injection — besides known sinks, accept
extra_pointer_protos so a custom write-loop callee gets a pointer prototype
at its call sites, letting the decompiler recover the caller's args and the
destination buffer size (the key enabler).
- binary_pcode_scan: two-pass — pass 1 summarizes every function and collects
write-loop callees + their prototypes; the main pass injects those protos and
reports an overflow at any call passing a recovered fixed-size stack buffer to
a write-loop parameter (Heuristic). Call-site guard: suppress when another arg
is a constant >= the capacity (a size was passed → bounded copy).
- router: detectInterprocBufferWrites emits the finding from the annotated SSA
function (call_target + in_buffer_sizes), with ExploitContext populated.
Validated: dist-baby_bof/index_nocanary.cgi now reports the decode_base64 →
256-byte `decoded` overflow in validate_auth (the SOLVE.md "Fold Gap"); zero
new FP across bench/corpora/ctf-challenges; div/null/sink-BOF unchanged.
Unit: test_pcode_summary (7 assertions). meson test 76/76.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Turn a detected binary stack-overflow into actionable exploit material:
each buffer-overflow finding now carries candidate exploitation primitives
discovered from the same binary.
- rop_gadgets module (fold::binary, r2-gated): classifyGadgets() is a pure,
unit-tested classifier over (addr, opcode-text) gadget pairs into reg-control
/ syscall / stack-pivot / control-flow classes, arch-aware (AArch64 + x86-64);
discoverExploitPrimitives() enumerates via r2 /Rj, keeps top-N per class, and
adds "win" targets (jumpable high-value func/stub addresses — system/execve/
puts/printf/... — resolved by name via extractCallTargetNames).
- r2_backend: extractRopGadgets wraps r2 /Rj (flattened opcode text), bounded by
search.maxhits to keep large static binaries fast (~0.5s on a 900KB binary).
- report: ExploitContext gains a GadgetRef list; BinaryBBObserver::onBufferCopy
fills input_channel (the sink) + buffer_offset (recovered capacity) +
controlled_value; scanBinaryWithPcode attaches the gadget inventory once when
any binary-buffer-overflow finding exists (no cost on clean binaries, graceful
if r2 is absent). Serialized in JSON (write + read round-trip) and SARIF.
Scope: supply classified primitives, not auto-assembled chains; attached only
to buffer-overflow findings (no standalone subcommand). Opt-in security tooling
for authorized CTF/pentest use.
Validated: libbof_overflow BOF findings now carry exploit_context.gadgets
(reg-control x0-setup sequences, stack-pivots, printf win target) +
input_channel/buffer_offset. Unit: test_rop_gadgets (8 cases). meson test 75/75.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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>
Follow-up to 3fa6d0f56 (dead-encoder removal): test_binary_bb_observer.cpp had
a stale `#include "fold/symbolic/binary_bb_encoder.hpp"` and three TEST_CASEs
exercising the deleted encodeBinaryBBs. The earlier commit's targeted build did
not compile this test, so the break only surfaced in the full suite. Remove the
stale include and the obsolete encodeBinaryBBs cases; the direct
BinaryBBObserver hook tests (null-deref / div-by-zero / overflow) remain and
pass. Full suite 71 Ok / 0 Fail / 1 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>
Abstract-block mode fired one over-approximate onBinaryArith per block with
fresh unconstrained operands, so it proved nothing for div-by-zero / null-deref
(0 binary findings on libdiv_by_zero / libnull_deref). A full per-instruction
symbolic encoder with path modeling is the eventual fix, but on symbolic args
an unconstrained overflow/aliasing check is trivially SAT and would fire on
every add/sub/mul (the FP blowup) — so this slice lands the sound, zero-FP
subset: constant-zero propagation.
scanInstructionsForConstHazards (pure, unit-tested): a per-function state
machine tracking which registers / stack slots provably hold 0.
mov r,0 | mov r,wzr | str wzr,[slot] | ldr r,[zeroed-slot] -> r/slot is 0
sdiv/udiv d,a,b with b==0 -> div by zero
ldr/str through a zero base register [x0] -> null deref
Tracking resets at every branch / call / ret, so it never reasons across an
unmodeled path — no false positives, at the cost of missing path-dependent
zeros (div_by_zero_variable, null_deref_conditional remain FN: those need
branch modeling, deferred).
Both structural disasm passes (this + UAF) now share one per-function pdfj
sweep via disasmFindingsInSession; const-hazard scanning runs default-on
alongside the import/string detectors and under --detectors
security/div-by-zero/null-deref. Findings carry Heuristic confidence.
Validated on the CTF corpus: +3 TP — div_by_zero_direct, mod_by_zero
(CWE-369), null_deref_direct (CWE-476), all previously FN in binary mode —
with zero new findings across the other 8 dylibs. 6 r2-free unit tests
(test_binary_const_hazards) cover literal-zero divisor, slot-propagated null
deref, non-zero/unknown divisors, branch-reset, and non-zero pointer
negatives. 70 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Binary mode had no UAF/double-free detection. In abstract-block mode the Z3
encoder gives every call argument a fresh, unconstrained constant, so an
aliasing check (freed_ptr == deref_ptr) is trivially SAT for unrelated
pointers — it would fire on every post-free deref. A Z3-proven aliasing UAF
is therefore not viable until per-instruction value flow lands.
Instead detect it structurally over r2 per-instruction disassembly, keyed on
the *stack slot* a heap pointer lives in (r2 names it, e.g. `[ptr]`/`[dest]`)
— a reliable identity within one function, no aliasing needed:
scanInstructionsForUaf (pure, unit-tested): a per-function state machine.
ldr <reg>,[slot] -> reg sources slot
bl free -> slot dangling (double free if already dangling)
bl <other> -> use-after-free if the freed slot's pointer is the arg
str <alloc>,[slot]-> slot revived (free+realloc+free is legitimate)
detectUseAfterFreeFromDisasm / uafFindingsInSession: r2 wrapper, run from
R2Backend::runDetectors on the shared session (no extra `aaa`), default-on
alongside the import/string detectors and under --detectors
security/use-after-free/double-free. Findings carry Heuristic confidence.
Cost is bounded: skip entirely when the binary imports no free/delete (instant
on the common case) and cap the per-function pdfj sweep at 4000 functions.
Validated on bench/corpora/ctf-challenges/libuaf_doublefree.dylib: +3 TP
(double_free_bug CWE-415, use_after_free_bug + use_global_after_free CWE-416 —
all previously FN in binary mode), zero new findings across the other 9 corpus
dylibs. 5 r2-free unit tests (test_binary_uaf) cover double-free, UAF,
clean-free, free+realloc+free, and cross-slot negatives. 69 Ok / 0 Fail /
1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`if ((p != 0) && (p->m))` and `if (p == 0 || p->m)` false-positived: the
walker's encodeConditionWithShortCircuit added the LHS to the Z3 solver for
the RHS encode but never updated the env's non-null marks — and the deref
gate checks `env.isDefinitelyNonNull`, not the solver. So only a fragile
same-line text heuristic (sourceLineShortCircuitProvesNonNull) suppressed the
canonical `p && p->m`; parenthesized / `!=0` forms slipped through.
Fix: in the &&/|| short-circuit handling, extract the LHS null-check
(extractNullCheckedVar) and mark its pointer definitely-non-null for the RHS
encode only, then clear it — short-circuit guarantees the LHS holds when the
RHS runs, and clearing prevents the fact leaking into the else-arm (where the
pointer may be null). Path-sensitive, shape-independent, and the bitwise `&`
case stays flagged (both operands really evaluate).
Drift gate: no per-detector change (null-deref 0.792/0.494/0.609 held) — the
fix removes a real FP class without moving the capped-corpus numbers and is
more robust than the text heuristic it supersedes.
Tests: 3 cases in test_null_deref (parenthesized && safe, || safe, bitwise &
still flagged).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Extend ir::Loop classification: a monotone single-induction-variable for-loop
with a symbolic bound (e.g. `for (i=0; i<n; ++i)`) is now Affine (was General).
The walker summarizes Affine loops like Counted ones — bind the induction
variable to a fresh symbolic, assert its start bound plus the loop condition
(encoded to a Z3 bool) as path constraints, walk the body once — exposing
high-index OOB that bounded unroll misses. Findings are over-approximations
(LoopHavoc/heuristic), never proved.
Net effect on the gate: oob recall 0.531 -> 0.559, F1 0.637 -> 0.652 (precision
dips 0.796 -> 0.782) — a contract-sanctioned over-approximation tradeoff.
Also regenerate bench/fp-baseline.json deterministically from a clean run: the
prior committed oob numbers (0.574) were not reproducible (transient warm-state
artifact); fresh runs are now bit-identical, so the gate is reliable.
Tests: test_ir_loop (affine classification), test_loop_summary (symbolic-bound
OOB exposed, not proved). Suite green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
For a counted loop whose trip count exceeds the unroll bound, bind the
induction variable to its full closed-form range (asserted as a Z3 path
constraint, not just interval metadata) and walk the body once, instead of
unrolling loop_unroll times. This fires each in-body sink against all
iterations at once: it exposes high-index OOB that bounded unroll misses
(oob recall 0.531 -> 0.574, F1 0.637 -> 0.658 on the gate) and collapses
per-iteration queries to one. Findings from the summarized walk are
over-approximations and are tagged LoopHavoc (heuristic) confidence, never
proved. General/while(1) loops keep the bounded-unroll fallback.
Per the precision contract (loop-summarization-research.md), this is a
recall-improving over-approximation that may add bounded, tagged FPs. The
drift gate is updated to match: it now fails on recall- or F1-drop beyond
tolerance (the regressions it was built for) and allows precision dips that
come with recall gains; the committed baseline is regenerated to the B2
numbers.
Tests: test_loop_summary (high-index OOB found + not proved; in-bounds loop
clean). Suite 68/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Foundation for core loop summarization (Workstream B). Adds a clang-free
ir::Loop / InductionVar / LoopKind (Counted | Affine | General) mirroring the
M30 ir::Expr pattern (Symbol-keyed, opaque frontend handle, lowering in
src/symbolic/ir_loop_clang.cpp).
buildLoopFromClang classifies counted `for` loops (constant init/stride/bound,
ascending or descending) into a Counted loop with a known trip count; affine
and unrecognized shapes (while(1) scanners, data-dependent bounds) stay
General and will use the bounded-unroll fallback. The symbolic core will
consume ir::Loop instead of clang::ForStmt so summarization is written once
and reused by the rust/binary frontends.
Tests: test_ir_loop (counted asc/strided/desc trip counts; while(1) and
data-dependent bound -> General). Suite 67/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Enumeration: replace the hand-rolled top-level `tu->decls()` walks (TU
security prefilter + every interprocedural pre-pass/cross-TU primer in
div-by-zero/int-overflow/null-deref/oob) with a shared RAV-based
`fold::detect::forEachFunctionWithBody`, so functions nested in namespaces
and classes are analyzed. Fixes 0-findings on namespaced C++ (dbench CTF).
TU prefilter: extracted to fold/cli/tu_security_prefilter; flags unsigned
-/* wraps so int-overflow candidates in size arithmetic are not skipped.
Timeout robustness: cooperative per-TU walk deadline (WalkOptions) checked
in the walk/unrollLoop/CFG-block checkpoints and the BatchSafetyObserver
flush loop, plus a non-progress unroll fixpoint — slow TUs degrade with
partial findings instead of being SIGALRM-quarantined.
OOB precheck: treat `*(p+i)` and indirect callees as candidates.
null-deref drift fix: remove the unsound `priorFunctionTextProvesNonNull`
source-text heuristic (added in 331a68467) that treated a textual `p!=0`
before a deref as proof of non-null, silently suppressing real null-derefs
(CWE-476 F1 0.485 -> 0.583, recall 0.379 -> 0.517).
Tests: test_function_enumeration, test_tu_security_prefilter, namespaced
cross-TU int-overflow regression. Full suite green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- Verified seedInterproceduralContext() pipeline: SecurityWalker calls it
before TraverseDecl, OOBObserver scans all call sites for ConstantArrayType
- OOB observer consumes param_buffer_sizes_ for ParmVarDecl base variables
- Test added for interprocedural buffer-bound detection
- encoder.cpp: extract VarDecl from ArraySubscriptExpr base when
trackedArrayVar returns null (covers ParmVarDecls like 'output')
- test_oob_access.cpp: test interprocedural buffer propagation
(decode_base64 receiving decoded[256] via pointer parameter)
- Root cause: validate_auth is summarized, preventing inline walk.
Mitigation tracked in docs/internal/interprocedural-notes.md
- SizeInfo struct: buffer_name, capacity, index_expr for OOB findings
- path_trace: vector of branch/call events from SafetyObserver
- counterexample: Z3 model key=value pairs for SAT findings
- variable_name, sink_function: named context for LLM steering
- Serialized in FindingEvidence + SARIF properties
- BinaryBBObserver extends SafetyObserver for binary BB analysis
- Detects null-deref, div-by-zero, int-overflow via Z3 on binary paths
- Wired into BinaryDetectorRunner in scan pipeline
- SafetyObserver subclass for binary basic block analysis
- Detects null-deref, div-by-zero, int-overflow on binary paths
- Wired into scan pipeline via BinaryDetectorRunner
- Binary Z3 findings flow through standard SARIF/JSON output
- Expected: +6 Z3-proved findings on CTF corpus
- Language enum: Unknown, Rust, Cpp, Swift on RustExprNode
- 4 new Clang node kinds: ThrowExpr, CXXConstructExpr, LambdaExpr, StmtExpr
- Updated json_keys namespace with new constants
- 42 roundtrip test assertions pass
- All 3 frontends now share the same IR representation
- SymbolicSummaryCache: per-function BV-64 cache to avoid re-encoding
- Language-agnostic observer overloads for Rust/Swift backends
- Abstract-interpretation pre-pass for Rust integer range filtering
- 3 new unit tests, 63/63 pass
- Store harness_file in binary fuzz predictions to fix prep↔run mismatch
- Resolve relative -I flags against compile DB directory
- Add caller_unsafe/is_param_sourced fields to fold-rust NDJSON
- Allow empty target_sources in fuzz-run for dlopen harnesses
- Recursive IR encoder descent for nested hazards
