docs+test: spectre/csdb policy + aarch64 CVE audit + arXiv 2604.17391 citation#105
Merged
Merged
Conversation
… citation Aligns synth with the Wasmtime 44.0.0 default (csdb off on aarch64) by making the per-lowering decision explicit, using the Crocus (ASPLOS 2024) F/D/A policy taxonomy. The threat model for synth is single-tenant ARMv7-M / RV32 with optional MPU/PMP isolation — not a multi-tenant sandbox — so Spectre-v1 BCB does not directly translate, but the decisions are documented per rule so a reviewer can re-check them after refactors. Per the audit of the April 2026 Wasmtime security advisories: - GHSA-jhxm-h53p-jm7w / CVE-2026-34971 (aarch64 Cranelift sandbox escape) has a *latent* analog in synth: the `add_with_shift` standard rule (`rules.rs:1887`) matches any `I32Shl;I32Add` but hard-codes the replacement's LSL `amount` to 2. The unsoundness is gated only by the fact that `RuleApplicator::apply_rules` currently does not actually rewrite ops to the rule's replacement. A regression test asserts the disjunction "rule removed OR amount not hard-coded OR applicator still inert" so the CVE shape cannot land silently. - GHSA-qqfj-4vcm-26hv / CVE-2026-34944 (x86-64 f64x2.splat over-read) has no analog: synth doesn't target x86-64, and the Helium MVE path uses correctly-sized VLDRW.32 / VDUP rather than a short-load + broadcast that could over-read. Adds a "Customer narrative" section to the README citing Andreasyan et al., arXiv 2604.17391 ("RISC-V Functional Safety for Autonomous Automotive Systems"), which argues that functional safety is a certification problem rather than a processor problem — exactly the framing synth's verifiable codegen targets. Files: - docs/spectre-policy.md (new) — policy intent, 21 per-rule decisions, CVE analog audit, references, review cadence. - crates/synth-synthesis/tests/regression_spectre_cve_2026_34971.rs (new) — two tests gating the latent CVE-2026-34971 shape. - README.md — new Customer narrative section. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
force-pushed
the
feat/spectre-policy-and-cve-audit
branch
from
d6babd2 to
654f768
Compare
5 tasks
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
May 21, 2026
…or I32Add (#76) (#113) * feat(verify): validator pattern prototype — CertifiedSelection + Z3 for I32Add Closes the architectural commitment for issue #76 and opens the path toward retiring issue #73's divergent-Rocq-proofs credibility gap. ## Architecture CompCert's certifying-algorithm pattern: don't verify the (NP-hard, heuristic, frequently-changing) instruction selector — verify a small, formally-checkable validator that consumes the selector's output and confirms each concrete selection is semantically equivalent to the WASM op it replaces. * New `CertifiedSelection<W, A>` type carries (wasm_op, arm_instrs, witness). Selectors emit witness-less selections; validators accept-or-reject and attach a Witness. * New `Validator<W, A>` trait + `Z3ArmValidator` implementation (prototype handles `WasmOp::I32Add` mapped to `ArmOp::Add` as the worked example). * Counterexample-driven rejection: a buggy selector that emits SUB instead of ADD gets caught with concrete input values (R0=5, R1=3 → arm=2, wasm=8). ## Migration path (from docs/validator-pattern.md) * Keep existing T1 Rocq proofs (35 ops) — they're correct already. * Validator covers everything else. T2 existence proofs (143) become redundant once their ops are validator-certified. * T3 admits (10) get re-examined — most should close via the validator since they were re-admitted for ARM-vs-Rocq divergence. ## Tests (in crates/synth-verify/src/validator_pattern.rs) * `i32_add_certifies` — selector picks ADD, validator accepts * (wrong-selection test, in the same module) — selector picks SUB, validator rejects with Counterexample * `unsupported_op_returns_structured_error` — non-I32Add ops return `UnsupportedOp`, not a panic * `certified_selection_witness_roundtrip` — plumbing ## What this PR is NOT This is the architectural commitment + one worked example. It does NOT validate all 150 wasm ops — that's the v0.5/v0.6 work this scaffolding enables. Per-op validator extension is structurally trivial now; the hard part was deciding the pattern. References: docs/validator-pattern.md (314 lines), issue #76, issue #73, issue #105's spectre-policy doc (cites the same Crocus paper). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * style(verify): fmt fix for validator_pattern.rs Run cargo fmt -p synth-verify to bring encode_arm_sequence's signature to single-line form. No semantic change. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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.
Summary
docs/spectre-policy.md— a per-lowering Spectre / speculative-execution policy for synth's WASM-to-ARM-Cortex-M / RV32 codegen, aligned with the Wasmtime 44.0.0 default (csdb off on aarch64) and using the Crocus (ASPLOS 2024) F/D/A policy taxonomy. 21 rule decisions documented.rules.rs:1887(theadd_with_shiftstandard rule hard-codes the LSLamountto 2 while pattern-matching anyI32Shl;I32Add). Gated today only by the fact thatRuleApplicator::apply_rulesdoes not actually rewrite ops to the replacement. A new regression testcrates/synth-synthesis/tests/regression_spectre_cve_2026_34971.rsasserts the safety disjunction so the CVE shape can't land silently.Key decisions in spectre-policy.md
add_with_shiftstandard rule) are flagged for explicit attention.--mitigate-spectre-v1): 1 rule for M7/M55. D (other mitigation suffices): 19 rules. A (accepted residual): 2 rules, both gated (one by a regression test, one by docs).AND-masking (BoundsCheckConfig::Masking) is recommended for Cortex-M55 per the Blade (POPL 2021) index-masking result.add_with_shiftrule; the regression test makes the latency of the bug explicit and self-checking.Files changed
docs/spectre-policy.md(new, ~210 lines)crates/synth-synthesis/tests/regression_spectre_cve_2026_34971.rs(new, 2 tests, both passing)README.md(new "Customer narrative" section between PulseEngine table and Installation)Test plan
cargo test -p synth-synthesis --test regression_spectre_cve_2026_34971— 2 passedcargo test --workspace --exclude synth-verify— all pass (synth-verify excluded due to unrelated bundled-z3 build issue on the dev machine; CI uses the system z3)cargo clippy --workspace --all-targets -- -D warnings— cleancargo fmt --check— cleansynth-verifybuilds via system z3Scope notes
This PR does not touch:
optimizer_bridge.rs(PR fix(opt): defensive panic on unmapped vreg instead of silent R0 fallback #101 territory)feat/riscv-cross-function-callsWIPThe regression test only reads the public
RuleDatabase/RuleApplicatorAPI; it has no overlap with in-flight work.References:
Generated with Claude Code