fix(#953): rv32 (memory 0) must trap every access, not invent a 64 KiB bound (SECURITY)

.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)

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/'

crates/synth-backend-riscv/src/backend.rs

@@ -183,17 +183,35 @@ impl Backend for RiscVBackend {
         config: &CompileConfig,
     ) -> Result<CompiledFunction, BackendError> {
         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![

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)))
+)

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()