From b2978e684b27aa989c17aa6032816385bed7b912 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 22 Jun 2026 17:31:50 +0200 Subject: [PATCH] feat(vcr-mem): layer-2 shadow-stack budget decision logic, frozen-safe (#242, #383) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit VCR-MEM-001 layer-2 derives the shadow-stack budget B from a PROVEN worst-case stack depth instead of an integrator-asserted number (layer-1, #383). This lands the DECISION LOGIC only — deliberately dep-free and decoupled from the scry production-dep decision (a 28-crate Bazel cascade that is a separate, user-gated step). `synth-cli/src/shadow_budget.rs`: pure `budget_from_bound(bound, sp_init, fallback) -> BudgetDecision` over a synth-OWNED `StackDepthBound` enum (Bytes(u64)|Unbounded|Unknown), so the logic + its 9 unit tests compile WITHOUT scry in the build graph. The adapter from `scry_analyze_core::StackBound` lives at the (gated) call site. Scope is primary-source-confirmed (scry-sai-core-1.12 lib.rs:276-281: max_stack_bytes = "the deepest weighted path … each function weighted by the frame its prologue subtracts from the __stack_pointer global … guest shadow-stack only") ⇒ Bytes(n) yields source=ProvenStackDepth labelled "proven stack DEPTH, asserted no-heap" — NOT a bare "proven footprint" (the #383 overclaim shape is explicitly guarded). Refuses when proven depth > sp_init, naming it as the ORIGINAL image under-provisioning its stack. Unbounded/Unknown ⇒ AssertedFallback or honest-refuse; Unknown NEVER yields ProvenStackDepth even with a fallback. B rounded up to 16-byte AAPCS/LLVM stack alignment (rounding up preserves B >= proven depth). Frozen-safe: no call site yet (`#[allow(dead_code)]`), no byte-changing codegen, default behaviour unchanged. The scry dep-architecture choice and the analyze()→budget wiring are the remaining gated steps, recorded in the roadmap (2a user decision / 2b adapter+wiring). Co-Authored-By: Claude Opus 4.8 --- artifacts/verified-codegen-roadmap.yaml | 43 ++++ crates/synth-cli/src/main.rs | 5 + crates/synth-cli/src/shadow_budget.rs | 266 ++++++++++++++++++++++++ 3 files changed, 314 insertions(+) create mode 100644 crates/synth-cli/src/shadow_budget.rs diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 7f605147..18daeaad 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1109,6 +1109,40 @@ artifacts: #359 check), behind the opt-in flag so frozen fixtures stay bit-identical. gale offered on-silicon reflash on this exact gust_kernel.wasm as the final gate. A FOCUSED gated step, not an idle-tick increment. + + LAYER-2 DECISION LOGIC LANDED (2026-06-22, frozen-safe, no dep change): + `synth-cli/src/shadow_budget.rs` — a pure `budget_from_bound(bound, + sp_init, fallback) -> BudgetDecision` over a synth-OWNED `StackDepthBound` + enum (Bytes(u64)|Unbounded|Unknown), so the decision compiles and unit- + tests (9 cases) WITHOUT scry in the build graph. Primary-source-confirmed + scope (scry-sai-core-1.12 lib.rs:276-281: max_stack_bytes is "the deepest + weighted path … each function weighted by the frame its prologue subtracts + from the __stack_pointer global … guest shadow-stack only") ⇒ Bytes(n) + yields source=ProvenStackDepth labelled "proven stack DEPTH, asserted + no-heap" (NOT a bare "proven footprint" — the #383 overclaim shape is + explicitly guarded against). Refuses when proven depth > sp_init (names it + as the ORIGINAL image under-provisioning its stack, a latent source bug + surfaced for free). Unbounded/Unknown ⇒ AssertedFallback or honest-refuse; + Unknown NEVER yields ProvenStackDepth even with a fallback (unit-tested). + B is rounded up to 16-byte AAPCS/LLVM stack alignment (rounding up keeps + B >= proven depth ⇒ soundness preserved). `#[allow(dead_code)]` until the + gated call site lands. + + TWO GATED STEPS REMAIN, the first a USER DECISION: + (2a) DEP ARCHITECTURE — promoting scry-sai-core from dev-dep to a + PRODUCTION dep of synth-cli pulls its full transitive closure into + the Bazel `rust_binary` compile (synth-cli IS in the Bazel graph: + crates/BUILD.bazel:230). MODULE.bazel uses `crate.from_specs()` + (21 manual `crate.spec`s, NOT `from_cargo`) — likely because z3 + needs `features=["static-link-z3"]`. So the cascade is real and the + fix is one of {from_cargo migration, feature-gate the scry call out + of the Bazel build, ~28 manual specs}. NOT an idle-tick or a unilateral + call — taken to the user. + (2b) ADAPTER + WIRING — `scry_analyze_core::StackBound -> StackDepthBound` + adapter at a gated call site that runs `analyze()` on the pre-link + Core module, feeds `budget_from_bound`, and routes the result into + the layer-1 shrink. Opt-in (e.g. `--shadow-stack-size auto`); default + unchanged ⇒ frozen fixtures bit-identical. verifies-link scry SCRY-001. status: proposed tags: [codegen, native-pointer-abi, memory-layout, abstract-interpretation, scry, stack-depth, gale-383, track-a] links: @@ -1140,6 +1174,15 @@ artifacts: LAYER (2), next: acyclic + direct-only + canonical-frame modules derive B automatically (output "proven"); call_indirect / recursion / non-canonical frame ⇒ refuse → fall back to (1). LAYER (3): scry#51 proves the tail. + LAYER (2) DECISION-LOGIC criterion (LANDED 2026-06-22, frozen-safe): + `budget_from_bound` unit suite (synth-cli src/shadow_budget.rs) asserts — + Bytes(n) ⇒ source=ProvenStackDepth with B=align16(n); Bytes(n>sp_init) ⇒ + Refuse naming the original-image under-provision; Unbounded/Unknown+fallback + ⇒ source=AssertedFallback (NEVER ProvenStackDepth, even for Unknown); + Unbounded/Unknown+no-fallback ⇒ honest Refuse with the cause. Compiles + + passes with scry ABSENT from the build graph (dep-free synth-owned bound + enum). The scry production-dep wiring (2a/2b above) is the separate gated + step; default-off ⇒ frozen fixtures unaffected. - id: VCR-MEM-002 type: sw-req diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index a7097cfb..f02153e7 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -25,6 +25,11 @@ use tracing::{Level, info}; use wast::parser::{self, ParseBuffer}; use wast::{Wast, WastDirective}; +// Layer-2 budget-derivation logic, landed frozen-safe ahead of the gated call +// site that runs scry's `analyze()` (the scry production-dep step is a separate, +// user-gated decision). `allow(dead_code)` until that wiring lands. +#[allow(dead_code)] +mod shadow_budget; mod sign; /// Sentinel value clap substitutes when `--sbom` is given without a path. diff --git a/crates/synth-cli/src/shadow_budget.rs b/crates/synth-cli/src/shadow_budget.rs new file mode 100644 index 00000000..65ed2b6e --- /dev/null +++ b/crates/synth-cli/src/shadow_budget.rs @@ -0,0 +1,266 @@ +//! VCR-MEM-001 layer-2: derive the shadow-stack budget `B` from a PROVEN +//! worst-case shadow-stack depth, instead of trusting an integrator-asserted +//! number (layer-1, #383). +//! +//! This module is the **decision logic only** and is deliberately dep-free: +//! it operates over a synth-owned [`StackDepthBound`], never over +//! `scry_analyze_core::StackBound`. The adapter from scry's type lives at the +//! (gated) call site that actually runs `analyze()`; keeping the decision here +//! means the budget logic — and its unit tests — compile and run without scry +//! in the build graph (and, critically, without scry's 28-crate transitive +//! closure entering the Bazel `rust_binary` compile). The mechanism that +//! *consumes* `B` is the proven layer-1 shrink (`--shadow-stack-size`, +//! main.rs:2641): re-base the `__stack_pointer` global `sp_init -> B` and +//! resize the `.bss` reservation. Layer-2 only changes *where B comes from*. +//! +//! ## Soundness scope — "proven stack DEPTH, asserted no-heap" +//! +//! When the bound is [`StackDepthBound::Bytes`], `B` is derived from scry's +//! `stack_usage.max_stack_bytes`, documented (scry-sai-core, FEAT-021 / +//! SCRY-001) as "the deepest weighted path through the call graph, each +//! function weighted by the frame its prologue subtracts from the +//! `__stack_pointer` global … guest shadow-stack only." Because it is a *sound +//! over-approximation*, `B >= real max shadow-stack depth`, so the reservation +//! cannot underflow the live stack. That is the ONLY thing layer-2 proves. +//! +//! What stays **asserted** (the inherited layer-1 contract, NOT proven here): +//! the static tail above `sp_init` and any heap use. scry's bound says nothing +//! about heap allocation or static data — so this remains safe only for the +//! no-grow / no-heap MCU images layer-1 already requires. We must label the +//! footprint as proven-depth + asserted-no-heap and never restate it as a bare +//! "proven footprint" (the #383 overclaim shape). + +/// Synth-owned mirror of a worst-case shadow-stack depth result. +/// +/// Mirrors `scry_analyze_core::StackBound`'s three-way shape but is dep-free so +/// the decision logic below compiles without scry. Per scry's contract, +/// `Unbounded` and `Unknown` both mean "no finite bound proven" and are NEVER +/// treated as zero. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum StackDepthBound { + /// A proven finite worst-case shadow-stack depth, in bytes. `u64` to match + /// scry's `StackBound::Bytes(u64)` without a lossy narrowing at the adapter. + Bytes(u64), + /// Recursion / a cycle in the call graph — no finite bound exists. + Unbounded, + /// The analyzer could not determine a bound (dynamic `alloca`, an + /// unresolved `call_indirect` / host edge, or an ambiguous stack-pointer + /// global). + Unknown, +} + +/// How a chosen budget `B` is justified — drives the user-facing label so a +/// proven budget is never reported with the same words as an asserted one. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum BudgetSource { + /// `B` derived from a proven shadow-stack depth (scry FEAT-021 / SCRY-001). + /// Scope: proven stack DEPTH only; the static tail above `sp_init` and any + /// heap remain the layer-1 ASSERTED no-heap / no-grow contract. + ProvenStackDepth, + /// `B` is the integrator-asserted layer-1 fallback: no finite bound was + /// proven, but the caller supplied a trusted budget to fall back to. + AssertedFallback, +} + +/// The outcome of the budget derivation: either use a concrete `B` (with its +/// justification) or refuse honestly (the #359/#368 typed-Err lesson — never +/// silently pick a number we cannot defend). +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum BudgetDecision { + /// Re-base the shadow stack to `bytes`, justified by `source`. + Use { bytes: u32, source: BudgetSource }, + /// No defensible budget; the message explains why (surfaced as a typed + /// `Err` at the call site). + Refuse(String), +} + +/// AAPCS wants 8-byte stack alignment; LLVM typically initialises +/// `__stack_pointer` 16-aligned. We round the re-based top up to 16 so frames +/// stay aligned — rounding *up* preserves `B >= proven depth`, so soundness is +/// not weakened. (All observed fixture `sp_init`s — 4096, 65536, 1048576 — are +/// 16-aligned, so a 16-aligned `B <= sp_init` whenever the depth fits.) +const STACK_ALIGN_BYTES: u64 = 16; + +/// Decide the shadow-stack budget `B` from a proven depth `bound`, given the +/// module's original shadow-stack top `sp_init` and an optional +/// integrator-asserted `fallback` (the layer-1 `--shadow-stack-size` value). +/// +/// - [`StackDepthBound::Bytes(n)`] → a PROVEN budget: `B = align16(n)`, source +/// [`BudgetSource::ProvenStackDepth`]. Refuses if `n > sp_init` — a proven +/// depth that exceeds the original reservation means the *original image +/// under-provisioned its stack*, a latent bug layer-2 surfaces for free +/// rather than hiding behind a generic refuse. +/// - [`StackDepthBound::Unbounded`] / [`StackDepthBound::Unknown`] → no finite +/// bound proven: fall back to the asserted `fallback` if given +/// ([`BudgetSource::AssertedFallback`]), else refuse honestly. +pub fn budget_from_bound( + bound: StackDepthBound, + sp_init: u32, + fallback: Option, +) -> BudgetDecision { + match bound { + StackDepthBound::Bytes(n) => { + // A proven depth above the original top is an under-provisioned + // image, not a shrink opportunity — name it precisely. + if n > u64::from(sp_init) { + return BudgetDecision::Refuse(format!( + "proven shadow-stack depth {n} B exceeds the original reservation top \ + sp_init={sp_init} B — the original image UNDER-provisioned its stack \ + (this is a latent bug in the source, not a shrink target). Refusing. \ + VCR-MEM-001 layer-2/#383." + )); + } + // Round the re-based top up to 16-byte alignment. Since `n <= sp_init` + // and `sp_init` is 16-aligned in every observed image, `align16(n) <= + // sp_init`; `min` is a belt-and-braces guard for a non-aligned top. + let aligned = n.next_multiple_of(STACK_ALIGN_BYTES); + let bytes = aligned.min(u64::from(sp_init)) as u32; + BudgetDecision::Use { + bytes, + source: BudgetSource::ProvenStackDepth, + } + } + StackDepthBound::Unbounded | StackDepthBound::Unknown => match fallback { + Some(b) => BudgetDecision::Use { + bytes: b, + source: BudgetSource::AssertedFallback, + }, + None => BudgetDecision::Refuse(format!( + "no finite shadow-stack bound was proven ({}) and no asserted \ + --shadow-stack-size fallback was given; refusing to invent a budget. \ + VCR-MEM-001 layer-2/#383.", + match bound { + StackDepthBound::Unbounded => "recursion / call-graph cycle ⇒ unbounded", + _ => + "analysis incomplete ⇒ unknown (dynamic alloca, \ + unresolved call_indirect, or ambiguous stack pointer)", + } + )), + }, + } +} + +#[cfg(test)] +mod tests { + use super::*; + + // The #392 spike measured msgq's max_stack_bytes = Bytes(32); a realistic + // sp_init for that image is the full 1 MiB page top. Proven depth 32 → + // align16 → 32, justified ProvenStackDepth. + #[test] + fn proven_depth_rounds_to_16_and_is_proven() { + let d = budget_from_bound(StackDepthBound::Bytes(32), 1_048_576, Some(4096)); + assert_eq!( + d, + BudgetDecision::Use { + bytes: 32, + source: BudgetSource::ProvenStackDepth + } + ); + } + + #[test] + fn proven_depth_unaligned_rounds_up() { + // 33 → next multiple of 16 = 48. + let d = budget_from_bound(StackDepthBound::Bytes(33), 65_536, None); + assert_eq!( + d, + BudgetDecision::Use { + bytes: 48, + source: BudgetSource::ProvenStackDepth + } + ); + } + + #[test] + fn zero_depth_is_proven_zero() { + // sp_global present but no frame ever subtracted ⇒ Bytes(0): a proven + // zero-byte stack. Stays proven; layer-1 will re-base to 0 + static tail. + let d = budget_from_bound(StackDepthBound::Bytes(0), 4096, None); + assert_eq!( + d, + BudgetDecision::Use { + bytes: 0, + source: BudgetSource::ProvenStackDepth + } + ); + } + + #[test] + fn proven_depth_above_sp_init_is_under_provision_refusal() { + // A proven depth exceeding the original top is the source image's bug, + // surfaced explicitly — NOT a generic refuse. + let d = budget_from_bound(StackDepthBound::Bytes(8192), 4096, Some(2048)); + match d { + BudgetDecision::Refuse(msg) => { + assert!(msg.contains("UNDER-provisioned"), "got: {msg}"); + assert!(msg.contains("8192")); + } + other => panic!("expected under-provision refusal, got {other:?}"), + } + } + + #[test] + fn proven_depth_exactly_at_top_is_accepted() { + // n == sp_init is not "exceeds"; align16 keeps it at the top (no shrink + // benefit, still sound and proven). + let d = budget_from_bound(StackDepthBound::Bytes(4096), 4096, None); + assert_eq!( + d, + BudgetDecision::Use { + bytes: 4096, + source: BudgetSource::ProvenStackDepth + } + ); + } + + #[test] + fn unbounded_with_fallback_is_asserted() { + let d = budget_from_bound(StackDepthBound::Unbounded, 65_536, Some(8192)); + assert_eq!( + d, + BudgetDecision::Use { + bytes: 8192, + source: BudgetSource::AssertedFallback + } + ); + } + + #[test] + fn unbounded_without_fallback_refuses() { + let d = budget_from_bound(StackDepthBound::Unbounded, 65_536, None); + match d { + BudgetDecision::Refuse(msg) => { + assert!(msg.contains("unbounded"), "got: {msg}"); + assert!(msg.contains("recursion")); + } + other => panic!("expected unbounded refusal, got {other:?}"), + } + } + + #[test] + fn unknown_with_fallback_is_asserted_not_proven() { + // The critical anti-overclaim case: Unknown must NEVER yield + // ProvenStackDepth, even with a fallback. + let d = budget_from_bound(StackDepthBound::Unknown, 65_536, Some(1024)); + assert_eq!( + d, + BudgetDecision::Use { + bytes: 1024, + source: BudgetSource::AssertedFallback + } + ); + } + + #[test] + fn unknown_without_fallback_refuses_with_cause() { + let d = budget_from_bound(StackDepthBound::Unknown, 65_536, None); + match d { + BudgetDecision::Refuse(msg) => { + assert!(msg.contains("unknown"), "got: {msg}"); + assert!(msg.contains("call_indirect") || msg.contains("alloca")); + } + other => panic!("expected unknown refusal, got {other:?}"), + } + } +}