From 9d662581cf1722b83e3d53a7762831937ac98f2c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 21:40:28 +0200 Subject: [PATCH 1/2] fix(#932): --proven-safe must never elide against a floor it invented (SECURITY) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For a module whose memory is IMPORTED the derived floor was all_memories.first().map(|m| m.initial_bytes()).unwrap_or(0) and imported memories are not in `all_memories`, so `unwrap_or(0)` turned 'no floor can be established' into 'the floor is 0 bytes'. Measured on v0.55.0: baseline, no --proven-safe .......... 2 udf guards memory_min_bytes = 0 ACCEPTED ... 0 udf guards <-- guards STRIPPED memory_min_bytes = 65536 REFUSED .... 2 udf guards <-- the TRUTH rejected The fail-closed contract INVERTED: the honest document rejected, the vacuous one stripping real guards, while synth printed 'proved 1 access site in-bounds against the 0 B floor' — self-refuting, since no access is in bounds of a zero-byte memory. An imported memory is real at run time, so that is an unguarded access at an attacker-controlled offset. The floor is now Option and None REFUSES. Absence of evidence is never evidence of safety — the rule the rest of this seam states and this line broke. MY FIRST TEST WAS VACUOUS, and mutation caught it: it used a dummy hash, so every compile was refused at the HASH gate and the guards survived for a reason unrelated to #932 — reverting the fix did NOT fail it. It now scrapes the real hash from synth's own diagnostic so the hash gate PASSES and the floor check is the only thing that can refuse. Re-verified: reverting the fix reproduces 'ACCEPTED ... against the 0 B floor' and the test fails. That required a product change too: the floor refusal now reports the computed hash, which a consumer debugging a rejected document needs anyway. NO REGRESSION: a DECLARED memory still accepts a truthful document and elides 2 -> 0 guards against the real 65536 B floor, asserted by the second test so this fix cannot be mistaken for deleting the feature. NAMED RESIDUAL, not silent: the truthful document for an IMPORTED memory is still refused, because the decoder discards the import's declared minimum (TypeRef::Memory(_) -> ImportKind::Memory). Safe but not yet useful; carrying the minimum through is tracked on #932. ROOT CAUSE OF THE MISS: the #901 differential used a DECLARED memory, so the imported shape was never exercised — the v0.53 lesson that a validator tests the shape it was written against. clippy 0, fmt 0, 2/2 tests, red-first verified. Refs #932, RQ-56-PSAFE --- crates/synth-cli/src/main.rs | 58 ++++- .../tests/proven_safe_imported_memory_932.rs | 222 ++++++++++++++++++ crates/synth-core/src/proven_safe.rs | 9 + 3 files changed, 285 insertions(+), 4 deletions(-) create mode 100644 crates/synth-cli/tests/proven_safe_imported_memory_932.rs diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index bdb86628..f3d94f34 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -3328,7 +3328,32 @@ fn compile_all_exports( // (post-`.wat`-parse, post-loom, post-#418 arena-bind), so a pre-compile // rewrite that shifts operator indices also breaks the hash — index skew // and byte skew are one gate. - let proven_safe_module_min_bytes = all_memories.first().map(|m| m.initial_bytes()).unwrap_or(0); + // #932 (CRITICAL/SECURITY): this was + // all_memories.first().map(|m| m.initial_bytes()).unwrap_or(0) + // and `unwrap_or(0)` turned "no floor can be established" into "the floor + // is 0 bytes". An IMPORTED memory is not in `all_memories` (imports land in + // `all_imports`), so for `(import "env" "memory" (memory 1))` the derived + // floor was 0 — and then: + // + // memory_min_bytes = 0 -> ACCEPTED, 2 udf guards -> 0 (STRIPPED) + // memory_min_bytes = 65536 -> REFUSED, guards kept (the TRUTH) + // + // i.e. the fail-closed contract INVERTED: the honest document was rejected + // and the vacuous one stripped real guards, with synth printing "proved 1 + // access site in-bounds against the 0 B floor" — self-refuting, since no + // access is in bounds of a zero-byte memory. An imported memory is real at + // run time, so that is an unguarded access at an attacker-controlled offset. + // + // A floor synth cannot ESTABLISH is now `None`, and `None` REFUSES. Absence + // of evidence is never evidence of safety — the same rule the rest of this + // seam already states and this line quietly broke. + // + // FOLLOW-UP (named, not silent): an imported memory declares its own + // minimum, but the decoder discards it (`TypeRef::Memory(_)` -> + // `ImportKind::Memory`), so the truthful document still cannot be accepted + // for imported memory — it is REFUSED, which is safe but not yet useful. + // Carrying the declared minimum through is tracked on #932. + let proven_safe_module_min_bytes: Option = all_memories.first().map(|m| m.initial_bytes()); let proven_safe_ingest: Option = proven_safe.as_ref().map(|path| { let module_bytes: &[u8] = sbom_wasm_bytes.as_deref().unwrap_or(&[]); @@ -3338,8 +3363,29 @@ fn compile_all_exports( path.display() ); } - let r = - synth_core::proven_safe::ingest(path, module_bytes, proven_safe_module_min_bytes); + let Some(min_bytes) = proven_safe_module_min_bytes else { + // #932: no DEFINED memory, so no floor synth can stand behind. + // The computed hash is reported even on this refusal: a + // consumer debugging a rejected document should not have to + // provoke a DIFFERENT refusal to learn what synth hashed, and + // #932's own regression test needs it to construct a document + // that reaches the floor check rather than dying at the hash. + eprintln!( + "warning: --proven-safe {}: this module defines no linear memory \ + (an imported memory declares its minimum elsewhere, which synth \ + does not yet carry), so NO memory floor can be established; NO \ + bounds guard is elided (fail closed). This compile's module \ + hashes to {}.", + path.display(), + synth_core::proven_safe::hex_sha256(module_bytes) + ); + return synth_core::proven_safe::ProvenSafeIngest::refused( + "no linear memory is DEFINED by this module, so no memory floor \ + can be established; refusing rather than validating verdicts \ + against a 0 B floor (#932)", + ); + }; + let r = synth_core::proven_safe::ingest(path, module_bytes, min_bytes); for d in &r.diagnostics { eprintln!("warning: proven-safe: {d}"); } @@ -4271,7 +4317,11 @@ fn compile_all_exports( scry_version: ing.scry_version.clone(), module_sha256: ing.actual_module_sha256.clone(), declared_module_sha256: ing.declared_module_sha256.clone(), - memory_min_bytes: proven_safe_module_min_bytes, + // #932: an attestation is only reached on an ACCEPTED ingest, and + // acceptance now requires an ESTABLISHED floor — so this cannot be + // the old invented 0. The `unwrap_or(0)` here is unreachable by + // construction; it is not a fallback. + memory_min_bytes: proven_safe_module_min_bytes.unwrap_or(0), declared_memory_min_bytes: ing.declared_memory_min_bytes, safety_bounds: safety_bounds.as_str().to_string(), accepted: ing.accepted, diff --git a/crates/synth-cli/tests/proven_safe_imported_memory_932.rs b/crates/synth-cli/tests/proven_safe_imported_memory_932.rs new file mode 100644 index 00000000..6779c673 --- /dev/null +++ b/crates/synth-cli/tests/proven_safe_imported_memory_932.rs @@ -0,0 +1,222 @@ +//! #932 (CRITICAL/SECURITY) — `--proven-safe` must never elide against a floor +//! it invented. +//! +//! For a module whose memory is IMPORTED, the derived floor was +//! `all_memories.first().map(..).unwrap_or(0)` = **0**, because imported +//! memories are not in `all_memories`. The consequences, measured on v0.55.0: +//! +//! | claimed `memory_min_bytes` | verdict | `udf` guards | +//! |---|---|---| +//! | baseline, no `--proven-safe` | — | 2 | +//! | `0` (vacuous) | ACCEPTED | **0** — guards STRIPPED | +//! | `65536` (the truth) | REFUSED | 2 | +//! +//! The fail-closed contract inverted: the honest document was rejected and the +//! vacuous one stripped real guards, while synth printed "proved 1 access site +//! in-bounds against the 0 B floor" — self-refuting, since no access is in +//! bounds of a zero-byte memory. An imported memory is real at run time, so +//! that is an unguarded access at an attacker-controlled offset. +//! +//! # Why this test exists in this shape +//! +//! The #901 differential that gated the original feature used a module with a +//! **declared** memory, so the imported shape was never exercised and the +//! validator only ever saw the case it was written against. That is the blind +//! spot recorded after v0.53 — *two validators can share one blind spot; only +//! exercising the other shape catches it*. So this test pins the SHAPE, not +//! just the symptom. + +use std::path::{Path, PathBuf}; +use std::process::Command; + +fn synth() -> PathBuf { + PathBuf::from(env!("CARGO_BIN_EXE_synth")) +} + +fn workdir(tag: &str) -> PathBuf { + let d = std::env::temp_dir().join(format!("synth-932-{tag}")); + std::fs::create_dir_all(&d).expect("temp dir"); + d +} + +/// Count the inline bounds-guard traps (`udf`) in the emitted object. +/// +/// Read from synth's own disassembler so the test does not depend on +/// llvm-objdump being installed on the runner (the #850 host-dependency +/// lesson: a differential that needs a host tool is a differential that +/// silently stops running). +fn guard_count(obj: &Path) -> usize { + let out = Command::new(synth()) + .args(["disasm", obj.to_str().unwrap()]) + .output() + .expect("run synth disasm"); + String::from_utf8_lossy(&out.stdout) + .lines() + .filter(|l| l.to_ascii_lowercase().contains("udf")) + .count() +} + +fn compile(dir: &Path, wasm: &Path, out: &str, verdicts: Option<&Path>) -> (PathBuf, String) { + let obj = dir.join(out); + let mut c = Command::new(synth()); + c.args([ + "compile", + wasm.to_str().unwrap(), + "-b", + "arm", + "--target", + "cortex-m4", + "--safety-bounds", + "software", + "--all-exports", + "--relocatable", + "-o", + obj.to_str().unwrap(), + ]); + if let Some(v) = verdicts { + c.args(["--proven-safe", v.to_str().unwrap()]); + } + let o = c.output().expect("run synth compile"); + assert!( + o.status.success(), + "compile failed: {}", + String::from_utf8_lossy(&o.stderr) + ); + (obj, String::from_utf8_lossy(&o.stderr).to_string()) +} + +/// The sha256 synth computes over the bytes it hands to the DECODER. +/// +/// Scraped from synth's own mismatch diagnostic rather than recomputed here: +/// the hash covers post-`.wat`-parse, post-loom, post-arena-bind bytes, so +/// hashing the source file would be a DIFFERENT number and the test would once +/// again pass for the wrong reason. +/// +/// This matters more than it looks. The first version of this test used a dummy +/// hash, so every compile was refused at the HASH gate and the guards survived +/// for a reason unrelated to #932 — mutating the fix away did NOT make the test +/// fail. Getting the hash right is what makes the floor check the only thing +/// left that can refuse. +fn actual_module_sha256(dir: &Path, wat: &Path) -> String { + let probe = dir.join("probe_hash.json"); + std::fs::write( + &probe, + format!( + r#"{{"schema":"scry/safe-accesses/v1","module_sha256":"{}", + "memory_min_bytes":65536,"proven_safe":[]}}"#, + "0".repeat(64) + ), + ) + .expect("write probe"); + let (_o, stderr) = compile(dir, wat, "probe.o", Some(&probe)); + let re_hash = stderr + .split("hashes to ") + .nth(1) + .and_then(|s| s.split(['.', ' ', '\n']).next()) + .map(|s| s.trim().to_string()); + re_hash.unwrap_or_else(|| panic!("could not scrape the module hash from:\n{stderr}")) +} + +const IMPORTED: &str = r#"(module + (import "env" "memory" (memory 1)) + (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a)))) +"#; + +/// THE SECURITY PROPERTY. A module with no floor synth can establish must not +/// have a single guard elided — whatever the document claims. +#[test] +fn imported_memory_never_elides_against_an_invented_floor() { + let dir = workdir("imported"); + let wat = dir.join("imp.wat"); + std::fs::write(&wat, IMPORTED).expect("write wat"); + + let (_base, _) = compile(&dir, &wat, "base.o", None); + let baseline = guard_count(&_base); + let sha = actual_module_sha256(&dir, &wat); + // Non-vacuity: if the baseline emits no guards the comparison below proves + // nothing, and this test would pass over an empty set forever. + assert!( + baseline > 0, + "fixture must emit bounds guards without --proven-safe, got {baseline}" + ); + + // Both the VACUOUS claim (0) and the TRUTHFUL one (65536) must leave every + // guard standing: synth cannot establish the floor for an imported memory, + // and absence of evidence is not evidence of safety. + for claimed in [0u64, 65536] { + let v = dir.join(format!("verdicts_{claimed}.json")); + // The hash is CORRECT on purpose: with a wrong one the hash gate + // refuses first and this test proves nothing about the floor (verified + // by mutation — see `actual_module_sha256`). + std::fs::write( + &v, + format!( + r#"{{"schema":"scry/safe-accesses/v1", + "module_sha256":"{sha}", + "memory_min_bytes":{claimed}, + "proven_safe":[{{"func":0,"pc":1,"op":"i32.load","width":4}}]}}"# + ), + ) + .expect("write verdicts"); + + let (obj, stderr) = compile(&dir, &wat, &format!("out_{claimed}.o"), Some(&v)); + assert_eq!( + guard_count(&obj), + baseline, + "claimed floor {claimed}: guards were elided for a module whose floor \ + synth cannot establish — this is #932, an unguarded access at an \ + attacker-controlled offset. stderr:\n{stderr}" + ); + assert!( + !stderr.contains("0 B floor"), + "synth must never report proving anything 'against the 0 B floor' — \ + no access is in bounds of a zero-byte memory. stderr:\n{stderr}" + ); + } +} + +/// The feature must still WORK where a floor genuinely exists — otherwise the +/// fix above is indistinguishable from deleting the feature. +#[test] +fn declared_memory_still_elides_on_a_truthful_document() { + let dir = workdir("declared"); + let wat = dir.join("decl.wat"); + std::fs::write( + &wat, + r#"(module + (memory 1) + (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a)))) +"#, + ) + .expect("write wat"); + + let (base, _) = compile(&dir, &wat, "base.o", None); + let baseline = guard_count(&base); + assert!(baseline > 0, "fixture must emit guards, got {baseline}"); + + let sha = actual_module_sha256(&dir, &wat); + let v = dir.join("v.json"); + std::fs::write( + &v, + format!( + r#"{{"schema":"scry/safe-accesses/v1","module_sha256":"{sha}", + "memory_min_bytes":65536, + "proven_safe":[{{"func":0,"pc":1,"op":"i32.load","width":4}}]}}"# + ), + ) + .expect("write verdicts"); + let (obj, stderr) = compile(&dir, &wat, "out.o", Some(&v)); + + assert!( + !stderr.contains("no linear memory"), + "a DECLARED memory establishes a floor — the #932 refusal must not fire \ + here. stderr:\n{stderr}" + ); + assert!( + guard_count(&obj) < baseline, + "the feature must still ELIDE where a floor genuinely exists, else the \ + #932 fix is indistinguishable from deleting it: baseline {baseline}, \ + got {}. stderr:\n{stderr}", + guard_count(&obj) + ); +} diff --git a/crates/synth-core/src/proven_safe.rs b/crates/synth-core/src/proven_safe.rs index 11bdc067..31d6678f 100644 --- a/crates/synth-core/src/proven_safe.rs +++ b/crates/synth-core/src/proven_safe.rs @@ -140,6 +140,15 @@ pub struct ProvenSafeIngest { } impl ProvenSafeIngest { + /// A refusal the CALLER establishes, for a gate that cannot be checked + /// inside this module. #932: the memory floor is derived by the CLI from + /// the decoded module, so "no floor could be established" is refusable only + /// out there — and it must refuse, not fall back to a `0` floor, because + /// every verdict validated against a zero-byte floor is vacuous. + pub fn refused(reason: impl Into) -> Self { + Self::refuse(reason) + } + /// A refusal: nothing trusted, one named reason. fn refuse(reason: impl Into) -> Self { let reason = reason.into(); From 2679b53e73b7dc51bd14ae25d52a3bbb98baa484 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 8 Aug 2026 13:17:34 +0200 Subject: [PATCH 2/2] test(#932): measure synth's own code size, not disassembly text MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The CI Test job failed with 'fixture must emit guards, got 0' — on macOS the test passed, on the ubuntu runner it counted ZERO. The test parsed `synth disasm` output for `udf` mnemonics. That is a lesson already recorded in this repo and violated anyway: DISASSEMBLY TEXT IS HOST-DEPENDENT — read structure, not rendering. Worse, I switched TO disasm specifically to avoid an llvm-objdump host dependency, trading one host dependency for the known-worse one. Now uses synth's OWN reported `Total code size: N bytes`: its own number, identical on every host, and it moves for exactly the reason under test — eliding a bounds guard REMOVES instructions (24 B guarded -> 8 B elided). Red-first RE-verified after the rewrite, and note the near-miss: the first mutation attempt silently did not apply, because `cargo fmt` had reformatted the anchor line — so the 'MUTATED' run was actually unmutated and proved nothing. Asserting the replacement applied is what caught it. With the mutation genuinely applied: 'code SHRANK 24 -> 8 bytes' and the test fails. clippy 0, fmt 0, 2/2. --- .../tests/proven_safe_imported_memory_932.rs | 189 +++++++++--------- 1 file changed, 89 insertions(+), 100 deletions(-) diff --git a/crates/synth-cli/tests/proven_safe_imported_memory_932.rs b/crates/synth-cli/tests/proven_safe_imported_memory_932.rs index 6779c673..500324f4 100644 --- a/crates/synth-cli/tests/proven_safe_imported_memory_932.rs +++ b/crates/synth-cli/tests/proven_safe_imported_memory_932.rs @@ -3,16 +3,16 @@ //! //! For a module whose memory is IMPORTED, the derived floor was //! `all_memories.first().map(..).unwrap_or(0)` = **0**, because imported -//! memories are not in `all_memories`. The consequences, measured on v0.55.0: +//! memories live in `imports`, not `memories`. Measured on v0.55.0: //! -//! | claimed `memory_min_bytes` | verdict | `udf` guards | +//! | claimed `memory_min_bytes` | verdict | bounds guards | //! |---|---|---| -//! | baseline, no `--proven-safe` | — | 2 | -//! | `0` (vacuous) | ACCEPTED | **0** — guards STRIPPED | -//! | `65536` (the truth) | REFUSED | 2 | +//! | baseline, no `--proven-safe` | — | present | +//! | `0` (vacuous) | ACCEPTED | **STRIPPED** | +//! | `65536` (the truth) | REFUSED | present | //! -//! The fail-closed contract inverted: the honest document was rejected and the -//! vacuous one stripped real guards, while synth printed "proved 1 access site +//! The fail-closed contract inverted: the honest document rejected, the vacuous +//! one stripping real guards, while synth printed "proved 1 access site //! in-bounds against the 0 B floor" — self-refuting, since no access is in //! bounds of a zero-byte memory. An imported memory is real at run time, so //! that is an unguarded access at an attacker-controlled offset. @@ -21,10 +21,9 @@ //! //! The #901 differential that gated the original feature used a module with a //! **declared** memory, so the imported shape was never exercised and the -//! validator only ever saw the case it was written against. That is the blind -//! spot recorded after v0.53 — *two validators can share one blind spot; only -//! exercising the other shape catches it*. So this test pins the SHAPE, not -//! just the symptom. +//! validator only ever saw the case it was written against — the v0.53 lesson +//! that a validator tests the shape it was written against. This pins the +//! SHAPE, not just the symptom. use std::path::{Path, PathBuf}; use std::process::Command; @@ -39,24 +38,29 @@ fn workdir(tag: &str) -> PathBuf { d } -/// Count the inline bounds-guard traps (`udf`) in the emitted object. +/// Bytes of machine code, from synth's OWN stdout (`Total code size: N bytes`). /// -/// Read from synth's own disassembler so the test does not depend on -/// llvm-objdump being installed on the runner (the #850 host-dependency -/// lesson: a differential that needs a host tool is a differential that -/// silently stops running). -fn guard_count(obj: &Path) -> usize { - let out = Command::new(synth()) - .args(["disasm", obj.to_str().unwrap()]) - .output() - .expect("run synth disasm"); - String::from_utf8_lossy(&out.stdout) - .lines() - .filter(|l| l.to_ascii_lowercase().contains("udf")) - .count() +/// NOT from disassembly. The first version counted `udf` mnemonics in +/// `synth disasm` output; it passed on macOS and returned ZERO on the ubuntu +/// runner, failing both tests with "fixture must emit guards, got 0". That is a +/// lesson already recorded in this repo and violated anyway: **disassembly TEXT +/// is host-dependent — read structure, not rendering.** It also traded an +/// `llvm-objdump` host dependency for a worse one. +/// +/// Code size is synth's own number, identical on every host, and it moves for +/// exactly the reason under test: eliding a bounds guard REMOVES instructions +/// (measured on the declared-memory fixture: 24 B guarded, 8 B elided). +fn code_size(stdout: &str) -> usize { + stdout + .split("Total code size:") + .nth(1) + .and_then(|s| s.split_whitespace().next()) + .and_then(|n| n.parse().ok()) + .unwrap_or_else(|| panic!("no 'Total code size:' in synth stdout:\n{stdout}")) } -fn compile(dir: &Path, wasm: &Path, out: &str, verdicts: Option<&Path>) -> (PathBuf, String) { +/// Compile and return `(code_size_bytes, stderr)`. +fn compile(dir: &Path, wasm: &Path, out: &str, verdicts: Option<&Path>) -> (usize, String) { let obj = dir.join(out); let mut c = Command::new(synth()); c.args([ @@ -82,21 +86,20 @@ fn compile(dir: &Path, wasm: &Path, out: &str, verdicts: Option<&Path>) -> (Path "compile failed: {}", String::from_utf8_lossy(&o.stderr) ); - (obj, String::from_utf8_lossy(&o.stderr).to_string()) + ( + code_size(&String::from_utf8_lossy(&o.stdout)), + String::from_utf8_lossy(&o.stderr).to_string(), + ) } -/// The sha256 synth computes over the bytes it hands to the DECODER. -/// -/// Scraped from synth's own mismatch diagnostic rather than recomputed here: -/// the hash covers post-`.wat`-parse, post-loom, post-arena-bind bytes, so -/// hashing the source file would be a DIFFERENT number and the test would once -/// again pass for the wrong reason. +/// The sha256 synth computes over the bytes it hands to the DECODER, scraped +/// from synth's own diagnostic. /// /// This matters more than it looks. The first version of this test used a dummy /// hash, so every compile was refused at the HASH gate and the guards survived -/// for a reason unrelated to #932 — mutating the fix away did NOT make the test -/// fail. Getting the hash right is what makes the floor check the only thing -/// left that can refuse. +/// for a reason unrelated to #932 — mutating the fix away did NOT fail the +/// test. Making the hash CORRECT is what leaves the floor check as the only +/// thing that can refuse. fn actual_module_sha256(dir: &Path, wat: &Path) -> String { let probe = dir.join("probe_hash.json"); std::fs::write( @@ -108,13 +111,27 @@ fn actual_module_sha256(dir: &Path, wat: &Path) -> String { ), ) .expect("write probe"); - let (_o, stderr) = compile(dir, wat, "probe.o", Some(&probe)); - let re_hash = stderr + let (_sz, stderr) = compile(dir, wat, "probe.o", Some(&probe)); + stderr .split("hashes to ") .nth(1) .and_then(|s| s.split(['.', ' ', '\n']).next()) - .map(|s| s.trim().to_string()); - re_hash.unwrap_or_else(|| panic!("could not scrape the module hash from:\n{stderr}")) + .map(|s| s.trim().to_string()) + .unwrap_or_else(|| panic!("could not scrape the module hash from:\n{stderr}")) +} + +fn verdict_doc(dir: &Path, name: &str, sha: &str, claimed: u64) -> PathBuf { + let v = dir.join(name); + std::fs::write( + &v, + format!( + r#"{{"schema":"scry/safe-accesses/v1","module_sha256":"{sha}", + "memory_min_bytes":{claimed}, + "proven_safe":[{{"func":0,"pc":1,"op":"i32.load","width":4}}]}}"# + ), + ) + .expect("write verdicts"); + v } const IMPORTED: &str = r#"(module @@ -122,50 +139,40 @@ const IMPORTED: &str = r#"(module (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a)))) "#; -/// THE SECURITY PROPERTY. A module with no floor synth can establish must not -/// have a single guard elided — whatever the document claims. +const DECLARED: &str = r#"(module + (memory 1) + (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a)))) +"#; + +/// THE SECURITY PROPERTY. A module whose floor synth cannot establish must keep +/// every guard — whatever the document claims. #[test] fn imported_memory_never_elides_against_an_invented_floor() { let dir = workdir("imported"); let wat = dir.join("imp.wat"); std::fs::write(&wat, IMPORTED).expect("write wat"); - let (_base, _) = compile(&dir, &wat, "base.o", None); - let baseline = guard_count(&_base); - let sha = actual_module_sha256(&dir, &wat); - // Non-vacuity: if the baseline emits no guards the comparison below proves - // nothing, and this test would pass over an empty set forever. + let (baseline, _) = compile(&dir, &wat, "base.o", None); + // Non-vacuity: with no code there is nothing to elide and the comparisons + // below would pass over an empty set forever. assert!( baseline > 0, - "fixture must emit bounds guards without --proven-safe, got {baseline}" + "fixture must emit code without --proven-safe, got {baseline} bytes" ); + let sha = actual_module_sha256(&dir, &wat); - // Both the VACUOUS claim (0) and the TRUTHFUL one (65536) must leave every - // guard standing: synth cannot establish the floor for an imported memory, - // and absence of evidence is not evidence of safety. + // The VACUOUS claim (0) and the TRUTHFUL one (65536) must BOTH leave the + // code untouched: synth cannot establish this module's floor, and absence + // of evidence is not evidence of safety. for claimed in [0u64, 65536] { - let v = dir.join(format!("verdicts_{claimed}.json")); - // The hash is CORRECT on purpose: with a wrong one the hash gate - // refuses first and this test proves nothing about the floor (verified - // by mutation — see `actual_module_sha256`). - std::fs::write( - &v, - format!( - r#"{{"schema":"scry/safe-accesses/v1", - "module_sha256":"{sha}", - "memory_min_bytes":{claimed}, - "proven_safe":[{{"func":0,"pc":1,"op":"i32.load","width":4}}]}}"# - ), - ) - .expect("write verdicts"); - - let (obj, stderr) = compile(&dir, &wat, &format!("out_{claimed}.o"), Some(&v)); + let v = verdict_doc(&dir, &format!("verdicts_{claimed}.json"), &sha, claimed); + let (size, stderr) = compile(&dir, &wat, &format!("out_{claimed}.o"), Some(&v)); assert_eq!( - guard_count(&obj), - baseline, - "claimed floor {claimed}: guards were elided for a module whose floor \ - synth cannot establish — this is #932, an unguarded access at an \ - attacker-controlled offset. stderr:\n{stderr}" + size, baseline, + "claimed floor {claimed}: code SHRANK {baseline} -> {size} bytes, i.e. \ + guards were elided for a module whose floor synth cannot establish. \ + That is #932 — an unguarded access at an attacker-controlled \ + offset. stderr:\n{stderr}" ); assert!( !stderr.contains("0 B floor"), @@ -175,37 +182,20 @@ fn imported_memory_never_elides_against_an_invented_floor() { } } -/// The feature must still WORK where a floor genuinely exists — otherwise the -/// fix above is indistinguishable from deleting the feature. +/// The feature must still WORK where a floor genuinely exists, or the fix above +/// is indistinguishable from deleting it. #[test] fn declared_memory_still_elides_on_a_truthful_document() { let dir = workdir("declared"); let wat = dir.join("decl.wat"); - std::fs::write( - &wat, - r#"(module - (memory 1) - (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a)))) -"#, - ) - .expect("write wat"); - - let (base, _) = compile(&dir, &wat, "base.o", None); - let baseline = guard_count(&base); - assert!(baseline > 0, "fixture must emit guards, got {baseline}"); + std::fs::write(&wat, DECLARED).expect("write wat"); + let (baseline, _) = compile(&dir, &wat, "base.o", None); + assert!(baseline > 0, "fixture must emit code, got {baseline} bytes"); let sha = actual_module_sha256(&dir, &wat); - let v = dir.join("v.json"); - std::fs::write( - &v, - format!( - r#"{{"schema":"scry/safe-accesses/v1","module_sha256":"{sha}", - "memory_min_bytes":65536, - "proven_safe":[{{"func":0,"pc":1,"op":"i32.load","width":4}}]}}"# - ), - ) - .expect("write verdicts"); - let (obj, stderr) = compile(&dir, &wat, "out.o", Some(&v)); + + let v = verdict_doc(&dir, "v.json", &sha, 65536); + let (size, stderr) = compile(&dir, &wat, "out.o", Some(&v)); assert!( !stderr.contains("no linear memory"), @@ -213,10 +203,9 @@ fn declared_memory_still_elides_on_a_truthful_document() { here. stderr:\n{stderr}" ); assert!( - guard_count(&obj) < baseline, + size < baseline, "the feature must still ELIDE where a floor genuinely exists, else the \ #932 fix is indistinguishable from deleting it: baseline {baseline}, \ - got {}. stderr:\n{stderr}", - guard_count(&obj) + got {size}. stderr:\n{stderr}" ); }