Problem: normalizeClangTuPath, normalizeQuarantinePath and fan-out's
normalizePath were three copies of the same absolute + weakly_canonical
routine. Coverage, worker records and the quarantine file must agree on a
TU's spelling, and three copies can drift apart.
Fix: move the routine to fold/cli/tu_path.hpp as normalizeTuPath and use it
at every site. No behaviour change.
Test: existing test_scan_coverage (path spellings), test_tu_quarantine and
test_subprocess_fanout, updated to the new name. Full suite: 140/140.
Problem: null-deref, div-by-zero and int-overflow re-check a portfolio
verdict on the reporting solver and reconcile the two, but then memoized the
re-check's unsat core (and read its model) from the raw re-check result. A
portfolio SAT that the re-check called UNSAT became unknown, yet its core was
still reused as the assumptions for later queries on the same path. The
disagreement itself was silent: no stat, and the trace showed the portfolio's
verdict.
Fix: all six sites use symbolic::recheckPortfolioVerdict and act only on the
reconciled verdict, so an unknown leaves no core or model behind. The helper
counts SolverStats::portfolio_disagreements (merged, printed, and exported in
the detector profile), and the sites trace
"UNKNOWN (portfolio re-check disagreed)".
Test: test_model_validation "[portfolio]" checks the helper's agreement,
unknown and disagreement cases and the merged counter. Full suite: 140/140.
Problem: isCLibraryFunction accepted any global-scope non-member function,
so a project's `void free(Obj*)` overload was modeled as libc free: calling
it twice was a double free, and reading after it a use-after-free.
Fix: a global function counts only when it is extern "C", in namespace std,
or declared in a system header. extern "C" also covers C translation units,
where external functions have C language linkage.
Test: test_library_callee_identity "[global]" (DoubleFree and UseAfterFree
now 0; were 1 each); test_encoder_callee_names flips the global C++ helper
to not-a-library-callee. Full suite: 140/140.
Problem: with --portfolio the OOB and UAF detectors took the portfolio's
SAT/UNSAT answer as final. The portfolio solves on its own contexts, so the
reporting solver was never checked: OOB read its counterexample from an
unchecked solver (i=0 under `i > 5`), and a SAT the reporting solver would
not reproduce was still emitted. Other detectors already fail closed through
reconcilePortfolioRecheck.
Fix: add symbolic::recheckPortfolioVerdict, which re-checks a decided verdict
on the reporting solver and reconciles the two (disagreement or timeout ->
unknown), and apply it at the four OOB and two UAF portfolio sites. The
now-redundant UNSAT-only artifact re-checks in OOB checkHazard are removed.
Test: test_proved_requires_exact_model "[portfolio]" requires the portfolio
counterexample to satisfy the path (was i=0, now i=6).
Problem: OOBObserver::emit marked every constant-index array OOB as Proved,
even when the path reaching the access was over-approximated (an opaque call
or a truncated loop). The heap and UAF paths already gated on exactEncoding.
Fix: pass exactEncoding(env) into emit and require it alongside a numeral
index before assigning Proved; otherwise the finding is Heuristic.
Test: test_proved_requires_exact_model "[oob]" adds an exact control (stays
Proved) and an opaque-call path (now Heuristic; was Proved).
Two gaps in the loop-exit soundness rule from 6adcc24, both found in
review and reproduced as Proved always-conditions:
- `continue` was not an escape. The walkers drop an arm that ends in
`continue` (it always leaves the iteration), so iterations that took it
were never modeled, yet the unroll still counted as exact and the
loop's variables were not havocked:
for (i = 0; i < 2; i++) { if (y) continue; x++; } if (x == 2)
was "always true" although y != 0 gives x == 0. containsLoopEscape now
treats a continue that targets the loop as an escape (a switch
captures break but not continue; a nested loop captures both).
- Havocking a truncated loop reset scalar variables only. Array element
and member stores from the partial unroll survived:
for (i = 0; i < n && i < 4; i++) buf[i] = 1; if (buf[0] == 1)
was "always true" although n == 0 leaves buf[0] == 0. The unroll now
records the base variables of array/member stores and replaces their
arrays/values with fresh ones of the same sort; a store through a
pointer havocs every tracked heap array (SymbolicEnv::havocHeapArrays)
and marks the env over-approximated. The three walkers share this via
LoopUnrollExits::havoc.
Tests (test_loop_exit_soundness): continue, local-array and heap-pointer
stores are no longer Proved by dead-branch, always-condition or
unreachable; the exact constant-bound loop stays Proved (negative
control). A pointer-mutating call inside the loop (review #9) did not
reproduce for unreachable; its case is kept as a regression guard.
Problem: symbols are 64-bit bitvectors whose low bits carry the source
value, but int-overflow witnesses printed the whole bitvector. For a
32-bit `int a` the report showed a=2147483648 or a=-9223372034707292160,
which are not values of `a` and would make bad fuzz seeds
(tests/fixtures/clones/exact.cpp).
Fix: detect::sourceIntTypesOf() maps the function's integer parameters
and locals to their width and signedness (a name declared with two types
is left out). collectModelBindings() takes that map and prints each bound
symbol truncated to its source width with its signedness
(formatSourceIntValue). int-overflow passes the map for the current
function; other detectors are unchanged.
Test: test_int_overflow "[witness]": every binding for an `int` overflow
lies in int range, and formatSourceIntValue covers sign/width cases.
exact.cpp before: a=2147483648, a=3221225471. After: a=-2147483648,
a=-1073741825, the int values that actually overflow.
Problem: with --portfolio, null-deref, div-by-zero and int-overflow take
the verdict from a separate portfolio solver, then re-check on their own
solver only to obtain a model or unsat core. The re-check's result was
never compared: if it timed out (unknown) or disagreed, the portfolio's
SAT still produced a finding, with no model from the reporting solver.
Fix: symbolic::reconcilePortfolioRecheck() keeps the verdict only when
the re-check reproduces it and otherwise returns unknown. It is applied
at all six re-check sites.
Test: test_model_validation "portfolio verdicts stand only when the
re-check agrees" covers agreement, re-check unknown, and disagreement in
both directions. null_deref, int_overflow, div_by_zero and
source_structure pass.
Problem: SummaryStore keyed summaries by getQualifiedNameAsString (plus
"@file" for internal linkage), which overloads share. When a TU calls a
function whose body lives in another TU, the lookup returns whichever
overload was summarized last. Example: `take(int*, int)` dereferences p,
`take(int*, long)` checks it, and a call `take(q, 1L)` with a null q was
reported as a null-deref because it inherited the other overload's nonnull
precondition. Lookups also used a different spelling (no "@file") than
stores for static functions, so their summaries were never found at call
sites.
Fix: summaryStoreKey()/summaryStoreKeyForCall() return the declaration's
USR (semanticFunctionId: USR, TU-qualified for internal linkage). Every
clang-side store, lookup, dependency edge and staleness check uses it:
summary_encoder, null-deref, div-by-zero, OOB and the summary priming
pipeline, which still selects targets by the call graph's qualified names.
Rust summaries keep their own keys. Now that static callees' summaries
are found, null-deref's summary-precondition path applies the same
DEBUGASSERT and static-parameter-contract filters as its callee-deref
path.
Test: tests/unit/test_summary_key_identity.cpp covers per-overload
summaries, key identity across redeclarations and distinct keys across
namespaces, and the cross-TU overload call. That call reported a false
null-deref before the fix; a control call to the dereferencing overload
still reports one. Tests that hand-built the old keys
(test_symbolic_summary, test_cross_tu_security) now derive them from the
declaration. Full suite: 140/140 (rust_frontend's 500 ms timeout test
flaked once at load average 22 and passed on four reruns).
Problem: a TU the front end could not parse left no trace. ClangTool::run's
status was discarded, TUs with compile errors were analyzed on a partial
AST and counted as done, and the isolated-worker path dropped TUs that
never produced an AST. A scan of only broken files printed no findings and
exited 0, the same as a clean scan. Separately, the scan logger wrote to
stdout, so any warning corrupted a SARIF/JSON report written to stdout.
Fix: every TU now yields an outcome (clean, compile-errors,
analysis-failed); workers carry it on their file_finished record, and the
fan-out parent adds timeout/crash/worker-exit for the TU a worker died on.
tuCoverage() turns the requested file list plus outcomes into a
ScanCoverage (requested TUs with no outcome are frontend-failed). SARIF
gets a run `invocations` entry (executionSuccessful, one
toolExecutionNotification per gap); findings JSON gets an additive
`coverage` object. A scan with any gap, or with nothing analyzed, exits 2
after writing its report. CLI diagnostics now go to stderr, as
docs/internal/cli-philosophy.md principle 12 requires. USAGE.md and
AGENTS.md document the coverage fields and the exit code.
Test: tests/unit/test_scan_coverage.cpp (classification, path spelling,
complete/untracked controls, merge, both writers, and unchanged output
without coverage); test_cli_paths "[coverage]" covers a clean TU (exit 0,
complete) and a TU with a missing include (exit 2, gap in JSON, SARIF on
stdout parseable with executionSuccessful=false). Before: both probe files
exited 0 with no coverage information. Full suite: 139/139.
Problem: docs/research/soundness.md defines `proved` as an exact bounded
model establishing the property, but several detectors assigned Proved
without one: double-free from a heap-model flag, static-ptr-asymmetry from
a cross-function pattern, unused-function and dead-statement from AST
facts, the stdlib copy-overflow check, and the heap use-after-free / OOB
checks from SAT results whose encoding precision was never consulted. A
SAT result over an over-approximated path (an opaque call, an unsupported
node) can be spurious.
Fix: double-free and static-ptr-asymmetry report Heuristic; unused-function
and dead-statement report Syntactic; the stdlib copy check reports
Heuristic. Heap OOB and use-after-free keep Proved only when the path's
SymbolicEnv carries no imprecision tag. So that `malloc(sizeof(T))` paths
stay exact, sizeof/alignof on complete non-VLA types are now encoded as
exact constants (symbolic::typeTraitConstant) instead of an unsupported
node.
Test: tests/unit/test_proved_requires_exact_model.cpp covers each
downgraded detector, a heap UAF on an exact path (stays Proved, control)
and under an opaque call (Heuristic), and typeTraitConstant including the
VLA negative case. Full suite: 138/138.
malloc/free heap modeling (encoder), use-after-free's free/realloc, and
the taint source/sink tables selected a model by the callee's bare
identifier. A project function that merely shares a libc name was
modeled as libc:
namespace mine { void free(void*); }
mine::free(p); ... std::free(p); // double-free "proved", plus
// oob "double free" and a UAF
and `Pool::free(p)` behaved the same way, as did a member function
named `system` as a command-execution sink.
isCLibraryFunction / isCLibraryCallee (encoder_callee_names) accept a
direct callee that is not a class member and is declared at global
scope, in namespace std, or extern "C". The encoder's malloc-family and
free models, use-after-free's free/realloc, and every libc/POSIX taint
entry now require it. Entries that are deliberately method-name
heuristics (get, Query, execute, query, fromJson, readString*, the
request-parameter getters) are marked c_api = false and keep matching
by name as before.
Tests: test_library_callee_identity (namespaced and member `free` are
not double-free/UAF; member `system` is not a sink; libc free twice and
libc system(getenv()) still are), and isCLibraryCallee cases in
test_encoder_callee_names (::free, std::free, mine::free, Pool::free,
a global helper, an indirect call). Full suite 137/137.
The dead-branch, always-condition and unreachable walkers unroll loops
loop_unroll times, following only the path on which the guard holds.
When the guard could also be false (any symbolic bound), that early
exit was dropped, and the loop's assigned variables were havocked only
for loops containing calls. The state after the loop was therefore
"the loop ran exactly loop_unroll times", and conditions on it were
reported as Proved:
int s = 0; for (unsigned i = 0; i < n; ++i) s += 1;
if (s == 0) ... // "dead" proved/exact, "always false" proved
The same held for `s > 100`, while loops, and a `break` out of a
constant loop. On the audit probes this was 7 Proved findings, all
false.
LoopUnrollExits now records whether the unroll saw every way out of
the loop: no iteration could exit early (the guard's false branch was
infeasible), the unroll stopped because the guard became infeasible
rather than because loop_unroll ran out, and the body has no break or
goto that escapes. When any of that fails, the walker havocs the loop's
assigned variables and restores the entry path, as it already did for
opaque loops. A loop the unroll exits exactly (constant bound within
budget) keeps its precise state, so a genuinely dead branch after it
is still Proved.
Loop-bound provenance (--suppress-loop-bound-always-conditions) stays
off by default: it existed to downgrade proofs that leaned on the
unroll bound, and an inexact loop exit now havocs instead of producing
such a proof in the first place.
The duplicated helpers (containsCallExpr, collectAssignedVars,
appendAssignedVars, havocAssignedVars) move from dead_branch.cpp and
always_condition.cpp into detect/loop_havoc so all three walkers share
them; dead_branch.cpp drops under the 800-line soft cap.
Tests: test_loop_exit_soundness covers the symbolic-bound cases for all
three detectors (4 Proved each for dead and always-condition before),
the break escape, the exact-loop negative control, and the extracted
helpers (containsLoopEscape, LoopUnrollExits). Full suite 136/136.
Iteration 3 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
mergeTranslationUnitGraphContributions hard-failed with 'conflicting
semantic-USR function evidence' when the same function USR recurred
across TU contributions with spelling-variant qualified names (libc++
inline-namespace std:: vs std::__1) or an empty body hash (TU-dependent
template instantiation). ProjectCallGraph::addFunction — the exhaustive
fallback builder this merge must mirror — merges duplicates leniently,
so the incremental path could never succeed on real C++ codebases and
every scan silently paid the exhaustive fallback.
Measured (fold self-scan, 8 TUs):
- call-graph phase with --cache-dir: 24.1s median -> 1.7s (93% cut);
exhaustive-fallback warnings eliminated
- project eval wall median: 160.1s -> 92.6s (n=2, partly noise)
Finding fingerprints are exactly preserved (fold 0fec78e5..., yams
247523c5...; churn 0, pairwise Jaccard 1.0, both project evals ok).
Full suite 136/137 (sole failure: pre-existing benchmark_evaluation
fixture-schema issue, unrelated area). Red test added: 'contribution
merge tolerates same-USR spelling variants like the exhaustive
builder' (test_project_index.cpp).
Iteration 1 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md, workflow-driven
measure->select->implement->validate->checkpoint).
Baseline measured (tests/benchmarks/runs/optimization-2026-07-30/):
- fold self-scan median 251.7s, peak RSS 1390.5 MiB; sql-injection
detector 40.37% of analyze share (101.4s median) with 0 Z3 queries
- yams self-scan median 10.7s, peak RSS 489.9 MiB
Implement attempt: shared thread-local scratch Z3 context for
summarizeLeafFunctionSymbolically (stack samples showed Z3 ast_table
init from the ensureSymbolicSummary chain dominating walk time).
REJECTED by the new characterization test: Z3 hash-consing collapses
same-named parameters across functions and summary composition
silently degrades. Reverted; regression test retained plus rationale
comment at the reverted site.
Also documents: SummaryStore::lookupOrCompute returns pointers into
its internal map (invalidated by clear()); open finding on
load-sensitive summary recomputation under CPU saturation.
No production behavior change; fold:symbolic_summary 10/10 green,
focused suites green, git diff --check clean.
ARM NEON reductions (vaddvq_*/vminvq_*/vmaxvq_*) expand to GNU statement
expressions `({ ...; __ret = builtin(x); __ret; })`. The uninit-read walker
flat-traversed the statement expression, flagging the result read `__ret`
before noticing the assignment that writes it inside the same expression.
Track variables assigned within a StmtExpr (TraverseStmtExpr) so the result
read is not a false uninit-read.
Verified: simeon neon.cpp range_neon 2->0, statement-expression repro 1->0,
genuine uninit local still fires; full suite 137/137.
`(d & (d-1)) == 0 ? low & (d-1) : low % d` (simeon sketch_bucket) flagged
`low % d` as division-by-zero, but the guard `(0 & -1) == 0` is TRUE when
d==0, so the `%` arm is unreachable for a zero divisor. Teach
conditionProvesNonZero that `x & (x-1)` clears the lowest set bit (zero iff x
is 0 or a power of two):
* `(x & (x-1)) == 0` false arm -> x != 0
* `(x & (x-1)) != 0` true arm -> x != 0
Also route the same check through analyzeDivCallee so the callsite
precondition for the guarded divisor param is suppressed in the same TU.
Verified: simeon.cpp:48 `proved` finding gone; positive repro 1->0, bare
`a % d` still fires; 59 div-by-zero tests + full suite 137/137.
std::string/std::string_view size()/length() was cached only in the member
cache, which assign() clears. So `char* p = malloc(s.size()+1); ...; p[s.size()]`
encoded the two size() calls as DIFFERENT symbols, letting the solver find a
spurious out-of-bounds (yams object_storage_adapter.cpp dup_cstr, plugin_host_services_shim).
Route zero-arg const size()/length() through the assignment-surviving
string-length cache (string_lengths_), so both calls resolve to one length
symbol: the final write lands exactly at the end (in-bounds), while a genuine
size()+1 write still fires.
Adds positive/negative oob tests; full suite 137/137.
Given the engine can afford days of compute (fuzzing-grade), widen the
solver budgets so hard queries resolve instead of timing out:
- checkAdaptive escalation ceiling raised to 1 hour per query (was 8x base)
- budget_seconds 7200 -> 604800 (7 days)
- per_tu_timeout 900 -> 86400 (24h)
A single hard query getting up to an hour of escalating compute is cheap
relative to a lost vulnerability.
The 1800s solver budget, 6s per-query timeout, and 300s per-TU watchdog were
too tight for large security scans (e.g. 780-file yams), causing Z3 "unknown"
results and preempted TUs. Raise to 7200s budget, 30s per-query, and 900s
per-TU so slow-but-productive TUs finish and complex queries resolve.
std::basic_string / std::basic_string_view methods (substr/append/insert/...)
do size()-pos and pos+count arithmetic that is bounded by the container size
invariant, so an unbounded pos/length at a call site is a logic contract, not
signed-overflow UB. analyzeOverflowCallee now skips these, removing the
chromium file_path.cc substr/append FPs (6 signed findings -> 0) while
preserving the 10 genuine unsigned-wrap findings.
Adds positive tests (substr/append call sites are not flagged) and a clean
negative (free-function arithmetic is still flagged).
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.
- int-overflow: unsigned wrap is defined, not UB — split to
fold.unsigned-wrap so signed-UB findings aren't drowned; on by
default (--report-unsigned-wrap=false opts out)
- use-after-free: model return/throw as path-terminating so
`delete p; return;` in an error branch can't poison the fall-through
- oob-access: real sizeof for complete structs (was 1); recognize
std::min/clamp/modulo index bounds
- memory-leak: static-storage singletons + return-to-caller are
caller-owned, not leaks
YAMS scan: UAF 4→0, struct-OOB ~10→0, singleton-leak ~15→0,
min/modulo-bound OOB →0. 137/137 tests pass.
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>
