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..500324f4 --- /dev/null +++ b/crates/synth-cli/tests/proven_safe_imported_memory_932.rs @@ -0,0 +1,211 @@ +//! #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 live in `imports`, not `memories`. Measured on v0.55.0: +//! +//! | claimed `memory_min_bytes` | verdict | bounds guards | +//! |---|---|---| +//! | baseline, no `--proven-safe` | — | present | +//! | `0` (vacuous) | ACCEPTED | **STRIPPED** | +//! | `65536` (the truth) | REFUSED | present | +//! +//! 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. +//! +//! # 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 — 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; + +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 +} + +/// Bytes of machine code, from synth's OWN stdout (`Total code size: N bytes`). +/// +/// 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}")) +} + +/// 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([ + "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) + ); + ( + 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 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 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( + &probe, + format!( + r#"{{"schema":"scry/safe-accesses/v1","module_sha256":"{}", + "memory_min_bytes":65536,"proven_safe":[]}}"#, + "0".repeat(64) + ), + ) + .expect("write probe"); + 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()) + .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 + (import "env" "memory" (memory 1)) + (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a)))) +"#; + +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 (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 code without --proven-safe, got {baseline} bytes" + ); + let sha = actual_module_sha256(&dir, &wat); + + // 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 = verdict_doc(&dir, &format!("verdicts_{claimed}.json"), &sha, claimed); + let (size, stderr) = compile(&dir, &wat, &format!("out_{claimed}.o"), Some(&v)); + assert_eq!( + 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"), + "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, 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, 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 = verdict_doc(&dir, "v.json", &sha, 65536); + let (size, 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!( + size < baseline, + "the feature must still ELIDE where a floor genuinely exists, else the \ + #932 fix is indistinguishable from deleting it: baseline {baseline}, \ + got {size}. stderr:\n{stderr}" + ); +} 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();