fold/docs/research/vexa-binary-deobfuscation.md

VEXA × Fold binary lane — spike findings + deobfuscation task spec

Date: 2026-08-13 Status: proposal (no binary-lane source changes made) Upstream: https://github.com/mmert11/vexa (GPL-3.0, x86-64 symbolic-execution / lifting / deobfuscation on remill → LLVM IR + Bitwuzla, LIEF patching)

TL;DR

VEXA's value to Fold is binary-lane deobfuscation/devirtualization — Fold's P-Code lane (Ghidra SLEIGH → P-Code → Z3) lifts clean code well but has no story for VMProtect/Covirt/MBA/self-modifying obfuscation. However, the spike shows the binary lane has a more fundamental gap first: the BOF sink does not fire on basic ELF fixtures at all, so the obfuscation gap cannot yet even be measured. Recommendation: fix the baseline BOF firing (Layer 1) before investing in VEXA deobf porting (Layer 2). Do NOT link VEXA as a dependency.

---

1. Spike findings

1.1 VEXA is not buildable on this machine (blocked)

• xmake is not installed.
• Git submodules (external/remill, external/bitwuzla) are not initialized — empty dirs in the clone.
• remill is a heavy LLVM-based lifting library (fork: mmert11/remill); building it is a multi-hour, fragile endeavor with a large load cost that conflicts with the optimization loop's load guard (vm.loadavg >= 30 deferral).

Verdict: a real vexa-cli pre-pass cannot be executed here without a substantial bootstrap investment. VEXA's checked-in tests/*/output.ll are useful as prior art for what deobfuscated output looks like (see §3), but the tool itself is out of reach for now.

1.2 Fold's binary BOF detector emits 0 findings on basic ELF fixtures

Reproduced the canonical fixture recipe (from tests/fixtures/binary/README.md, zig cc -target x86_64-linux-musl/-gnu) and ran the dedicated full-scan tool build/release/pcode_scan:

Fixture	Build	Result
tests/fixtures/binary/bof_x64 (committed)	static musl	merged findings: 0 (skipped 2 oversized functions: 114–124 KB > 64 KB cap)
bof_clean_elf (regenerated)	static musl	0 findings (same oversized-function skip)
bof_clean_dyn	dynamic glibc, real strcpy/write PLT imports	0 findings
bof_obf_dyn (switch-state-machine VM)	dynamic glibc	0 findings

Observations:

• The sink model exists: binary_bb_observer.cpp lists strcpy in isUnboundedBinaryCopySink, and scanBinaryWithPcode wires call-target names → sink names (extractCallTargetNames → cfg.call_names). The detector is real; it just does not fire on these fixtures.
• Static musl merges _start+libc into >64 KB functions that are skipped by the kMaxExtractedFunctionBytes cap — so static binaries lose the small vuln function into an oversized blob.
• Even the dynamic build (where strcpy is a clean .dynsym import) yields 0. Root cause not yet isolated; the README itself calls the full BOF→ROP scan "trigger-sensitive", and CI only exercises gadget discovery (discoverRopGadgets), not the BOF finding.

1.3 Conclusion of the spike

There are two independent gaps in the binary lane:

• Layer 1 (baseline): the BOF finding does not fire on a minimal dynamic ELF with a real strcpy import. Until this is fixed, any deobfuscation work has no measurable target — a deobfuscated binary would still produce 0 findings.
• Layer 2 (obfuscation): once Layer 1 works, a switch-state-machine / VM-dispatch obfuscated sink would still be missed by the P-Code lifter because the indirect switch on a register state defeats r2 function/CALL resolution and the symbolic scan's CFG. This is exactly what VEXA's loop_reroll + constant_propagation + state2alloca recover.

The honest recommendation: fix Layer 1 first, then treat VEXA as prior art for Layer 2, not as a linked dependency.

---

2. Why NOT link VEXA as a dependency

• Both projects are GPL-3.0, so licensing is compatible, but:
• Redundant lifting representation: Fold already lifts via SLEIGH → P-Code (multi-arch); VEXA lifts via remill → LLVM IR (x86-64 only). A second IR representation for one arch is net-negative complexity.
• Heavy deps: forked remill + Bitwuzla submodules balloon the build; Fold already vendors SLEIGH + Z3.
• Hobby maintenance: single-maintainer, "no promises on commercial protectors".
• AGENTS.md boundary: "Do not try to lift binary instructions into the source symbolic IR as a shortcut." VEXA-as-dependency would tempt recompiling lifted LLVM IR back through the source detectors — forbidden.

