From 420f126f6fc4f2a6aaa3abecd57e290d2d518536 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 12 Aug 2026 21:58:29 +0200 Subject: [PATCH] fix(#953): rv32 `(memory 0)` must trap every access, not invent a 64 KiB bound (SECURITY) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A module declaring `(memory 0)` got a bound baked at 65532 — byte-for-byte the guard of a 1-page module — so every address in 0..=65532 passed the `--safety-bounds software` check and the access was performed against a memory with no bytes. Reads AND writes. Reported by gale (#953) 30 minutes after v0.56.0 published; reproduced on the shipped tag. ## Root cause: `0` as both a value and a sentinel let mem_size = if config.linear_memory_bytes > 0 { .. } else { 64 * 1024 }; The fallback's stated purpose is real — a hand-built driver with no module context still needs a bound. But `0` is ALSO exactly what `(memory 0)` produces, and the two are indistinguishable, so it invented a bound for a module that declared none. **Same disease as #932, fixed one release earlier, running the other way.** There `unwrap_or(0)` turned "no floor establishable" into "the floor is 0 bytes" and STRIPPED guards; here `0` meant "unset" and INVENTED one. ## Why deleting the fallback is the fix, not a workaround Measured rather than assumed. With it removed, exactly ONE test in the tree failed — and the bytes it rejected contained `0x00100073` (`ebreak`): rv32 already folds to an unconditional trap at size 0, which is the correct answer and precisely what aarch64 does (`brk #0`). The other two backends were right all along: aarch64 reads the value raw, ARM derives its bound from a runtime register with an underflow check. rv32 was the anomaly. So the contract is now: `linear_memory_bytes` is the size, full stop; 0 means zero bytes. A caller with no module context states the size — which is what a real driver does, and what the one affected test now does. Leaving it 0 fails CLOSED (everything traps) rather than open. ## Evidence — red-first, executed against wasmtime `scripts/repro/rv32_zero_memory_953_differential.py`, CI-wired. 9 vectors across load/store/load8, each asserting synth TRAPS iff wasmtime traps — a trap is observed as a real `ebreak` intercept, not as "the value came back wrong", which would pass vacuously if the function returned 0 for an unrelated reason. pre-fix 6/9 FAIL (ld/st/ld8 at 0 and at 65528 all performed the access) post-fix 9/9 PASS The three 65536 vectors are the NON-VACUITY control: they trapped before the fix too, so the fixture is demonstrably not just trapping on everything. synth-backend-riscv 259 passed / 0 failed; frozen anchors 10/10; clippy clean. Emulation-floor ledger 295701 -> 295710 in both surfaces. The instance is fixed here. The MECHANISM — every numeric sentinel that means both a value and its own absence — is RQ-57-SENTINEL, and it must produce a count of sites examined and converted or it has not been done. Closes #953 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 6 +- claims.yaml | 2 +- crates/synth-backend-riscv/src/backend.rs | 47 ++++-- scripts/repro/rv32_zero_memory_953.wat | 31 ++++ .../rv32_zero_memory_953_differential.py | 145 ++++++++++++++++++ 5 files changed, 218 insertions(+), 13 deletions(-) create mode 100644 scripts/repro/rv32_zero_memory_953.wat create mode 100644 scripts/repro/rv32_zero_memory_953_differential.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0ce129fd..66e8972e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -260,7 +260,7 @@ jobs: run: | set -euo pipefail python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \ - --min-emulation-floor 295701 \ + --min-emulation-floor 295710 \ | tee /tmp/oracle-wiring.log python3 - <<'PY' import json, sys @@ -3355,6 +3355,10 @@ jobs: run: | ./target/debug/synth compile scripts/repro/rv32_br_value_931.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/br931.o python scripts/oracle_run.py scripts/repro/rv32_br_value_931_differential.py /tmp/br931.o + - name: RV32 zero-page memory traps every access (#953, SECURITY) + run: | + ./target/debug/synth compile scripts/repro/rv32_zero_memory_953.wat -b riscv -t rv32imac --safety-bounds software --all-exports --relocatable -o /tmp/z953.o + python scripts/oracle_run.py scripts/repro/rv32_zero_memory_953_differential.py /tmp/z953.o - name: RV32 mask/software bounds effective-address oracle (#655) run: python scripts/oracle_run.py scripts/repro/mask_bounds_655_riscv_differential.py - name: RV32 cmp->select fusion differential (#472) diff --git a/claims.yaml b/claims.yaml index c3ea316c..9f02a66c 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1133,7 +1133,7 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910-CI doc: .github/workflows/ci.yml - text: "--min-emulation-floor 295701" + text: "--min-emulation-floor 295710" evidence: - kind: count-min # oracle steps routed through the driver pattern: 'oracle_run\.py scripts/repro/' diff --git a/crates/synth-backend-riscv/src/backend.rs b/crates/synth-backend-riscv/src/backend.rs index 4ee20d56..406ffead 100644 --- a/crates/synth-backend-riscv/src/backend.rs +++ b/crates/synth-backend-riscv/src/backend.rs @@ -183,17 +183,35 @@ impl Backend for RiscVBackend { config: &CompileConfig, ) -> Result { ensure_supported_target(&config.target)?; - // Prefer the config's declared linear-memory size (the CLI populates it - // from the module's first memory — `--all-exports` compiles per function - // through here, NOT `compile_module`, so `memory.size` must read it from - // the config to report the right page count). Fall back to 1 wasm page - // when unset (a hand-built driver with no module context) so - // Software/Mask bounds modes can still synthesise their guard. - let mem_size = if config.linear_memory_bytes > 0 { - config.linear_memory_bytes - } else { - 64 * 1024 - }; + // #953 (SECURITY): `linear_memory_bytes` is the memory size, FULL STOP. + // Zero means zero bytes — it is NOT a sentinel for "unset". + // + // This used to fall back to 1 wasm page when the value was 0, for "a + // hand-built driver with no module context". But 0 is also exactly what + // a module legitimately declaring `(memory 0)` produces, and the two + // were indistinguishable — so the fallback INVENTED a 65532-byte bound + // for a module that declared none, and every address in 0..=65532 + // passed the `--safety-bounds software` guard for a memory with no + // bytes. Reads and writes both. + // + // That is the #932 disease running the other way, one release later: + // there `unwrap_or(0)` turned "no floor establishable" into "the floor + // is 0 bytes" and STRIPPED guards; here 0 meant "unset" and INVENTED + // one. A number that means both a value and its own absence will keep + // producing this. + // + // The other two backends already do it this way and are correct: + // aarch64 reads `config.linear_memory_bytes` raw (and folds to an + // unconditional `brk` at size 0, since with zero pages every access is + // statically out of bounds), and ARM derives its bound from a runtime + // register with an underflow check. rv32 was the anomaly. + // + // CONTRACT for callers with no module context: state the size. Leaving + // it 0 now means "zero-byte memory" and every access traps — which + // fails CLOSED. Exactly one in-tree caller relied on the old fallback + // (`compile_with_software_bounds_emits_bgeu_in_function_bytes`); it now + // sets the size explicitly, which is what a real driver would do. + let mem_size = config.linear_memory_bytes; let opts = build_options(config, mem_size)?; compile_function_with_opts(name, ops, config, opts) } @@ -664,10 +682,17 @@ mod tests { fn compile_with_software_bounds_emits_bgeu_in_function_bytes() { // i32.load + safety-bounds software should produce a 32-bit instruction // whose lowest 7 bits == 0b1100011 (BRANCH opcode). + // + // #953: this is the ONE in-tree caller that relied on + // `linear_memory_bytes == 0` meaning "unset, assume a page". It now + // states the size, which is what a real hand-built driver would do. + // Left at 0 it would (correctly) emit an unconditional trap instead of + // a conditional guard, because 0 now means a zero-byte memory. let b = RiscVBackend::new(); let cfg = CompileConfig { target: TargetSpec::riscv32imac(), safety_bounds: SafetyBounds::Software, + linear_memory_bytes: 64 * 1024, ..Default::default() }; let ops = vec![ diff --git a/scripts/repro/rv32_zero_memory_953.wat b/scripts/repro/rv32_zero_memory_953.wat new file mode 100644 index 00000000..a0832211 --- /dev/null +++ b/scripts/repro/rv32_zero_memory_953.wat @@ -0,0 +1,31 @@ +;; #953 (SECURITY) — a module that declares ZERO pages of linear memory. +;; +;; Every address is out of bounds of a 0-byte memory, so under +;; `--safety-bounds software` every access must trap. wasmtime traps for all of +;; these; on v0.56.0 rv32 performed all of them, because the guard was baked at +;; 65532 — byte-for-byte the guard of a 1-page module. +;; +;; The address values below are chosen to straddle the invented bound rather +;; than to look adversarial: 0 is the friendliest possible address and was +;; accepted; 65528 is the last 4-byte-aligned address INSIDE the invented +;; 65532 bound and was accepted; 65536 is past it and was already trapping, so +;; it is the control that proves the guard existed at all and that the fixture +;; is not simply trapping on everything for an unrelated reason. +(module + (memory 0) + + (func (export "ld") (param $a i32) (result i32) + (i32.load (local.get $a))) + + ;; Stores emit the identical bound, so this is an out-of-bounds WRITE and not + ;; only a read. Returns the value it stored so a trap is distinguishable from + ;; a silent no-op. + (func (export "st") (param $a i32) (result i32) + (i32.store (local.get $a) (i32.const 42)) + (i32.const 42)) + + ;; Sub-word accesses take a different guard path (width-adjusted bound), so + ;; they are exercised too rather than assumed to follow the i32 case. + (func (export "ld8") (param $a i32) (result i32) + (i32.load8_u (local.get $a))) +) diff --git a/scripts/repro/rv32_zero_memory_953_differential.py b/scripts/repro/rv32_zero_memory_953_differential.py new file mode 100644 index 00000000..79365134 --- /dev/null +++ b/scripts/repro/rv32_zero_memory_953_differential.py @@ -0,0 +1,145 @@ +#!/usr/bin/env python3 +# ci-status: wired +# ci-checks: emulations >= 9 +"""#953 (SECURITY) — rv32 `(memory 0)` got a 65532-byte bounds guard. + +`--safety-bounds software` is the mode whose entire purpose is to make every +out-of-bounds access trap. On v0.56.0, a module declaring `(memory 0)` got a +bound baked at **65532** — byte-for-byte the guard of a 1-page module — so every +address in `0..=65532` passed the check and the access was performed against a +memory with no bytes at all. Reads AND writes: + + lui t1, 0x10 ; 65536 + addi t1, t1, -0x4 ; 65532 <- bound for a ZERO-byte memory + bltu t1, t0, ... ; trap only if 65532 < addr + +ROOT CAUSE: `0` used as both a value and a sentinel. +`config.linear_memory_bytes == 0` meant "unset — a hand-built driver with no +module context, fall back to 1 page" AND is exactly what `(memory 0)` produces. +The two were indistinguishable. + +This is the same disease as #932 (fixed one release earlier) running the other +way: there `unwrap_or(0)` turned "no floor establishable" into "the floor is 0 +bytes" and STRIPPED guards; here `0` meant "unset" and INVENTED one. + +# What this oracle asserts, and why it is shaped this way + +wasmtime is the reference: it traps on every access to a zero-byte memory. The +compiled function must do the same. A trap is observed as a unicorn `ebreak` +intercept, NOT as "the value came back wrong" — a wrong-value check would pass +vacuously if the function returned 0 for an unrelated reason. + +The 65536 vector is the NON-VACUITY control: it was already trapping before the +fix, so if it ever stops trapping the fixture has broken in a way that would +make the other vectors meaningless. +""" + +import struct +import sys + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_RISCV, UC_HOOK_INTR, UC_MODE_RISCV32, Uc, UcError +from unicorn.riscv_const import UC_RISCV_REG_A0, UC_RISCV_REG_RA, UC_RISCV_REG_S11, UC_RISCV_REG_SP + +WAT = "scripts/repro/rv32_zero_memory_953.wat" +ELF = sys.argv[1] if len(sys.argv) > 1 else "/tmp/z953.o" + +CODE, LIN, RET = 0x100000, 0x40000, 0x200000 + +# (export, address). Every one must TRAP: the memory has zero bytes. +# 0 — the friendliest possible address; accepted pre-fix. +# 65528 — last aligned address inside the INVENTED 65532 bound; accepted. +# 65536 — past the invented bound; already trapped pre-fix (the control). +VECTORS = [ + ("ld", 0), + ("ld", 65528), + ("ld", 65536), + ("st", 0), + ("st", 65528), + ("st", 65536), + ("ld8", 0), + ("ld8", 65531), + ("ld8", 65536), +] + + +def symbols(path): + with open(path, "rb") as fh: + f = ELFFile(fh) + st = f.get_section_by_name(".symtab") + syms = { + s.name: s["st_value"] + for s in st.iter_symbols() + if s.name and s["st_info"]["type"] == "STT_FUNC" + } + return syms, f.get_section_by_name(".text").data() + + +def main(): + engine = wasmtime.Engine() + module = wasmtime.Module.from_file(engine, WAT) + + def wasmtime_traps(name, addr): + store = wasmtime.Store(engine) + inst = wasmtime.Instance(store, module, []) + try: + inst.exports(store)[name](store, addr) + return False + except Exception: + return True + + syms, code = symbols(ELF) + + def synth_traps(name, addr): + """True if the compiled function traps (ebreak) at this address.""" + entry = syms.get(name) + if entry is None: + return None # function skipped — a decline, not a trap + mu = Uc(UC_ARCH_RISCV, UC_MODE_RISCV32) + for base, size in [(CODE, 0x20000), (LIN, 0x20000), (0x88000, 0x10000), (RET, 0x1000)]: + mu.mem_map(base, size) + mu.mem_write(CODE, code) + mu.reg_write(UC_RISCV_REG_SP, 0x90000) + mu.reg_write(UC_RISCV_REG_S11, LIN) + mu.reg_write(UC_RISCV_REG_A0, addr & 0xFFFFFFFF) + mu.reg_write(UC_RISCV_REG_RA, RET) + trapped = [] + mu.hook_add(UC_HOOK_INTR, lambda *_: trapped.append(True)) + try: + mu.emu_start(CODE + entry, RET, count=4000) + except UcError: + # A fault reaching unicorn is also a refusal to perform the access. + return True + return bool(trapped) + + fails = executed = 0 + for name, addr in VECTORS: + want = wasmtime_traps(name, addr) + got = synth_traps(name, addr) + if got is None: + print(f" {name}({addr}): SYMBOL MISSING — function skipped, not trapped") + fails += 1 + continue + executed += 1 + ok = got == want + fails += 0 if ok else 1 + print( + f" {name}({addr}): synth_traps={got} wasmtime_traps={want} " + f"{'OK' if ok else '*** ACCESS PERFORMED ON A ZERO-BYTE MEMORY ***'}" + ) + + print(f"\n#953 EMULATIONS={executed}/{len(VECTORS)}") + if executed != len(VECTORS): + print(f"FAIL: only {executed} of {len(VECTORS)} vectors reached the emulator") + sys.exit(1) + print( + "RESULT: PASS — every access to a zero-byte memory traps, matching wasmtime" + if not fails + else f"FAIL: {fails} vector(s) disagree with wasmtime" + ) + sys.exit(1 if fails else 0) + + +if __name__ == "__main__": + main()