fix(#932): --proven-safe must never elide against a floor it invented (SECURITY) - #934
Merged
Merged
Conversation
… (SECURITY)
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<u32> 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
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.
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #932. v0.56 lane RQ-56-PSAFE.
The defect
Imported memories are not in
all_memories, so the derived floor was.unwrap_or(0)— 'no floor establishable' became 'the floor is 0 bytes'.memory_min_bytes0(vacuous)65536(the truth)The floor is now
Option<u32>;Nonerefuses.My first test was vacuous, and mutation caught it
It used a dummy hash, so every compile was refused at the hash gate — the guards survived for a reason unrelated to #932, and 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 left that can refuse.
That needed a product change too: the floor refusal reports the computed hash, which a consumer debugging a rejected document needs regardless.
Now potent — reverting the fix reproduces
ACCEPTED … against the 0 B floorand the test fails.Named residual
The truthful document for an imported memory is still refused, because the decoder discards the import's declared minimum (
TypeRef::Memory(_)). Safe but not yet useful; tracked on #932 rather than left as a surprise.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.