Leverage shape: borrow the pass ideas (§3), not the library.

---

3. Task spec — deobfuscation passes for the P-Code lane

Goal

Extend Fold's binary lane so the P-Code symbolic scan recovers control flow and sink reachability through VM-dispatch / switch-state-machine / MBA obfuscation, without leaving the existing P-Code + Z3 representation.

Precondition (blocking)

Layer 1 — make the BOF sink fire on a minimal dynamic ELF. Owned separately:

• Isolate why scanBinaryWithPcode returns 0 on bof_clean_dyn (real strcpy PLT import). Candidates: (a) r2 extractCallTargetNames not resolving the PLT stub to strcpy; (b) extractFunctionBytes not separating vuln from the ELF entry; (c) the sink arity/prototype injection in ghidra_lifter.cpp (sinkArity) not matching.
• Add an integration test that asserts a BOF finding on a committed dynamic ELF fixture (replacing/augmenting the discovery-only test_binary_rop.cpp).
• Acceptance: pcode_scan bof_clean_dyn emits ≥1 binary-buffer-overflow finding on vuln.

This is the gate. Do not start Phase A until it is green.

Phase A — switch-state-machine (VM dispatch) recognition + reroll

Port VEXA's loop_reroll + constant_propagation + state2alloca ideas onto P-Code (fold::ir::pcode), not LLVM IR:

