docs: binary safety checks design — ARM + RISC-V opt-in safety profiles#110
Merged
Conversation
Adds docs/binary-safety-design.md covering eight runtime-guard categories (memory bounds, divide-by-zero, signed-division overflow, stack overflow, CFI forward and backward edges, AAPCS prologue/epilogue invariants, linear-memory poisoning, and component-model type confusion) with a hardware-fast-path / software-fallback decision tree per check and a per-target support matrix for Cortex-M3..M85 and RV32I..RV32GC. Specifies a unified --safety profile CLI surface (none / fuzz / rtos / asil-d / paranoid) plus fine-grained --safety-X overrides, cross-references docs/spectre-policy.md for transient-execution coverage, and lays out a 5-phase roadmap including Rocq proof reparameterisation in Phase 5. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
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
…ds + RV32 div trap + safety-manifest.json (#115) Implements Phase 1 of docs/binary-safety-design.md (#110). * CLI: new `--safety-bounds <mpu|software|mask|none>` flag. Keeps `--bounds-check` as a deprecated alias mapping to `--safety-bounds software`; emits a one-line deprecation notice. * CompileConfig grows a `safety_bounds: SafetyBounds` field; the ARM and RISC-V backends both read it. * Plumb through `BoundsCheckConfig` (now `SafetyBounds` at the public boundary). Existing `None` / `Software` semantics preserved on ARM. * RV32 selector: ported the software bounds-check sequence (`bgeu addr, mem_size, trap_label; ...; trap_label: ebreak`) to every i32 load/store and sub-word variant. * RV32 selector: emit `bne rs2, x0, ok; ebreak; ok: div` (and `divu`, `rem`, `remu`) trap-on-zero guards. Mirrors the existing ARM pattern (instruction_selector.rs:3895). * `safety-manifest.json` written alongside the output ELF whenever any safety flag is enabled. Schema: synth_version, target_triple, safety_bounds, safety_div_zero, safety_div_overflow, linear_memory_bytes. ## Hand-tested * `synth compile examples/wat/simple_add.wat --safety-bounds mpu -o /tmp/sa.elf --cortex-m` succeeds; `/tmp/sa.safety-manifest.json` contains the expected fields. * `synth compile examples/wat/simple_add.wat --bounds-check -o /tmp/sa.elf --cortex-m` prints the deprecation notice and still produces a working ELF. * `synth compile /tmp/rv_div.wat --backend riscv --target riscv32imac --safety-bounds software --all-exports -o /tmp/rv_div.elf` succeeds; RV32 ELF contains the div-by-zero trap sequence; manifest emitted. ## Out of scope (later phases per docs/binary-safety-design.md §6) * Phase 2: stack overflow (MSPLIM/PSPLIM/canary), CFI BTI/PAC * Phase 3: linear-memory poisoning * Phase 4: component-model type confusion * Phase 5: parameterise Compilation.v by SafetyProfile in Rocq ## Verification * `cargo test --workspace --exclude synth-verify` — all pass (z3-sys download blocked in this environment; synth-verify excluded accordingly, CI will exercise it). * `cargo clippy --workspace --exclude synth-verify --all-targets -- -D warnings` — clean. * `cargo fmt --check` — clean. 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/binary-safety-design.md(842 lines) covering eight categories of opt-in runtime safety guards for synth's ARM Cortex-M and RISC-V RV32 targets.--safety <profile>CLI surface (none/fuzz/rtos/asil-d/paranoid) plus fine-grained--safety-bounds,--safety-stack,--safety-cfi-fwd,--safety-cfi-bwd,--safety-prologue,--safety-poison,--safety-cm-types,--safety-spectre-v1overrides.coq/Synth/Compilation.vbySafetyProfileso existing T1/T2 lemmas can be re-proven per profile.Checks covered
--bounds-checkflag.safe_lift_*family insynth-abi).Test plan
cargo build/cargo testunaffected.docs/spectre-policy.md(existing) anddocs/design/MEMORY_ARCHITECTURE.md(existing) — links verified to existing files.instruction_selector.rs,mpu.rs,pmp.rs) verified against current HEAD on main.Open questions for reviewers
The document lists 8 open questions in §6, including:
s10be reserved for a stack-limit pointer when--safety-bounds=soft?🤖 Generated with Claude Code