Validating the solver end-to-end on the x86-64 static index_amd64.cgi surfaced
and fixed several issues; it now correctly targets execve on a real binary.
- r2_backend: ROP gadget searches (`/R...`) on large/static binaries exceeded the
3s per-command watchdog and were killed → empty gadget set. Give `/R` searches
the generous analysis timeout, and run `search.maxhits` + the search as ONE
command (under the CLI fallback each command is a separate r2 process, so a
prior `e search.maxhits` would not persist). extractRopGadgets gains an optional
disassembly `filter` (e.g. "syscall"/"svc").
- gadget_semantics: GadgetEffect.has_syscall — a `syscall; ret` gadget ends in
`ret` (term=Ret) with the syscall mid-gadget, so term alone missed it.
- discoverGadgetEffects: besides the by-address sweep, run targeted filtered
sweeps for syscall and each argument register — those gadgets live in libc at
high addresses a by-address cap would miss; dedup by address.
- rop_chain: target priority is now shell-win (system/exec*) → execve syscall
chain → leak-win (puts/printf) — a leak must not be preferred over a shell.
`satisfy` is transactional (rolls back partial attempts so a failed register
setup leaves no litter in the chain). findSyscallGadget uses has_syscall.
Validated: index_amd64.cgi (x86-64 static) now reports the decode_base64 overflow
with a chain targeting execve and landing on a real syscall gadget; effects=2157
(417 syscall) discovered. When clean pop rdi/rsi/rdx/rax / "/bin/sh" are absent
(as here) it honestly emits the syscall endpoint + "incomplete" caveats rather
than a fabricated chain. Corpus BOF parity (3/1/1); meson test 78/78.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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>
The base64-blob hardcoded-string heuristic fired on identifier-shaped strings
that aren't secrets. Two guards (extractHardcodedStrings +
detectHardcodedStringsFromTree) now:
- require a real base64 structural char (+ / =) — C++ mangled symbols and
plain alphabets lack one, while base64 of binary data has them; and
- skip the base64 alphabet table itself (ABC..xyz0-9+/), a codec constant
embedded in any binary with base64 code.
Validated on a real arm64 pwn binary (dist-baby_bof/index_nocanary.cgi):
base64-blob findings 5 -> 0. Genuine secrets unaffected — libcmd_injection.dylib
still reports supersecret123 and sk-1234567890abcdef. Full suite 71/0/1.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Completes the binary_bb_encoder deletion (3fa6d0f56) whose scan_runner include
and src/symbolic/meson.build entry were not captured in that commit — HEAD
referenced the deleted source. Also records build-config changes already in use:
- third_party/ghidra-decompiler/meson.build: link-only zlib (cpp.find_library)
to avoid the macOS SDK include path shadowing libc++ <cstdio>/<cstdlib>.
- meson.build/meson_options.txt: reserve optional analysis-lane feature names
(retdec/remill/souffle/phasar/crab) with vendor-manifest-only stubs; only
ghidra is wired.
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>
The abstract-block Z3 encoder was unreachable — serializeBinaryIR never emitted
the BasicBlock/CallSite nodes its `encodable` filter required, so it produced 0
findings, and its scan_runner call site was replaced by the P-Code pipeline in
the prior commit. Remove src/symbolic/binary_bb_encoder.{cpp,hpp}, the
meson source entry, and the stray include in scan_runner. No behavior change
(the code was already dead); both build configs stay green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The Ghidra P-Code pipeline now runs inside real `fold scan --input-type binary`.
- Decoupling hook (fold_core, no Ghidra dep): include/fold/binary/pcode_hook.{hpp}
+ src/binary/pcode_hook.cpp hold a settable PcodeScanHook. scan_runner calls
it when set + a security/div/null/overflow detector is requested, merging the
results and deduping against the structural-pass findings by
(kind, function, line) — additive, no double-report. This replaces the dead
abstract-block encoder block (the `encodable` filter that was always empty).
- Registration (gated): fold_ghidra exposes registerPcodeScanHook() which sets
the hook to scanBinaryWithPcode; the `fold` binary calls it at startup under
FOLD_HAVE_GHIDRA and links fold_ghidra. fold_core has no link dependency on
the Ghidra backend — so the ~30 test executables (which link only fold_core)
build without it. This fixes the link failure a direct call would cause.
Validated both build configs:
- -Dghidra=enabled: fold scan on libdiv_by_zero.dylib -> 2 div-by-zero (pcode +
slice-4 deduped to 2, not 4); full suite 71 Ok / 0 Fail / 1 timeout.
- -Dghidra=disabled (default): fold_core + all test exes link without
fold_ghidra; hook stays null -> r2-disasm structural passes own the binary
scan; full suite 71 Ok / 0 Fail / 1 timeout.
The former abstract encoder src/symbolic/binary_bb_encoder.cpp is now dead (no
caller) and removed in a follow-up. Remaining: encoder increments (path-forking,
null-deref, overflow) for the corpus parity gains beyond div-by-zero.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Drives the dual-stream router over a real binary end-to-end.
- r2_backend: detectBinaryArch() (iIj) + extractFunctionBytes() (aflj + p8,
skipping import thunks) — r2 supplies arch + per-function bytes; the Ghidra
lifter consumes them.
- binary_pcode_scan.cpp (fold-ghidra lib): scanBinaryWithPcode() maps the
r2 arch to a vendored SLEIGH spec (arm64-LE -> AARCH64:LE:64:v8A today;
unknown arch -> {} so the caller falls back to the r2-disasm passes),
enumerates functions, routes each through both lift streams, and merges +
dedups across functions. max_functions caps the sweep (robustness).
- meson: -DFOLD_GHIDRA_SPECS_DIR baked to the vendored specs path so the lifter
locates .ldefs/.sla at runtime; binary_pcode_scan added to fold-ghidra; the
pcode_scan driver gains a whole-binary `pcode_scan <binary>` mode.
Validated on the CTF corpus: libdiv_by_zero.dylib -> exactly 2 div-by-zero
(div_by_zero_direct + mod_by_zero, correctly attributed; div_by_zero_variable
abstains pending path-forking), and 0 on the other 9 dylibs. This reaches
parity with the shipped slice-4 div-by-zero TPs through the proper Z3/P-Code
pipeline. Next (Phase 4 part 2): wire into scan_runner additively (dedup the
div-by-zero overlap with the structural passes), then the encoder increments
(path-forking, null-deref, overflow) for the remaining corpus gains.
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>
Phase 2 of the Ghidra P-Code binary frontend. Adds the frontend-agnostic
P-Code IR and a dual-mode lifter, validated end-to-end.
- include/fold/ir/pcode.hpp: the ~25-op core P-Code IR (Op/Space/Varnode/
PcodeOp/Function), no Ghidra/clang types (M30 invariant). Function carries a
Source tag (Raw|SSA) so findings record provenance.
- include/fold/binary/ghidra_lifter.hpp + src/binary/ghidra_lifter.cpp
(Ghidra types confined): a buffer LoadImage (no BFD) + two entry points
producing the same ir::pcode::Function:
* liftRaw — Sleigh::oneInstruction, per-instruction RAW P-Code;
* liftSSA — SleighArchitecture + Funcdata + action pipeline, SSA high
P-Code (needs CapabilityPoint::initializeAll + whole-archive link).
Both serialized under one mutex (decompiler global state).
- meson: libghidra_decompiler gains the arch/loader infra (sleigh_arch,
inject_sleigh, loadimage_xml, xml_arch, raw_arch); dep switched to
link_whole so capability self-registration constructors run; pcode_lift
smoke driver added (built at fold's std, links the c++11 lib).
Empirical validation on arm64 sym._div_by_zero_direct confirms the dual-path
rationale: RAW preserves `(w9)=COPY const 0` + `INT_SDIV(w8,w9)` (the hazard),
while SSA folds it to `COPY const 0` (ARM64 sdiv-by-0 returns 0; Ghidra's
optimizer constant-folds x/0 -> 0). The two levels are complementary streams
into the Z3 core (next phases): raw for div/overflow/null-deref, SSA for
UAF/dataflow.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds a -Dghidra feature option (default disabled while the encoder is under
construction; enable with -Dghidra=enabled) and third_party/ghidra-decompiler/
meson.build that:
- builds libghidra_decompiler.a from the CORE+DECCORE+SLEIGH object sets
(80 files; cpp_std=c++11, warnings/werror disabled — vendored third-party);
- builds the ghidra_sleigh spec compiler and runs it per-arch to emit .sla
into the build dir (single-file form; source tree stays clean, .sla are
build artifacts);
- builds tools/pcode_dump (custom LoadImage, no BFD).
fold_core does not link it yet (the lifter/encoder glue is Phase 2-3); enabling
ghidra only adds these targets, leaving the normal build untouched.
Validated end-to-end through meson: ninja builds the lib + .sla + pcode_dump,
and the meson-built pcode_dump lifts arm64 sym._div_by_zero_direct to
INT_SDIV(w8,w9) with w9=COPY(const 0) — identical to the hand-build.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Foundation for replacing fold's dead/abstract binary encoder with a real
SSA P-Code frontend. Verified root-cause gap: serializeBinaryIR() emits only
data-discovery nodes (sections/strings/imports/exports); the control-flow
BinaryExprKind values (BasicBlock/CallSite/...) are never constructed, so the
Z3-BB encoder's encodable filter is always empty and encodeBinaryBBs never
runs — hence 0 binary Z3 findings. The P-Code pipeline supersedes that path.
Phase 0 — docs/internal/ghidra-pcode-integration-research.md: P-Code opcode
core, the decompiler C++ embedding API (LoadImage/SleighArchitecture/Funcdata),
the CORE+DECCORE+SLEIGH source sets, no-bison finding, and pypcode as build
reference.
Phase 1 — vendored Ghidra decompiler at pinned commit (Ghidra_12.1_build,
7e89d94e34...) under third_party/ghidra-decompiler/ (cpp + AArch64 specs +
Apache-2.0 LICENSE + VENDOR.md + .gitignore for build artifacts). Validated by
hand on this clang-21/macOS toolchain:
- full SSA engine (CORE+DECCORE+SLEIGH, 80 files incl. heritage/funcdata/
action) compiles clean, -std=c++11 -O2, NO BFD, NO bison (generated
parsers are committed upstream; ruleparse isn't in the lib set);
- sleigh compiler builds; AArch64 .slaspec -> .sla compiles;
- tools/pcode_dump.cpp (custom LoadImage, no BFD) lifts the real arm64
sym._div_by_zero_direct to correct P-Code: `mov w9,#0 -> COPY(const 0)`,
`sdiv -> INT_SDIV(w8,w9)` — divisor zero-ness explicit in the data flow,
so the Phase-3 encoder proves div-by-zero trivially, multi-arch.
Not yet meson-wired (next step) and no fold-side IR/encoder yet (Phase 2-3);
this commit is the validated vendor + smoke tool.
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>
The Loop-1 hardcoded-credential suppression left the binary string scan
matching only `key=value` credential forms, so bare secret literals and
provider API keys baked into a binary were missed, while the base64-blob
heuristic false-positived on toolchain paths (their long alnum+`/` runs are
valid base64).
- kApiKeyPattern: standalone provider keys (OpenAI sk-/pk-, Stripe
sk_live/sk_test, GitHub ghp_/gho_, AWS AKIA), category "api-key".
- kBareSecretPattern: a secret/password word embedded in a larger token with
a trailing digit/symbol (supersecret123, adminpass!), distinguishing a
hardcoded value from the English word "secret" in a message.
- looksLikeBuildArtifactPath: skip base64-blob on absolute toolchain paths
(/var/folders, /private/var, DerivedData, .dSYM, /.build/, /usr/lib,
/System/Library) — kills the build-path FP without losing embedded base64.
Validated on bench/corpora/ctf-challenges/libcmd_injection.dylib:
+2 TP (supersecret123, sk-1234567890abcdef now detected), -1 FP
(/var/folders base64 path suppressed). No new credential FPs across the
other corpus dylibs. Source backend untouched (binary-only TU). 68 Ok /
0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Fortified (`-D_FORTIFY_SOURCE`) Mach-O/ELF binaries import `__strcpy_chk`,
`__sprintf_chk`, `__strncpy_chk`, etc. instead of the base routine.
normalizedSymbolName stripped the leading `_` and known prefixes but not the
`_chk` suffix, so these normalized to `strcpy_chk`/… and missed the
dangerous-import and dangerous-call sets — fortified buffer-overflow sinks
(CWE-121) went undetected in binary mode.
Strip a trailing `_chk` (suffix-only, after lowercasing) so they map to
`strcpy`/`sprintf`/`strncpy`. Suffix-only is safe: stack-protector internals
`__stack_chk_fail` / `__stack_chk_guard` end in `_fail`/`_guard` and are
unaffected, and `__memcpy_chk` → `memcpy` (not in the dangerous set) stays
silent.
Validated on bench/corpora/ctf-challenges/libbof_overflow.dylib: the fortified
`__strcpy_chk`/`__sprintf_chk`/`__strncpy_chk` are now flagged (FN→TP for the
CWE-121 overflows). Source gate unaffected (binary-only change); meson 68/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Record that rust_ir_encoder and binary_bb_encoder do not route through
SecurityWalker/unrollLoop and have no loop handling, so "cross-frontend
ir::Loop reuse" is gated on a shared clang-free loop-walk core rather than
being a standalone slice. Lay out the realistic sequencing (clang-free CFG
foundation -> rust/binary lowering -> recall-preserving while(1) acceleration)
and note no safe small gate-validatable slice exists short of starting the
foundation. Clang counted+affine summarization is complete.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