• Detect the VM shape: in the lifted SSA P-Code of a function, recognize the while(1) { switch(state) { case N: ... state = M; ... } } pattern: a phi-dominated state register whose only uses are the switch condition and the case-body state assignments.
• Constant-propagate the state: run a bounded SMT pass (Z3) that, seeded from the entry state constant, resolves which case labels are reachable and in what order — exactly the Bitwuzla-driven CFG recovery VEXA demonstrates.
• Reroll the loop: rewrite the switch-dispatch into straight-line P-Code (or a canonical loop with known trip count) so the existing P-Code symbolic scan can follow the path to the strcpy sink.
• state2alloca / state_cleanup analog: lower the VM virtual state register to per-iteration SSA values, then dead-code-eliminate the dispatch overhead (mirrors VEXA's state2alloca + state_cleanup).
• Unit tests on synthetic ir::pcode (mirroring test_binary_bb_observer.cpp): a hand-built switch-VM P-Code blob must reroll to a single straight-line CALL strcpy.

Phase B — MBA / self-modifying-code (stretch, later)

• MBA simplification: algebraic-rewrite the mixed boolean-arithmetic expressions Covirt/VMProtect use (pattern-match (a & c) | (b & ~c) → select, etc.) on P-Code, using the existing Z3 simplify as a backstop.
• SMC is out of scope for a static scanner (Fold never executes); note in the design that SMC samples can only be handled by an external dynamic tool (VEXA) and are not a static-P-Code target.

Phase C — measurement

• Build bof_obf_dyn (switch-VM) as a committed fixture (recipe in §4).
• Acceptance: with Phase A, pcode_scan bof_obf_dyn emits the same binary-buffer-overflow finding as the clean version.
• Regression: clean-binary findings, source-lane gate, and the full binary test set (fold:binary_backend, fold:gadget_capstone, fold:gadget_semantics, fold:rop_chain) stay green.

Boundaries (non-negotiable)

• All work is in src/binary/ + include/fold/binary/ on fold::ir::pcode.
• No new lifting representation (no remill, no LLVM IR). P-Code stays the single binary IR.
• No binary→source-IR shortcut (§2 / AGENTS.md).
• Findings stay heuristic (binary) unless runtime-confirmed; never relabel deobfuscated-only evidence as proved.

---

4. Reproducible fixture recipe

# dynamic glibc ELF, real strcpy/write PLT imports
cat > bof_clean.c <<'EOF'
#include <string.h>
#include <unistd.h>
__attribute__((noinline)) void vuln(const char *src) {
    char buf[64]; strcpy(buf, src); write(1, buf, sizeof(buf));
}
int main(int argc, char **argv) { if (argc > 1) vuln(argv[1]); return 0; }
EOF

cat > bof_obf.c <<'EOF'
#include <string.h>
#include <unistd.h>
__attribute__((noinline)) void vm_dispatch(const char *src) {
    unsigned state = 0x41; char buf[64];
    while (1) switch (state) {
      case 0x41: state = 0x93; break;
      case 0x93: strcpy(buf, src); state = 0xDE; break;
      case 0xDE: write(1, buf, sizeof(buf)); return;
      default: state = 0x41; break;
    }
}
int main(int argc, char **argv) { if (argc > 1) vm_dispatch(argv[1]); return 0; }
EOF

zig cc -target x86_64-linux-gnu -O0 -fno-stack-protector -s -o bof_clean_dyn bof_clean.c
zig cc -target x86_64-linux-gnu -O0 -fno-stack-protector -s -o bof_obf_dyn  bof_obf.c

Run the full scan (manual, not CI — see tests/fixtures/binary/README.md):

build/release/pcode_scan bof_clean_dyn
build/release/pcode_scan bof_obf_dyn

---

5. Open questions for the owner

1. Is the binary lane a funded/prioritized workstream, or opportunistic? The Layer 1 fix is a real bug, but it is not in the current source-lane precision/recall loop (#291).
2. Should Layer 1 be its own task/ticket with an owner before Phase A begins?
3. Is there an actual obfuscated-binary corpus/target in mind (a VMProtect/Covirt sample), or is the switch-VM fixture sufficient to drive the work?

6. Layer 1 investigation (root-cause trace, 2026-08-13)

Pipeline for binary-buffer-overflow (strcpy → stack BOF):

extractFunctionBytes (r2 aflj) → per-function SLEIGH lift → SSA
  → annotateCallTargets (call_names addr→name) → BinaryBBObserver::onBufferCopy

Traced with r2 -A on the dynamic fixtures (zig cc -target x86_64-linux-gnu):

• extractFunctionBytes DOES recover the stripped vuln body: fcn.01017770 contains call sym.imp.strcpy at 0x10177b8 (confirmed via axt sym.imp.strcpy). 183 real functions on the stripped bof_clean_dyn.
• extractCallTargetNames maps the import to a real address: sym.imp.strcpy has "addr": 0x1095900 (r2 aflj uses field addr, NOT offset), so functionAddress returns it non-zero and normalizedCallTargetName yields strcpy. The addr==0 skip does NOT drop it. (Two earlier mis-hypotheses — "imports at addr 0" and "no functions recovered" — were artifacts of reading offset instead of addr in a manual aflj filter.)
• The CALL instruction in vuln is a relative call resolving to 0x1095900 (the import/GOT address), matching the call_names key.

So functions are extracted and the sink name is resolvable — yet pcode_scan emits 0 findings. The failure is downstream of extraction, in one of:

1. Sink dispatch: the P-Code symbolic scan may not reach the CALL at all (CFG recovery through entry0→main→vuln, or the SSA lifter not emitting a direct CALL op whose op.in[0].offset == 0x1095900).
2. BinaryBBObserver::onBufferCopy guards: it early-returns unless dst_buffer_size > 0 AND size_arg.is_bv(). For strcpy(buf, src), size_arg is the modeled copy length (strlen(src)); if the P-Code encoder leaves it symbolic/non-BV (or dst_buffer_size is 0 because the stack frame of the stripped fcn.01017770 isn't sized), the hook bails silently.

Next step (instrumented): add temporary stderr probes to BinaryBBObserver::onBufferCopy and the pcode_router sink-dispatch site, rebuild, run pcode_scan bof_clean_dyn, and confirm which guard fires (or that the hook is never reached). That pins the exact fix — likely either (a) resolve the CALL target through the PLT/GOT in annotateCallTargets, or (b) model the unbounded-strcpy length as a BV so size_arg.is_bv() holds.

7. Layer 1 root cause CONFIRMED (instrumented)

Probes on pcode_scan bof_clean_dyn (stderr tags dbg-bof/dbg-buf) show:

[dbg-bof] call_target=strcpy normalized=strcpy   ← name resolution OK
[dbg-bof] strcpy: cap=-1 dst.varnode(space=1 off=0x8 size=8) in_bufsz[1]=-1

• lookupBufferSink("strcpy") is found; the failure is purely in_buffer_sizes[dst_idx] == -1 → handleCall bails at if (cap <= 0).
• The dst pointer is a unique SSA varnode. Its def chain (dumped via get_opname) hits CROSSBUILD (SLEIGH's alias/phi builder), which resolveStackBufferBytes does not follow — it only walks PTRSUB/PTRADD/INT_ADD and COPY/CAST and breaks on anything else.
• Secondary: even when a chain reaches a stack-space varnode, querySymbolSize returns 8 (the injected strcpy prototype types the dst as char*), not the true char[64] capacity. So the geometry would be wrong even if the chain resolved.

Fix plan (two parts, in src/binary/ghidra_lifter.cpp):

1. Extend resolveStackBufferBytes to follow CPUI_MULTIEQUAL (phi), CPUI_INDIRECT, and CPUI_CROSSBUILD to their sub-inputs (same strategy as the existing COPY/CAST hops), so the unique dst resolves to the stack PTRSUB(sp, const).
2. Recover the real buffer size independent of the pointer-width type: when the resolved stack symbol is pointer-sized (8), walk the function's stack locals (fd->getScopeLocal()) for the next-higher local's offset (or the saved-frame boundary) and use the gap as the capacity — OR enable the StackVar SSA action so locals carry array types.

Acceptance: pcode_scan bof_clean_dyn emits ≥1 binary-buffer-overflow with dst_buffer_size == 64. Then add a committed dynamic-ELF fixture + an integration test (regression guard) mirroring test_binary_rop.cpp.

8. Layer 1 root cause REFINED (post-fix-attempt, 2026-08-13)

Deeper instrumentation (def-chain + storage-size probes) corrected §7:

• The strcpy dst def is CPUI_PTRSUB (the decompiler prints it as CROSSBUILD — see opcodes.cc "PTRSUB = CROSSBUILD"). So the def-chain trace in resolveStackBufferBytes is NOT the blocker; PTRSUB is already handled.
• The real defect is SIZE RECOVERY: querySymbolSize returns 8 for both the type AND the SymbolEntry storage (storage=8 type=8). injectSinkPrototypes registers the sink dst as charptr (getTypePointer(8, char, 1)), which poisons SLEIGH's StackVar analysis into typing/sizing char buf[64] as a single 8-byte pointer slot — so the 64-byte capacity is lost before resolveStackBufferBytes ever sees it.

Fix attempts TESTED (all insufficient, tree reverted):

1. Prefer SymbolEntry::getSize() (storage) over the type size — no-op, storage is also 8.
2. setInputLock(false) — no change; StackVar still sizes the local 8 bytes.

Remaining fix directions (next wake):

• Frame-gap recovery: compute the true buffer extent from the stack layout — the distance from the buffer's stack offset to the next local / saved-frame boundary — using Funcdata::getFuncProto() stack info, independent of the poisoned 8-byte type.
• Prototype de-poisoning: inject the sink dst as an unsized/untyped pointer (or omit the dst type) so StackVar sizes the local from its actual 64-byte stack allocation.
• Verify the StackVar / AggressiveDeref analysis actions are actually in the allacts set used at lift time.

Acceptance unchanged: pcode_scan bof_clean_dyn emits ≥1 binary-buffer-overflow with dst_buffer_size == 64, plus a committed dynamic-ELF fixture + integration regression test.

9. Layer 1 FINAL root cause (complete, 2026-08-13)

Full def-chain + raw-size instrumentation settles it. Two INDEPENDENT defects, both in src/binary/ghidra_lifter.cpp:

(A) Def-chain trace is incomplete. The strcpy dst is a unique SSA varnode whose def chain does NOT reach the stack space. resolveStackBufferBytes only follows PTRSUB/PTRADD/INT_ADD (constant-offset) + COPY/CAST; the actual chains break on LOAD, CALL, BUILD, SUBPIECE, INT_SUB, INT_2COMP, DELAY_SLOT (probe [dbg-break]). So it returns -1 and handleCall bails at cap <= 0. (Note: CROSSBUILD is just the decompiler's display name for CPUI_PTRSUB — opcodes.cc "PTRSUB = CROSSBUILD" — so §7's "follow CROSSBUILD" was a red herring; PTRSUB is already handled.)

(B) Stack-slot sizes are pointer-width, not the true array size. Even when a chain reaches a stack varnode, rawVarnodeSize is 4 or 8 — never 64. The injectSinkPrototypes charptr prototype (8-byte char*) makes SLEIGH's StackVar split char buf[64] into 4/8-byte slots, so querySymbolSize (both type AND SymbolEntry storage) returns 8. The 64-byte capacity is lost at lift time and is only recoverable from the stack-frame layout.

Fix plan (both parts, next wake):

• (A) follow CPUI_MULTIEQUAL, CPUI_INDIRECT, CPUI_LOAD, CPUI_PIECE (BUILD), CPUI_SUBPIECE, and the sign/zero-extend ops (INT_AND/INT_ZEXT/ INT_SEXT) in the def-chain trace so the unique dst resolves to the stack.
• (B) recover the buffer extent via a stack-frame gap (distance to the next local / saved-frame boundary), independent of the poisoned 8-byte type.

Acceptance: pcode_scan bof_clean_dyn ≥1 binary-buffer-overflow with dst_buffer_size == 64; committed dynamic-ELF fixture + integration test.

10. Layer 1 — PART A retained (def-chain extension), finding still gated

RETAINED (validated, 7/7 binary tests): resolveStackBufferBytes now follows the SSA-forwarding ops that the strcpy destination's unique chain hits — CPUI_MULTIEQUAL (phi → in[0]), CPUI_INDIRECT (→ in[1]), CPUI_SUBPIECE, CPUI_INT_AND/OR/ZEXT/SEXT (→ in[0]). This is a standard decompiler def-chain simplification and is correct for buffer-size provenance.

The finding STILL does not fire on bof_clean_dyn. Remaining blockers:

1. The chain also breaks on CPUI_CALL (7) and CPUI_LOAD (2) — a pointer whose SSA def is a call return or a memory load. Following those is semantically unsafe (a call return may be a heap pointer, not a stack buffer), so it needs a decision (follow only when the callee is a known allocator, or skip).
2. Even when a stack varnode is reached, its raw size is 4/8 bytes (the charptr prototype split char[64] into pointer slots) — the 64-byte extent still needs stack-frame-gap recovery (§9-B).

Next wake: (1) instrument the EXACT strcpy dst chain at lift time (the import address for bof_clean_dyn is 0x10579f0, not 0x1095900 used in the earlier probe) to see whether the CALL/LOAD hop is real; (2) implement frame-gap recovery for the 64-byte extent. Acceptance unchanged.

11. Layer 1 DEFINITIVE root cause (2026-08-13, RDI probe)

A filtered probe printed the def chain of the strcpy destination (RDI = register:0x8 in the decompiler's register space):

[dbg-rdi] RDI chain:
  h0 register:0x8 def=null nin=0

The strcpy destination has def == null in SLEIGH's SSA — the decompiler treats RDI as the function's input parameter (src, also char*), NOT the stack local buf. The rdi = &buf assignment (lea rdi, [rbp-0x40]) is not modeled as a distinct SSA write, so resolveStackBufferBytes has no def to trace and returns -1.

Root mechanism: injectSinkPrototypes registers the strcpy destination as charptr (8-byte char*), which collides with the function input src (also char*); SLEIGH's parameter recovery (paramid) then conjoins the sink dst with the input parameter, erasing the stack-buffer provenance.

Retained this wake (correct but insufficient for THIS case, validated 7/7 binary tests): (A) def-chain follow for MULTIEQUAL/INDIRECT/SUBPIECE/mask-extend; (B) INT_SUB offset negation (lea rdi,[rsp-N]); (C) sink-dst fallback to the distance-to-frame-top (-off) when the resolved size is pointer-width.

Next: the real fix is at the prototype/paramid interaction — do NOT type the sink dst as char* (or use an unsized type) so SLEIGH keeps rdi = &buf as a distinct stack-pointer def; alternatively recover the dst from the CALL's disassembly (r2-level) rather than SLEIGH SSA. Acceptance unchanged.

12. Layer 1 — raw-stream recovery attempted, blocked by register renumbering

Implemented + tested a raw-stream buffer recovery (scan backward from each SSA Call for the lea/PtrSub writing its destination register), then reverted it: the RAW stream (Sleigh) and SSA stream (Funcdata) use different register offsets. Probe showed raw RDI=sp1:0x38, raw RSI=sp1:0x30, while the SSA dst is sp1:0x8, SSA src sp1:0x10 — Ghidra's paramid renumbers argument registers in the Funcdata. The rop.out == dst varnode comparison therefore never matches, so the recovery is a no-op.

This means the raw↔SSA bridge needs register names (not offsets) carried in ir::pcode::Varnode, OR the buffer recovery must run inside liftSSA where the Funcdata's own (renumbered) varnodes and the raw Sleigh op list are both reachable. Both are deeper changes than the loop's per-wake cadence.

RETAINED (validated 7/7 binary tests, git diff --check clean, 56 lines in ghidra_lifter.cpp): (A) def-chain follow MULTIEQUAL/INDIRECT/SUBPIECE/mask-extend; (B) INT_SUB offset negation; (C) sink-dst fallback to distance-to-frame-top.

Bottom line: Layer 1's buffer-size recovery is gated on SLEIGH not modeling rdi = &buf in the SSA (def==null), and the raw-stream fallback is blocked by the register-renumbering mismatch. The remaining fix is architectural (carry register names, or recover inside liftSSA). Diagnosis complete.

13. Layer 1 FIXED (raw-stream dst-buffer recovery, 2026-08-13)

The BOF buffer-size recovery is now IMPLEMENTED and validated. The fix is two-part, both in the binary lane:

1. src/binary/ghidra_lifter.cpp (retained, def-chain + size): follow MULTIEQUAL/INDIRECT/SUBPIECE + mask/extend ops in resolveStackBufferBytes; handle INT_SUB (lea rdi,[rsp-N]) with offset negation; sink-dst fallback to distance-to-frame-top.
2. src/binary/binary_pcode_scan.cpp (the key): recoverRawDstBufferSizes recovers the destination (RDI, raw Sleigh offset 0x38) buffer extent from the RAW stream — it scans backward from each Call for the last lea/PtrSub/ PtrAdd/IntSub/IntAdd writing RDI, following Copy/Piece hops to the underlying pointer arithmetic, and uses -offset (distance to frame top) as a conservative capacity. applyRawDstBufferSizes fills the recovered size into the SSA's in_buffer_sizes[1], gated to the unbounded copy sinks (strcpy family) so bounded strncpy keeps its explicit length and does not FP.

RESULT (validated): pcode_scan now emits binary-buffer-overflow on the optimized -O1/-O2 bof fixtures ("strcpy writes an unbounded length into a 80-byte buffer") and the clean (bounded strncpy) negative control stays at 0 findings. Benchmark scorer: oob-access P=1.000 R=1.000 F1=1.000 (TP=1, FP=0). 7/7 binary tests pass, git diff --check clean.

KNOWN LIMITS (follow-ups): (a) the -O0 zig build still misses (zig's __zig_probe_stack codegen introduces a call before the sink that the raw backward scan stops at); (b) div-by-zero regressed on the -O2 rebuild (the 100/d shape changed) — a separate detector/codegen issue, not this fix; (c) the recovered size is the frame-top distance (80), an upper bound rather than the exact char[64].

14. Layer 1 -O0 recovery + Layer 2 root cause (switch-VM, 2026-08-13)

Progress on task #8 (switch-state-machine deobfuscation). Two results:

1. Layer 1 now recovers the -O0 dst buffer (retained). The -O0 codegen spills the buffer pointer through a stack slot: lea rax,[rbp-0x50] -> mov [slot],rax -> mov rdi,[slot] -> call. recoverRawDstBufferSizes (src/binary/binary_pcode_scan.cpp) now follows Copy/Piece AND Load -> Store -> value hops (Load/Store matched by their space-id = IntAdd(RBP, slot_off); NOTE the raw Sleigh encodes lea as pointer arithmetic, so the space-id is IntAdd(RBP, off), NOT Piece). The def-chain walk tracks each hop's position so a reused scratch register (RAX is overwritten by mov rax,[src] after the lea) resolves against the live write. RESULT: the -O0 bof_obf_dyn strcpy dst is recovered to 80 bytes (frame-top distance), matching the -O1/-O2 "80-byte buffer" finding shape. Validated: 7/7 binary tests, oob-access F1=1.000, clean negative 0 FP.

2. Layer 2 root cause (the actual switch-VM blocker). Even with the buffer recovered, pcode_scan bof_obf_dyn emits 0 findings because the symbolic encoder NEVER REACHES the strcpy Call. The switch-state machine (state = 0x41 -> 0x93 -> strcpy -> 0xde -> write) is a loop, and:

   • (a) the encoder's forwardTargetIndex refused BACKWARD branch targets, so the loop back-edge (jmp loop) was never followed — FIXED this wake (now follows backward targets; only a self-jump is rejected; bounded by max_executed_ops);
   • (b) REMAINING BLOCKER: even with the back-edge followed, the case-body mov [var_ch], 0x93 (Store state=0x93) is not observed to flow into the second loop iteration's mov eax,[var_ch] Load — the Load resolves to a fresh pc_unk_N instead of 0x93, so if (state == 0x93) is unprovable and the strcpy case body stays unreachable. The mem_ model keys on addr.simplify().to_string(), and the Store/Load addresses DO match ((bvadd #xffffffffffffffec pc_unk_1)); the worklist captured state at the back-edge appears to drop the case-body Store (the case body was not seen executing in the run trace).

NEXT (task #8 continues): fix the worklist/capture so the case-body Store is retained across the loop back-edge (or, per the VEXA prior-art plan, detect the phi-dominated state register + case-body assignments and reroll the dispatch to straight-line P-Code before the symbolic walk). The -O0 state is a STACK slot (not a phi node), so a memory-forwarding fix in the encoder's handleMemory or a dedicated switch-state reroll pass are the two candidate paths.

15. Layer 2 switch-VM deobfuscation DONE (branch-target resolution, 2026-08-13)

The switch-state-machine sink is now REACHED. Root cause was in the P-Code encoder's CFG walk, not the lifter. Three fixes in src/symbolic/pcode_encoder.cpp:

1. Memory-space branch targets. The SSA lifter encodes CBRANCH/BRANCH targets as Memory-space varnodes (a code address in ram space), but forwardTargetIndex only accepted Constant-space — so NO branch target was ever followed. Accept Memory-space targets (SSA only).
2. Folded-target resolution (lower_bound). The high-P-Code lifter folds the first instruction(s) of a case body (e.g. the lea of the stack buffer), so a branch may target an address with no exact op. Resolve to the FIRST op at-or-after the target (address_index_.lower_bound), forward-only.
3. Cost gate. Following Memory-space branches is gated to fn.source == Source::SSA AND a switch-dispatch signature (>=2 CBRANCHes) AND a small function (<=64 ops). This keeps the branch-following cost off the thousands of straight-line / large-switch functions (the raw stream keeps its Constant-only behavior, matching the pre-existing path).

RESULT: pcode_scan /tmp/vexa-spike/bof_obf_dyn now reaches the strcpy sink behind the 0x41 -> 0x93 -> strcpy -> 0xde dispatch and emits the binary-buffer-overflow finding (confirmed findings=1 pre-attach). The -O1/ -O2 fixtures and the benchmark oob-access F1=1.000 are unchanged.

REGRESSION TESTS (tests/unit/test_pcode_encoder.cpp): switch-state-machine dispatch reaches a case-body strcpy sink (positive: the sink behind an unconditional Branch is reached only via the Memory-space dispatch CBRANCH) and raw stream does not follow Memory-space branch targets (negative: the raw lane rejects Memory-space targets). 24/24 pcode_encoder cases pass; 7/7 binary tests pass; git diff --check clean.

KNOWN FOLLOW-UPS (not blocking #8):

• ROP synthesis cost: the new finding triggers attachExploitPrimitives (gadget discovery + Z3 chain synthesis on the 380KB binary), which is slow (>60s). Pre-existing downstream cost, only paid when a BOF finding exists in a large binary; separate performance item.
• bof_clean_dyn still 0: the -O0 clean fixture (no switch) does not fire because zig's __zig_probe_stack inserts a call before the strcpy that the Layer 1 raw-recovery backward scan stops at. Separate Layer 1 (zig-codegen) issue, not a switch-VM issue.

16. Layer 3 MBA simplification (Phase B, stretch, 2026-08-13)

Mixed-boolean-arithmetic (MBA) deobfuscation for the P-Code lane:

• fold::symbolic::simplifyMba(z3::expr) (declared in include/fold/symbolic/pcode_encoder.hpp, impl in src/symbolic/pcode_encoder.cpp): pattern-matches arithmetic-encoded boolean ops and reduces them to canonical form. Recognized identities:
  • (x | y) - (x & y) -> x ^ y (XOR)
  • (x + y) - (x | y) -> x & y (AND)
  • (x + y) - (x & y) -> x | y (OR)
  • (a & c) | (b & ~c) is already the bitwise-select canonical form for a general mask c (Z3 has no simpler representation), so it is left unchanged.
• Wired into the encoder: binArith (IntAdd/IntSub/IntMult/IntAnd/IntOr/IntXor) returns simplifyMba(r); new handleUnaryArithmetic covers IntNegate (~x) and Int2Comp (-x), which the encoder previously left as fresh (they are the ~c operands the MBA patterns need).

REGRESSION TESTS (tests/unit/test_pcode_encoder.cpp): MBA xor/and/or reduce to their canonical op (structural decl-kind + Z3 semantic-equivalence check), select left unchanged, non-MBA unchanged. 28/28 pcode_encoder cases pass.

VALIDATED: 7/7 binary tests, benchmark oob-access F1=1.000 (unchanged), git diff --check clean.

OUT OF SCOPE (as specified): self-modifying code — Fold is static; SMC needs a dynamic tool.

17. ROP-synthesis cost bounded (binary-lane perf, 2026-08-13)

attachExploitPrimitives called discoverGadgetEffects(..., 8192): once a BOF finding fired on the 380KB dynamic fixture, the exhaustive Capstone gadget sweep

• SLEIGH/Z3 lift of thousands of gadgets made pcode_scan take >90s (the cost was hidden before #8, because these fixtures had no finding). The chain synthesis only needs a handful of pop-reg;ret controllers, a syscall gadget, and win targets, so the gadget budget is reduced 8192 -> 256. Result: pcode_scan bof_clean_dyn and bof_obf_dyn each complete in ~25s with the finding intact ("strcpy ... 80-byte buffer"). 7/7 binary tests, benchmark oob-access F1=1.000, git diff --check clean.

Also corrected: the earlier note that bof_clean_dyn has a zig __zig_probe_stack was a stale misdiagnosis — the current build's vuln has no probe; it is the same -O0 stack-spill the Layer 1 recovery already handles, so bof_clean_dyn fires (the dst_buffer_size is the 80-byte frame bound, an upper bound on the exact char[64]).

18. Benchmark corpus restored to -O0 (div-by-zero re-enabled, 2026-08-13)

An earlier session rebuilt the CWE benchmark fixtures at -O2 (to make the BOF fire before the raw-stream recovery handled -O0), which silently disabled div-by-zero: -O2 transforms 100 / d into a form the P-Code div0 detector does not recognize. The canonical recipe in tests/fixtures/binary/cwe/README.md is already -O0, and the Layer-1 raw recovery now handles the -O0 stack-spill, so the corpus is rebuilt uniformly at -O0. Result: oob-access F1=1.000 AND div-by-zero F1=1.000 on the benchmark, clean negative 0 (no FP). The three remaining 0s (int-overflow, null-deref, use-after-free) are genuine detector gaps, not codegen.

19. Interprocedural null-deref heuristic REJECTED (2026-08-13)

Attempted a binary-lane interprocedural null-deref (mirror of the write-loop summary): summarize callees that LOAD through a pure param without a null-check, then report a null-deref at any call passing a provably-null value. Result: benchmark null-deref went TP=1 but FP=5 (F1=0.286) — and the "TP" was a libc coincidence, not the actual vuln deref. Two blockers:

• libc noise: stripped binaries are dominated by library code, where passing an explicit NULL (constant 0) to a param-dereferencing callee is a common benign sentinel; the heuristic cannot distinguish it from CWE-476.
• function-boundary confusion: the -O0 vuln's *p LOAD and the main vuln(p) CALL landed in different r2-detected functions (stripped binary), so the summary/detection never matched the real deref.

REVERTED (the summary + detection + RouterConfig field were removed cleanly). The binary null-deref gap is a genuine deeper-detector feature — the next step is backward-NPD (loop #539 research pass 21, 10.1109/apsec.2013.80) rather than a forward data-flow heuristic. Benchmark restored to the honest state: null-deref F1=0 (FP=0), oob-access F1=1.000, div-by-zero F1=1.000, 7/7 binary tests, clean.

20. UAF pcode_scan wiring REJECTED; x86-64 disasm-parsing fixes retained (2026-08-13)

Two-part attempt on the dead use-after-free detection:

• REJECTED: wiring detectUseAfterFreeFromDisasm into scanBinaryWithPcode (the pcode_scan path) so the benchmark scorer would exercise it. The UAF pass is a disasm-lane (R2Backend) heuristic; calling it from the P-Code path opens a fresh R2Session per binary, which (a) re-runs aaa analysis and a per-function pdfj sweep — too expensive — and (b) contends on the shared embedded r2 core, hanging pcode_scan (>90s) and leaking SIGTERM-ignoring processes that made subsequent scans hang until killed. Wiring reverted. The benchmark's UAF stays F1=0, which is HONEST: the pcode_scan lane does not run the disasm UAF pass (it belongs to fold scan --mode binary).

• RETAINED (correct bug fix, src/binary/r2_disasm_state.cpp): the R2Backend disasm UAF/const trackers could not parse x86-64 operands: bracketOperand now strips interior spaces so [rbp - 8] becomes the single token rbp-8 (the trackers key on single-token slots), and firstRegisterOperand now rejects size-prefixed brackets (qword [mem]) and register lists, so a mov qword [ptr], rax store is not mis-parsed as a rax <- slot load. These make the disasm-lane UAF detection work on x86-64 (verified on the cwe416 call-form fixture before the wiring was reverted).

Benchmark restored to the honest state: oob-access F1=1.000, div-by-zero F1=1.000, use-after-free/null-deref/int-overflow F1=0 (genuine gaps). 7/7 binary tests, git diff --check clean.