Patch Audit Schema - SOUNDNESS_CLAIMS Spec

This is the schema spec referenced in How I Audit Security Patches with an AI Pipeline. It defines the SOUNDNESS_CLAIMS format, the empirical proof requirement, and the adjacent-unpatched rule.

SOUNDNESS_CLAIMS Format

Each claim is a falsifiable hypothesis about a specific attack vector. Required fields:

F(x):          The trigger - exact JS/Wasm/HTML/API call that initiates the attack
P(x-pre):      What the pre-fix code does with it - execution path, vulnerable state reached,
               specific values or pointers involved (file:line where the bad state occurs)
prefixfailure: The concrete outcome - crash type, what leaks, what gets corrupted, what misses a trap
postfixstatus: Where the fix blocks the path - specific file:line of the new guard or structural change
               Always ends with "To be confirmed empirically" until runtime proof is in hand

Claims must be adversarial hypotheses, not observations. The test is whether you can answer this question for each claim: if the fix were absent, what exact bad thing happens to what exact memory, register, or process state?

Wrong (observation):

F(x): Memory64 module with 1-byte load
P(x-pre): boundary is zero, so the overflow check is skipped
prefixfailure: The bounds check is not performed correctly
postfixstatus: Post-fix restructures the condition

Right (falsifiable hypothesis):

F(x): Wasm Memory64 module, i32.load8_s at address 0x100000000n (bit 32 set, beyond 4GB)
P(x-pre): BBQ JIT: boundary = size + uoffset - 1 = 1 + 0 - 1 = 0. Guard condition
           isMemory64() && boundary evaluates false. branchAddPtr skipped.
           zeroExtend32ToWord() truncates 0x100000000 -> 0x00000000. Load reads mem[0].
prefixfailure: OOB read - mem[0] read without OutOfBoundsMemoryAccess trap; i32.store8 at
               0x100000000n: wild write to raw address 0x100000000 outside Wasm sandbox
postfixstatus: WasmBBQJIT64.h:113 restructured - outer isMemory64() check, inner boundary
               check, zeroExtend32ToWord() only reached if both guards clear. To be
               confirmed empirically.

Empirical Proof Requirement

No claim about pre-fix behavior is valid without runtime evidence. Source analysis is a starting point, not proof - the compiled binary may differ, the code path may not be reachable, or the optimization may change the behavior.

Required evidence for "pre-fix code allows X":

For JSC/JIT/Wasm bugs:

• A runnable probe (.js file) that produces distinguishably different output on the pre-fix vs post-fix binary
• OR: llvm-objdump disassembly showing the specific instruction sequence in the binary (not the source)
• OR: LLDB breakpoint confirming the path is/isn't taken at runtime

For DOM/IPC/WebContent bugs:

• Source grep with file:line proving the vulnerable symbol is reachable from the trigger path
• OR: LLDB breakpoint in a browser process confirming the patched line is/isn't hit during probe execution
• OR: A JS-observable side effect that distinguishes the patched from unpatched branch

"Source analysis confirms X" is not sufficient. The standard is: "Running this command produces this output, which proves X."

LLVM Coverage Confirmation

For every NO_BYPASS verdict, the patched decision point must appear as HIT in an LLVM coverage run. A probe that exits cleanly but never executes the guard it's supposedly testing is a broken test, not a passing one.

What this catches: probes that test the wrong code path, probes that exit before reaching the patched line, and probes where the JIT didn't compile the relevant function.

Coverage output format (abridged):

=== COVERAGE DELTA ===
file.cpp:N   HIT (K calls)   - [what this line does]
file.cpp:M   NOT_HIT         - [patched guard - probe did not reach this line]

If the patched line shows NOT_HIT: revise the probe until it reaches the path, then re-run. A verdict submitted with a NOT_HIT patched line will be wrong.

Adjacent Unpatched Rule

Every analysis includes an explicit search for structurally identical code that the fix did not cover. The question is: does the same bug class exist in a sibling method, a parallel JIT tier, a different process, or a related struct?

For the BBQ Memory64 boundary-zero bug, the adjacent search found:

• OMG tier (WasmOMGIRGenerator.cpp): B3::Above instead of B3::AboveEqual
  • 1-byte off-by-one, separate commit
• IPInt tier (InPlaceInterpreter64.asm): missing size - 1 in the .memoryIsNotZero path
  • up to 7-byte OOB, separate commit

The BBQ fix left both untouched. An audit that stops at the patched commit misses both.

The search should cover at minimum:

• Parallel implementations of the same operation (JIT tiers, process pairs, protocol variants)
• Sibling methods in the same class/subsystem with the same pattern
• Related structs in the same IPC serializer definition

Scoring

Scores are 1–10 based on:

• Web accessibility - can this be triggered from a normal web page?
• Primitive strength - OOB write > OOB read > UAF > DoS > info leak only
• Mitigation layers - flag gates, process sandbox, guard pages
• Confirmed primitive - empirically demonstrated vs. theorized

Findings scored ≥ 5 get a PoC. Findings scored <5 are logged with the verdict and moved on.

Score 1: SaferCPP housekeeping, no reachable attack surface
Score 3: Interesting pattern, mitigated by flag gate or defense-in-depth
Score 5: Confirmed primitive, flag-gated or limited reach
Score 7: Confirmed primitive, web-accessible, requires second stage
Score 9+: Full chain or no mitigations