|
| 1 | +//! VCR-MEM-001 layer-2: derive the shadow-stack budget `B` from a PROVEN |
| 2 | +//! worst-case shadow-stack depth, instead of trusting an integrator-asserted |
| 3 | +//! number (layer-1, #383). |
| 4 | +//! |
| 5 | +//! This module is the **decision logic only** and is deliberately dep-free: |
| 6 | +//! it operates over a synth-owned [`StackDepthBound`], never over |
| 7 | +//! `scry_analyze_core::StackBound`. The adapter from scry's type lives at the |
| 8 | +//! (gated) call site that actually runs `analyze()`; keeping the decision here |
| 9 | +//! means the budget logic — and its unit tests — compile and run without scry |
| 10 | +//! in the build graph (and, critically, without scry's 28-crate transitive |
| 11 | +//! closure entering the Bazel `rust_binary` compile). The mechanism that |
| 12 | +//! *consumes* `B` is the proven layer-1 shrink (`--shadow-stack-size`, |
| 13 | +//! main.rs:2641): re-base the `__stack_pointer` global `sp_init -> B` and |
| 14 | +//! resize the `.bss` reservation. Layer-2 only changes *where B comes from*. |
| 15 | +//! |
| 16 | +//! ## Soundness scope — "proven stack DEPTH, asserted no-heap" |
| 17 | +//! |
| 18 | +//! When the bound is [`StackDepthBound::Bytes`], `B` is derived from scry's |
| 19 | +//! `stack_usage.max_stack_bytes`, documented (scry-sai-core, FEAT-021 / |
| 20 | +//! SCRY-001) as "the deepest weighted path through the call graph, each |
| 21 | +//! function weighted by the frame its prologue subtracts from the |
| 22 | +//! `__stack_pointer` global … guest shadow-stack only." Because it is a *sound |
| 23 | +//! over-approximation*, `B >= real max shadow-stack depth`, so the reservation |
| 24 | +//! cannot underflow the live stack. That is the ONLY thing layer-2 proves. |
| 25 | +//! |
| 26 | +//! What stays **asserted** (the inherited layer-1 contract, NOT proven here): |
| 27 | +//! the static tail above `sp_init` and any heap use. scry's bound says nothing |
| 28 | +//! about heap allocation or static data — so this remains safe only for the |
| 29 | +//! no-grow / no-heap MCU images layer-1 already requires. We must label the |
| 30 | +//! footprint as proven-depth + asserted-no-heap and never restate it as a bare |
| 31 | +//! "proven footprint" (the #383 overclaim shape). |
| 32 | +
|
| 33 | +/// Synth-owned mirror of a worst-case shadow-stack depth result. |
| 34 | +/// |
| 35 | +/// Mirrors `scry_analyze_core::StackBound`'s three-way shape but is dep-free so |
| 36 | +/// the decision logic below compiles without scry. Per scry's contract, |
| 37 | +/// `Unbounded` and `Unknown` both mean "no finite bound proven" and are NEVER |
| 38 | +/// treated as zero. |
| 39 | +#[derive(Clone, Copy, Debug, PartialEq, Eq)] |
| 40 | +pub enum StackDepthBound { |
| 41 | + /// A proven finite worst-case shadow-stack depth, in bytes. `u64` to match |
| 42 | + /// scry's `StackBound::Bytes(u64)` without a lossy narrowing at the adapter. |
| 43 | + Bytes(u64), |
| 44 | + /// Recursion / a cycle in the call graph — no finite bound exists. |
| 45 | + Unbounded, |
| 46 | + /// The analyzer could not determine a bound (dynamic `alloca`, an |
| 47 | + /// unresolved `call_indirect` / host edge, or an ambiguous stack-pointer |
| 48 | + /// global). |
| 49 | + Unknown, |
| 50 | +} |
| 51 | + |
| 52 | +/// How a chosen budget `B` is justified — drives the user-facing label so a |
| 53 | +/// proven budget is never reported with the same words as an asserted one. |
| 54 | +#[derive(Clone, Copy, Debug, PartialEq, Eq)] |
| 55 | +pub enum BudgetSource { |
| 56 | + /// `B` derived from a proven shadow-stack depth (scry FEAT-021 / SCRY-001). |
| 57 | + /// Scope: proven stack DEPTH only; the static tail above `sp_init` and any |
| 58 | + /// heap remain the layer-1 ASSERTED no-heap / no-grow contract. |
| 59 | + ProvenStackDepth, |
| 60 | + /// `B` is the integrator-asserted layer-1 fallback: no finite bound was |
| 61 | + /// proven, but the caller supplied a trusted budget to fall back to. |
| 62 | + AssertedFallback, |
| 63 | +} |
| 64 | + |
| 65 | +/// The outcome of the budget derivation: either use a concrete `B` (with its |
| 66 | +/// justification) or refuse honestly (the #359/#368 typed-Err lesson — never |
| 67 | +/// silently pick a number we cannot defend). |
| 68 | +#[derive(Clone, Debug, PartialEq, Eq)] |
| 69 | +pub enum BudgetDecision { |
| 70 | + /// Re-base the shadow stack to `bytes`, justified by `source`. |
| 71 | + Use { bytes: u32, source: BudgetSource }, |
| 72 | + /// No defensible budget; the message explains why (surfaced as a typed |
| 73 | + /// `Err` at the call site). |
| 74 | + Refuse(String), |
| 75 | +} |
| 76 | + |
| 77 | +/// AAPCS wants 8-byte stack alignment; LLVM typically initialises |
| 78 | +/// `__stack_pointer` 16-aligned. We round the re-based top up to 16 so frames |
| 79 | +/// stay aligned — rounding *up* preserves `B >= proven depth`, so soundness is |
| 80 | +/// not weakened. (All observed fixture `sp_init`s — 4096, 65536, 1048576 — are |
| 81 | +/// 16-aligned, so a 16-aligned `B <= sp_init` whenever the depth fits.) |
| 82 | +const STACK_ALIGN_BYTES: u64 = 16; |
| 83 | + |
| 84 | +/// Decide the shadow-stack budget `B` from a proven depth `bound`, given the |
| 85 | +/// module's original shadow-stack top `sp_init` and an optional |
| 86 | +/// integrator-asserted `fallback` (the layer-1 `--shadow-stack-size` value). |
| 87 | +/// |
| 88 | +/// - [`StackDepthBound::Bytes(n)`] → a PROVEN budget: `B = align16(n)`, source |
| 89 | +/// [`BudgetSource::ProvenStackDepth`]. Refuses if `n > sp_init` — a proven |
| 90 | +/// depth that exceeds the original reservation means the *original image |
| 91 | +/// under-provisioned its stack*, a latent bug layer-2 surfaces for free |
| 92 | +/// rather than hiding behind a generic refuse. |
| 93 | +/// - [`StackDepthBound::Unbounded`] / [`StackDepthBound::Unknown`] → no finite |
| 94 | +/// bound proven: fall back to the asserted `fallback` if given |
| 95 | +/// ([`BudgetSource::AssertedFallback`]), else refuse honestly. |
| 96 | +pub fn budget_from_bound( |
| 97 | + bound: StackDepthBound, |
| 98 | + sp_init: u32, |
| 99 | + fallback: Option<u32>, |
| 100 | +) -> BudgetDecision { |
| 101 | + match bound { |
| 102 | + StackDepthBound::Bytes(n) => { |
| 103 | + // A proven depth above the original top is an under-provisioned |
| 104 | + // image, not a shrink opportunity — name it precisely. |
| 105 | + if n > u64::from(sp_init) { |
| 106 | + return BudgetDecision::Refuse(format!( |
| 107 | + "proven shadow-stack depth {n} B exceeds the original reservation top \ |
| 108 | + sp_init={sp_init} B — the original image UNDER-provisioned its stack \ |
| 109 | + (this is a latent bug in the source, not a shrink target). Refusing. \ |
| 110 | + VCR-MEM-001 layer-2/#383." |
| 111 | + )); |
| 112 | + } |
| 113 | + // Round the re-based top up to 16-byte alignment. Since `n <= sp_init` |
| 114 | + // and `sp_init` is 16-aligned in every observed image, `align16(n) <= |
| 115 | + // sp_init`; `min` is a belt-and-braces guard for a non-aligned top. |
| 116 | + let aligned = n.next_multiple_of(STACK_ALIGN_BYTES); |
| 117 | + let bytes = aligned.min(u64::from(sp_init)) as u32; |
| 118 | + BudgetDecision::Use { |
| 119 | + bytes, |
| 120 | + source: BudgetSource::ProvenStackDepth, |
| 121 | + } |
| 122 | + } |
| 123 | + StackDepthBound::Unbounded | StackDepthBound::Unknown => match fallback { |
| 124 | + Some(b) => BudgetDecision::Use { |
| 125 | + bytes: b, |
| 126 | + source: BudgetSource::AssertedFallback, |
| 127 | + }, |
| 128 | + None => BudgetDecision::Refuse(format!( |
| 129 | + "no finite shadow-stack bound was proven ({}) and no asserted \ |
| 130 | + --shadow-stack-size fallback was given; refusing to invent a budget. \ |
| 131 | + VCR-MEM-001 layer-2/#383.", |
| 132 | + match bound { |
| 133 | + StackDepthBound::Unbounded => "recursion / call-graph cycle ⇒ unbounded", |
| 134 | + _ => |
| 135 | + "analysis incomplete ⇒ unknown (dynamic alloca, \ |
| 136 | + unresolved call_indirect, or ambiguous stack pointer)", |
| 137 | + } |
| 138 | + )), |
| 139 | + }, |
| 140 | + } |
| 141 | +} |
| 142 | + |
| 143 | +#[cfg(test)] |
| 144 | +mod tests { |
| 145 | + use super::*; |
| 146 | + |
| 147 | + // The #392 spike measured msgq's max_stack_bytes = Bytes(32); a realistic |
| 148 | + // sp_init for that image is the full 1 MiB page top. Proven depth 32 → |
| 149 | + // align16 → 32, justified ProvenStackDepth. |
| 150 | + #[test] |
| 151 | + fn proven_depth_rounds_to_16_and_is_proven() { |
| 152 | + let d = budget_from_bound(StackDepthBound::Bytes(32), 1_048_576, Some(4096)); |
| 153 | + assert_eq!( |
| 154 | + d, |
| 155 | + BudgetDecision::Use { |
| 156 | + bytes: 32, |
| 157 | + source: BudgetSource::ProvenStackDepth |
| 158 | + } |
| 159 | + ); |
| 160 | + } |
| 161 | + |
| 162 | + #[test] |
| 163 | + fn proven_depth_unaligned_rounds_up() { |
| 164 | + // 33 → next multiple of 16 = 48. |
| 165 | + let d = budget_from_bound(StackDepthBound::Bytes(33), 65_536, None); |
| 166 | + assert_eq!( |
| 167 | + d, |
| 168 | + BudgetDecision::Use { |
| 169 | + bytes: 48, |
| 170 | + source: BudgetSource::ProvenStackDepth |
| 171 | + } |
| 172 | + ); |
| 173 | + } |
| 174 | + |
| 175 | + #[test] |
| 176 | + fn zero_depth_is_proven_zero() { |
| 177 | + // sp_global present but no frame ever subtracted ⇒ Bytes(0): a proven |
| 178 | + // zero-byte stack. Stays proven; layer-1 will re-base to 0 + static tail. |
| 179 | + let d = budget_from_bound(StackDepthBound::Bytes(0), 4096, None); |
| 180 | + assert_eq!( |
| 181 | + d, |
| 182 | + BudgetDecision::Use { |
| 183 | + bytes: 0, |
| 184 | + source: BudgetSource::ProvenStackDepth |
| 185 | + } |
| 186 | + ); |
| 187 | + } |
| 188 | + |
| 189 | + #[test] |
| 190 | + fn proven_depth_above_sp_init_is_under_provision_refusal() { |
| 191 | + // A proven depth exceeding the original top is the source image's bug, |
| 192 | + // surfaced explicitly — NOT a generic refuse. |
| 193 | + let d = budget_from_bound(StackDepthBound::Bytes(8192), 4096, Some(2048)); |
| 194 | + match d { |
| 195 | + BudgetDecision::Refuse(msg) => { |
| 196 | + assert!(msg.contains("UNDER-provisioned"), "got: {msg}"); |
| 197 | + assert!(msg.contains("8192")); |
| 198 | + } |
| 199 | + other => panic!("expected under-provision refusal, got {other:?}"), |
| 200 | + } |
| 201 | + } |
| 202 | + |
| 203 | + #[test] |
| 204 | + fn proven_depth_exactly_at_top_is_accepted() { |
| 205 | + // n == sp_init is not "exceeds"; align16 keeps it at the top (no shrink |
| 206 | + // benefit, still sound and proven). |
| 207 | + let d = budget_from_bound(StackDepthBound::Bytes(4096), 4096, None); |
| 208 | + assert_eq!( |
| 209 | + d, |
| 210 | + BudgetDecision::Use { |
| 211 | + bytes: 4096, |
| 212 | + source: BudgetSource::ProvenStackDepth |
| 213 | + } |
| 214 | + ); |
| 215 | + } |
| 216 | + |
| 217 | + #[test] |
| 218 | + fn unbounded_with_fallback_is_asserted() { |
| 219 | + let d = budget_from_bound(StackDepthBound::Unbounded, 65_536, Some(8192)); |
| 220 | + assert_eq!( |
| 221 | + d, |
| 222 | + BudgetDecision::Use { |
| 223 | + bytes: 8192, |
| 224 | + source: BudgetSource::AssertedFallback |
| 225 | + } |
| 226 | + ); |
| 227 | + } |
| 228 | + |
| 229 | + #[test] |
| 230 | + fn unbounded_without_fallback_refuses() { |
| 231 | + let d = budget_from_bound(StackDepthBound::Unbounded, 65_536, None); |
| 232 | + match d { |
| 233 | + BudgetDecision::Refuse(msg) => { |
| 234 | + assert!(msg.contains("unbounded"), "got: {msg}"); |
| 235 | + assert!(msg.contains("recursion")); |
| 236 | + } |
| 237 | + other => panic!("expected unbounded refusal, got {other:?}"), |
| 238 | + } |
| 239 | + } |
| 240 | + |
| 241 | + #[test] |
| 242 | + fn unknown_with_fallback_is_asserted_not_proven() { |
| 243 | + // The critical anti-overclaim case: Unknown must NEVER yield |
| 244 | + // ProvenStackDepth, even with a fallback. |
| 245 | + let d = budget_from_bound(StackDepthBound::Unknown, 65_536, Some(1024)); |
| 246 | + assert_eq!( |
| 247 | + d, |
| 248 | + BudgetDecision::Use { |
| 249 | + bytes: 1024, |
| 250 | + source: BudgetSource::AssertedFallback |
| 251 | + } |
| 252 | + ); |
| 253 | + } |
| 254 | + |
| 255 | + #[test] |
| 256 | + fn unknown_without_fallback_refuses_with_cause() { |
| 257 | + let d = budget_from_bound(StackDepthBound::Unknown, 65_536, None); |
| 258 | + match d { |
| 259 | + BudgetDecision::Refuse(msg) => { |
| 260 | + assert!(msg.contains("unknown"), "got: {msg}"); |
| 261 | + assert!(msg.contains("call_indirect") || msg.contains("alloca")); |
| 262 | + } |
| 263 | + other => panic!("expected unknown refusal, got {other:?}"), |
| 264 | + } |
| 265 | + } |
| 266 | +} |
0 commit comments