RQ-57-SENTINEL: sentinel/value-collision sweep — 54 sites, 4 converted, 3 latent defects fixed by avrabe · Pull Request #959 · pulseengine/synth

avrabe · 2026-08-13T15:40:12Z

What this is

The RQ-57-SENTINEL deliverable from artifacts/release-v0.57.yaml: an audit of every size/count/address path where a NUMERIC SENTINEL stands in for absence — the mechanism behind #932 (v0.56.0) and #953 (v0.56.1), two security bugs one release apart with the same root cause in opposite directions.

The number (non-vacuity)

54 sites examined / 4 converted / 41 argued-(a) / 9 listed-(c) residuals.
Full per-site table with arguments: scripts/repro/sentinel_sweep_rq57.md.

Three latent defects found and fixed (the real prize — instances three, four, five of the mechanism)

1. SECURITY — ARM --safety-bounds mask + (memory 0) = unbounded OOB read/write.
arm_backend.rs exempted bytes == 0 from the mask power-of-two gate ("0 means unknown"). A (memory 0) module bakes startup R10 = 0, so the emitted guard SUB R12, R10, #1; AND addr, R12 computes 0 − 1 = 0xFFFFFFFF — an IDENTITY mask. Every access executed unmasked at [R11 + addr] for any 32-bit address, in the mode whose purpose is bounding. Verified pre-fix on v0.56.1 (exit 0, movw r10, #0x0 baked, AND-masked bodies). Zero-byte memory now REFUSES loudly — the same contract #953 gave rv32. This is #953's disease in a third backend-mode, and worse than the 64 KiB invention: no bound at all.

2. The single-function CLI path regressed under #953.
main.rs forced linear_memory_bytes: 0 for every backend except aarch64, on a comment (from #865) claiming the field was "never consumed" by ARM/RV32 — false for RV32, whose compile_function has always read it. When #953 deleted the rv32 64 KiB fallback, --func-index + --safety-bounds software on a (memory 1) module started compiling EVERY access to the zero-size ebreak fold (pre-fix: 00050293 00100073 at entry — a live availability miscompile in v0.56.1). The declared size now threads to ALL backends; byte-invisible where unconsumed (frozen anchors are --all-exports).

3. The #932 fix's own "unreachable by construction" comment was false.
The sweep's interim .expect() on the attestation's unwrap_or(0) panicked in one test run: attestations are ALSO emitted for REFUSED ingests (#901's refusal-is-attested rule), and the imported-memory refusal — #932's exact shape — reaches the flattened 0. Shipped v0.56.x refusal attestations recorded an invented "memory_min_bytes": 0. ElisionAttestation.memory_min_bytes is now Option<u32>; absence serializes as an explicit null (accepted-case JSON unchanged).

Also converted: NativeGlobalsLayout.sp_init (0-for-absent → Option<i32>; extent folds map None → 0 as the explicit max-identity, and --shadow-stack-size on a module with no SP global now refuses loudly instead of shrinking a phantom reservation).

The 9 (c)-residuals, listed not silent

Highest blast radius first (details + guardians in the sweep doc): imported-memory modules get linear_memory_bytes = 0 → silent always-trap compiles on rv32/aarch64 (fail-closed, but the "tell the caller" class — ties to the #932 decoder follow-up); the cortex-m image's initial_pages.unwrap_or(1); the emit_wasm_data && linear_memory_bytes > 0 region-skip; decoder type-table .get().unwrap_or(0) (guarded by wasmparser validation); validator_pattern arity; arm_backend param-table defaults (#518's mechanism, guarded by the CLI always populating); provenance/ELF-name diagnostic flatteners.

Red-first evidence

All three defects demonstrated on the pre-fix tree before conversion (transcripts in the sweep doc). New tests:

arm_safety_bounds_mask_zero_size_refused_rq57 (unit) + arm_mask_zero_memory_refused (CLI, end-to-end reachability)
rv32_single_func_software_uses_declared_bound + non-vacuity control rv32_single_func_zero_memory_stays_fail_closed (proves the fix threads the declared size rather than resurrecting a fallback — (memory 0) keeps the [SECURITY] rv32: (memory 0) gets a 65532-byte bounds guard — --safety-bounds software is a 64KB no-op for reads AND writes (aarch64 folds to brk) #953 ebreak fold)
no_floor_attests_null_not_zero_rq57 (attestation null, invented-0 unrepresentable)

Gates

cargo fmt --check clean; cargo clippy --workspace --all-targets -- -D warnings exit 0 (real exit code)
cargo test --workspace exit 0 (136 suites, 0 failures)
frozen_codegen_bytes 10/10 — the Option refactors moved no shipping bytes
Two pre-existing mask tests updated to STATE their size (linear_memory_bytes: 64 * 1024) — exactly what the [SECURITY] rv32: (memory 0) gets a 65532-byte bounds guard — --safety-bounds software is a 64KB no-op for reads AND writes (aarch64 folds to brk) #953 fix required of the rv32 driver test

Refs #953, #932

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

… defects found and fixed Audit of every size/count/address path where a numeric sentinel stands in for absence (the #932/#953 disease), across synth-core, synth-backend, synth-backend-riscv, synth-backend-aarch64, synth-cli, synth-verify. 54 sites examined / 4 converted / 41 argued-(a) / 9 listed-(c) residuals. Full table: scripts/repro/sentinel_sweep_rq57.md TWO LATENT DEFECTS found by the sweep (the third and fourth instances of the mechanism, one release after #953): 1. SECURITY — ARM `--safety-bounds mask` exempted `bytes == 0` from the power-of-two gate ("0 means unknown"). A `(memory 0)` module compiled with startup R10 = 0, so the emitted guard `SUB R12, R10, #1; AND` computed an IDENTITY mask (0xFFFFFFFF): every access executed unmasked at [R11 + addr] — unbounded OOB read/write in the mode whose purpose is bounding. Verified pre-fix (exit 0, movw r10 #0 baked). Zero-byte memory now REFUSES loudly, same contract as #953 gave rv32. 2. The single-function CLI path forced `linear_memory_bytes: 0` for every backend but aarch64, on a comment claiming the field was never consumed there — FALSE for RV32, whose compile_function reads it for the bound. After #953 removed the rv32 fallback, `--func-index` + software bounds on a `(memory 1)` module compiled every access to the zero-size ebreak fold (verified pre-fix: 00050293 00100073 at entry). The declared size now threads to ALL backends; `(memory 0)` keeps the fail-closed fold (pinned by a control test). Also converted: the #932 attestation `unwrap_or(0)` (documented-unreachable → expect, so acceptance-rule drift panics instead of attesting an invented 0 B floor) and `NativeGlobalsLayout.sp_init` (0-for-absent → Option<i32>; the shadow-stack shrink now refuses "no SP global" loudly). Red-first: both defects demonstrated on the pre-fix tree (transcripts in the sweep doc); new tests arm_safety_bounds_mask_zero_size_refused_rq57 + sentinel_sweep_rq57.rs (3 CLI tests incl. the non-vacuity control). Refs #953, #932 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…— type the absence The sweep's interim `.expect()` disproved the #932-era "unreachable by construction" comment in one test run: attestations are also emitted for REFUSED ingests (#901's refusal-is-attested rule), and the imported-memory refusal — #932's exact shape — reached the flattened 0. Shipped v0.56.x refusal attestations therefore recorded an invented `"memory_min_bytes": 0`. `ElisionAttestation.memory_min_bytes` is now `Option<u32>`; absence serializes as an explicit `null` (pinned by no_floor_attests_null_not_zero_rq57; the accepted-case JSON shape is unchanged — Some(x) is the bare number, proven_safe_bounds_901 still asserts 65536). Third latent defect found by this sweep. Refs #953, #932 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…lure) CI red on `Test`; the lane's local run was green. Both new assertions failed with `words: []` — an EMPTY word list, not a wrong one. Cause: the helper parsed `synth disasm` OUTPUT. The disassembler decodes with whatever target it defaults to and its rendering is host-dependent, so the parser matched on macOS and matched nothing on the ubuntu runner. This is #850, already recorded in this repo — and it is the SECOND time this exact trap has landed in a test I am responsible for: v0.56's #932 fixture counted `udf` mnemonics from `synth disasm`, passed on macOS, and returned 0 on ubuntu. Same mechanism, same month. Now reads the ELF `.text` SECTION BYTES via `object::{Object, ObjectSection}` (already a dev-dependency) and formats 4-byte little-endian words. That is host-independent BY CONSTRUCTION rather than by luck: synth is a cross-compiler and `.text` is a pure function of (wasm, flags) — the same property `frozen_codegen_bytes` relies on, which is why THAT test passes in CI while this one did not. The assertions are unchanged and still match the same encodings (`00010337` = lui t1,0x10 and `ffc30313` = addi t1,t1,-4), so the lane's red-first evidence still stands; only the reading mechanism moved. cargo test -p synth-cli --test sentinel_sweep_rq57 -> 3 passed, 0 failed Refs #953, #850

codecov · 2026-08-13T16:08:33Z

Codecov Report

❌ Patch coverage is 98.90110% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	96.96%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

Pulls four merged commits forward into a patch release because the first is a live vulnerability in a shipped version: #959 ARM --safety-bounds mask emitted an IDENTITY mask on (memory 0) #961 thumb-2 branch target could land mid-instruction (#930) #962 I64Const/I64Ldr/I64Str unpriced in the WCET model (#936) #958 synth verify covers i32.const + reports the decline denominator The ARM mask bug is the headline. The mask path exempted `bytes == 0` from its power-of-two gate, so `(memory 0)` compiled with exit 0 and `movw r10, #0x0`. The guard computes `R10 - 1`, and `0 - 1` is `0xFFFFFFFF` — a mask that masks nothing, in the mode whose whole purpose is to bound accesses. Unbounded OOB read AND write. It is the same sentinel/value collision as #953 one release earlier, running the other way: there `0` meant "unset" and INVENTED a 64 KiB bound, here `0` meant "no bound needed" and ERASED the real one. That is why the fix landed as a sweep of the collision class (54 sites, 4 converted, 3 latent defects) and not another point patch — the v0.53 finding was that we keep fixing instances rather than mechanisms. Release surfaces, all four swept to 0.56.2 and checker-confirmed: Cargo.toml [workspace.package] + 10 path-dep version= pins MODULE.bazel, npm/package.json, Cargo.lock (cargo metadata) scripts/check_version_pins.py: OK on all four Derived artifacts regenerated (--emit-status): artifacts/status.json, docs/status/FEATURE_MATRIX.md. Claim gate: 43/43. SCOPE MOVE, logged not silent: RQ-57-SENTINEL, RQ-57-BRTARGET, RQ-57-WCET2OPS, RQ-57-I32CONST and RQ-57-RULEINV were planned for v0.57 and are re-tagged release: v0.56.2 / status: implemented. SENTINEL carried the security fix and the other four were already merged on main, so a tag excluding them did not exist. rivet error/warning counts are unchanged by the move (50/164 before and after — pre-existing, unrelated to these artifacts). Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

… (RQ-57-MCDC) (#978) * feat(#912): MC/DC structural coverage over synth's own decision logic RQ-57-MCDC. #912 sat N/A for six releases on a surface argument: `witness` measures MC/DC on a Wasm artifact and synth emits ARM/RV32/A64 machine code, so "run witness on synth's output" is a category error. That is true about synth's OUTPUT and irrelevant — the decisions that ship a miscompile are in synth's own Rust, and those compile to Wasm fine. SURFACE, chosen on evidence (scripts/repro/mcdc_912_gate.md): * REJECTED native LLVM MC/DC — not a preference, the capability was REMOVED from rustc (rust-lang/rust#144999, merged 2025-08-08, Rust 1.91). Probed on three nightlies: `mcdc` is rejected, only `block|branch|condition` accepted. `condition` is the trap in the family — it builds, and it emits ZERO `llvm.instrprof.mcdc.*` intrinsics and zero mcdc_records. * REJECTED witness-over-the-fixtures-synth-compiles — it measures the fixture. gale's run named `pad_integral`, `do_count_chars`, `<u64 as Display>::fmt`, `write_prefix`, `cabi_realloc` and ZERO synth functions. A surface whose gap rows cannot name a synth decision cannot notice a missing condition in one. * CHOSEN witness over a wasm32-wasip1 build of synth's OWN crates. `synth-mcdc-harness` is a thin row driver — it calls the REAL pub fns with inputs arriving through Wasm params; it re-implements no predicate. THE RIGHT PARTS — scored where a missed condition HAS shipped a bug here: static_data_addr (VCR-VER-003 #777/#757/#798), alloc_validator (VCR-RA-003 #815; #871's fix WAS a condition added to the save-set predicate), and the RV32 bounds gate (#953/#959 — `mem_size == 0` was exempt from the power-of-two check, so `(memory 0)` emitted an identity mask and every access ran unmasked). EXCLUDED and named: instruction_selector (225 operator lines, its own lane); the aarch64 bounds closures (#865 — residual); wcet declines (match-dispatch, 1 operator line in 1061, so MC/DC has nothing to say there). MEASURED 20 decisions / 144 conditions / 63 proved / 31 gap / 50 dead, 3 at full MC/DC. Identical under witness 0.28.0 and 0.42.0. Gap rows are PRINTED with the closing vector — `is_ret` went 3-gap to 0-gap by adding exactly the three vectors witness named. THE GATE SCORES BY FUNCTION AND FLOORS COUNTS, for three reasons: the module-wide figure is 3/770 because wasip1 links wasi-libc + std; witness's `source_file` is an inlined-DWARF BASENAME and misattributes (resolve_owner's decision reports as static_data_addr.rs:355, it is at :274 — witness#179); and a ratio cannot notice a DELETED condition, which makes the percentage improve. RED-FIRST, two mutations, two distinct failure paths, both restored byte-identical: (a) delete `|| rs2 == Reg::RA` (the #871 fix) -> 19/142/54/2, all four floors trip; the condition-COUNT drop is what a ratio cannot produce. (b) drop one truth-table row (ra_validate:14) -> conditions stay 144, proved 63->62 and fully-proved 3->2. Wired as the `mcdc-structural-coverage` CI job, witness pinned to v0.42.0, with a non-vacuity assert so an empty scored table cannot print PASS. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#912): CI mode-126 on mcdc_run.sh, pin the toolchain, ceiling the dead count Three fixes from the first CI run and the cold read of it: 1. exit 126. `scripts/` is mode 644 in this repo (cf. scripts/oracle_run.py), so `./scripts/mcdc_run.sh` cannot exec on a fresh checkout even though it runs locally after a chmod. Invoke through `bash`, matching how every other script in this workflow is called. 2. PIN the toolchain to 1.96.1. The floors are counts of decisions and conditions RECONSTRUCTED FROM LOWERED WASM, so they are sensitive to how `std` inlines. `@stable` is a moving target and a Rust release could red this gate with no code change. Bumping the pin is allowed and obliges a RE-MEASURE, not a lowering. (Witness-version invariance — 0.28 = 0.42 — is evidence about witness, not about rustc; it does not transfer.) 3. CEILING the dead count at the measured 50. 50 of 144 scored conditions are never evaluated (40 in `is_straight_line`, whose match arms cover RV32 opcodes the row set does not construct). That residual was the one number in the table nothing guarded: a change that stopped reaching the segment barriers would raise `dead`, lower nothing else, and PASS. It is also a third potency surface — mutation (a) moves dead 50 -> 52, so the mutated run now trips five floors instead of four. Also trims the `sd_resolve_owner` doc comment, which claimed vectors the measurement does not show: its 2 gap conditions are now stated as a measured residual rather than implied closed. Baseline re-verified unchanged: 20 / 3 / 144 / 63 / 31 / 50, PASS. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * TEMPORARY red-first probe (#912) — DO NOT MERGE THIS COMMIT Reverted by the very next commit. Two things in one CI run: 1. RE-MEASURE the floors on the platform the gate actually runs on. The first CI run proved what could only be argued locally: these counts are PLATFORM-dependent, not just toolchain-version dependent. ubuntu x86_64, rustc 1.96.1, witness 0.42.0: 22 / 130 / 57 / 23 gap / 50 dead, 4 full macOS aarch64, rustc 1.96.1, witness 0.42.0: 20 / 144 / 63 / 31 gap / 50 dead, 3 full Same toolchain version, same witness, same 56 rows, different host. `validate_final_allocation_rv32` presents as 9 decisions / 44 conditions on Linux and 4 / 43 on macOS; `ensure_supported_target` vanishes on Linux. Floors move to the CI numbers — RE-MEASURED, not lowered to fit. Both baselines are recorded in the script so the macOS delta is a stated fact rather than a surprise. 2. RE-PROVE POTENCY ON THAT PLATFORM. The local mutation evidence does NOT obviously transfer when the same function presents as 9 decisions instead of 4 — and "it obviously still works" is the reasoning this whole lane exists to distrust. So this commit ALSO deletes the #871 condition `|| rs2 == Reg::RA` from the RV32 allocation validator's save-set predicate. The MC/DC job must go RED on the condition-COUNT floor, and the VCR-RA-003 RV32 job should go red independently. If this commit is green, the gate is vacuous and the lane is wrong. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * TEMPORARY red-first probe 2/2 (#912) — DO NOT MERGE, reverted next commit Probe 1 (25a9195) went RED on CI as required, but at the WRONG STEP for the evidence I wanted: the row-driver sanity gate (step 7) asserts `ra_validate(4) == 1` (#871: unsaved ra must be a violation), so deleting `|| rs2 == Reg::RA` fails there and the MC/DC measurement never runs. Two independent gates catching one mutation is good engineering and useless as proof that the MC/DC FLOORS bite. This probe isolates them. It restores the source byte-identical (verified: empty `git diff` vs the pre-mutation tree) and instead drops ONE truth-table row — `ra_validate:14`, the non-sp `Lw` that gives `sp_slot_load` its unique-cause pair. That touches no compiler behaviour, so: step 7 (row-driver sanity) must PASS step 8 (witness run) must PASS step 9 (MC/DC floors) must FAIL on and Conditions must stay at 130 — coverage lost, nothing deleted. That is the second of the two potency paths, and the one that proves the SCORING floor itself is what goes red, on the platform it actually runs on. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(#912): restore the probes, record the CI-platform potency evidence Both red-first probes reverted; the tree is byte-identical to 712f658 for crates/synth-backend-riscv/src/alloc_validator.rs and scripts/mcdc_run.sh (verified with an empty \$(git diff 712f658 -- <path>) on each). What the two CI probes established, which the local run could not: PROBE 1 (delete the #871 condition) went RED — at the WRONG STEP. The job's own row-driver sanity gate asserts ra_validate(4) == 1 and fails there, so the MC/DC measurement never ran; the VCR-RA-003 RV32 job went red independently too. Three gates catching one mutation is good engineering and NO evidence that the MC/DC floors bite. Recording it because 'a red gate is not evidence that the gate you were testing works' generalises well past this lane — read WHICH STEP failed. PROBE 2 (drop one truth-table row, no compiler behaviour touched) isolated them. Run 31821746035: sanity gate PASS, witness run PASS, SCORING STEP FAIL. baseline 22 4 130 57 23 50 probe 2 22 3 130 56 24 50 FAIL: proved conditions 56 < floor 57 FAIL: fully-proved decisions 3 < floor 4 Decisions unchanged, CONDITIONS UNCHANGED at 130 — nothing deleted — while proved fell and a decision dropped out of full MC/DC. That is the signature of coverage lost with structure intact, produced by the MC/DC scoring step itself, on the platform the gate blocks on. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

avrabe and others added 3 commits August 13, 2026 17:29

avrabe merged commit 8b4808b into main Aug 13, 2026
58 checks passed

avrabe deleted the feat/sentinel-sweep-953 branch August 13, 2026 16:57

avrabe mentioned this pull request Aug 13, 2026

chore(release): v0.56.2 — security + soundness patch #964

Merged

Navigation Menu

Uh oh!

RQ-57-SENTINEL: sentinel/value-collision sweep — 54 sites, 4 converted, 3 latent defects fixed - #959

RQ-57-SENTINEL: sentinel/value-collision sweep — 54 sites, 4 converted, 3 latent defects fixed#959
avrabe merged 3 commits into
mainfrom
feat/sentinel-sweep-953

avrabe commented Aug 13, 2026

Uh oh!

codecov Bot commented Aug 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

avrabe commented Aug 13, 2026

What this is

The number (non-vacuity)

Three latent defects found and fixed (the real prize — instances three, four, five of the mechanism)

The 9 (c)-residuals, listed not silent

Red-first evidence

Gates

Uh oh!

codecov Bot commented Aug 13, 2026

Codecov Report

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant