orchestrator/sm: recovery re-boots; guard out-of-turn verification verdicts - quiesce_all: assert reset on every live component before a recovery re-walk, so recovery is a genuine platform re-boot and no live component is re-verified while running (closes the TOCTOU on already-released siblings) - VerificationPassed: release only the component under verification (chain[cursor]); drop stale/out-of-turn verdicts, mirroring the INV9 guard on ComponentReady - tests: quiesce coverage (multi-sibling, at-rest re-verify), plus a property test (INV8) asserting verify-before-release across random event sequences
diff --git a/services/orchestrator/sm/src/lib.rs b/services/orchestrator/sm/src/lib.rs index 8dd5f35..5fe7e25 100644 --- a/services/orchestrator/sm/src/lib.rs +++ b/services/orchestrator/sm/src/lib.rs
@@ -65,8 +65,12 @@ /// `E` is bounded from below by the chain length: the worst single event is a /// full cascade (up to `N` `AssertReset`s, each paired with a `ReportIsolated`) /// plus the destination `PreSupervision` entry's `ReadFirmware`/`VerifyFirmware` -/// (2), all landing in one `Sink`. `Rot::new` refuses to compile unless -/// `E >= 2 * N + 2`, so a machine that builds can never overflow this buffer. +/// (2), all landing in one `Sink`. The re-walk quiesce (an `AssertReset` per +/// live component) never pushes past this bound, because gating and quiescing +/// are mutually exclusive per component: a component the cascade isolates is not +/// also live, so the two counts never sum above the full-cascade worst case. +/// `Rot::new` refuses to compile unless `E >= 2 * N + 2`, so a machine that +/// builds can never overflow this buffer. pub struct Sink<const E: usize> { effects: heapless::Vec<Effect, E>, } @@ -156,6 +160,17 @@ /// spurious timeout. Orthogonal to `lifecycle`: a gated component owes no /// boot-progress signal, so gating clears it. awaiting_boot: bool, + /// Set while this component has been released from reset and not since held + /// again — i.e. it is *live*, executing code. Set at every `ReleaseReset`, + /// cleared at every `AssertReset` (gating, recovery, or the pre-walk + /// quiesce). This is what makes recovery a genuine platform re-boot: on + /// re-entering [`State::PreSupervision`] the machine asserts reset on every + /// live component before re-verifying, so `VerifyFirmware` never runs + /// against code that is still executing (a live check says nothing about + /// what is running and is open to a post-check flash rewrite). Distinct from + /// `awaiting_boot`, which is cleared once the component reports in but stays + /// live: a booted component is `released` yet no longer `awaiting_boot`. + released: bool, } impl Default for ComponentStatus { @@ -164,6 +179,7 @@ lifecycle: ComponentLifecycle::Nominal, retry: 0, awaiting_boot: false, + released: false, } } } @@ -272,7 +288,9 @@ // A gated component is held in reset and no longer owes a // boot-progress signal; drop any pending watchdog so a late // `Timeout` can't drag an already-isolated component into recovery. + // It is also no longer live — the `AssertReset` above holds it. self.statuses[i].awaiting_boot = false; + self.statuses[i].released = false; } true } @@ -301,10 +319,13 @@ /// Record that `id` has been released and now owes a boot-progress signal. /// Paired with the `ReleaseReset` emitted at each release site: the shell - /// arms its per-component boot watchdog there, and this arms ours. - fn mark_awaiting_boot(&mut self, id: ComponentId) { + /// arms its per-component boot watchdog there, and this arms ours. Also + /// marks the component *live* (`released`), which a later re-entry to + /// [`State::PreSupervision`] uses to quiesce it before re-verifying. + fn mark_released(&mut self, id: ComponentId) { if let Some(i) = self.status_index(id) { self.statuses[i].awaiting_boot = true; + self.statuses[i].released = true; } } @@ -347,8 +368,31 @@ false } - /// Gate a component out of service according to its [`FailurePolicy`], and - /// report the [`Gating`] outcome. This is the **single source of truth** + /// Hold the whole platform for an at-rest re-verification: assert reset on + /// every component that is currently *live* (`released`) and drop its + /// boot-progress watchdog, so the walk that follows verifies code that is + /// quiesced rather than executing. This is what makes recovery a genuine + /// platform re-boot — no released component is ever re-verified while it is + /// still running (a live check says nothing about what is executing and is + /// open to a post-check flash rewrite). + /// + /// Lifecycle is untouched: these components are held for re-check, not gated + /// (`Nominal` stays `Nominal`), and each is released again by its + /// `ReleaseReset` once it re-passes verification. Isolated components are + /// already held (`released == false`) and are skipped, as is anything under + /// active recovery. At the initial power-on walk nothing is live yet, so + /// this emits nothing and cold boot is unchanged. + fn quiesce_all(&mut self, ctx: &mut Sink<E>) { + for i in 0..self.chain.len() { + if !self.statuses[i].released { + continue; + } + let (id, _) = self.chain[i]; + ctx.emit(Effect::AssertReset(id)); + self.statuses[i].released = false; + self.statuses[i].awaiting_boot = false; + } + } /// shared by both paths that take a component out of service — the /// runtime-corruption path ([`handle_corruption`](Self::handle_corruption)) /// and the recovery-exhaustion path — so the two can never disagree about @@ -457,12 +501,22 @@ // Cursor walk via Outcome::Handled — a self-transition would reset cursor. State::PreSupervision => match event { Event::VerificationPassed(id) => { + // Only the component currently under verification + // (`chain[cursor]`, whose `VerifyFirmware` was just emitted) + // may be released. A verdict for any other id is stale or + // out-of-turn and is dropped, so a misordered or hostile + // report cannot release an unverified component (cf. INV9 + // for `ComponentReady`). + if self.chain.get(self.cursor as usize).map(|(c, _)| c) != Some(id) { + return Outcome::Handled; + } // The component passed its check — it has recovered, so its // consecutive-failure streak ends (INV7: consecutive only). self.clear_retry(*id); ctx.emit(Effect::ReleaseReset(*id)); - // Released: arm its boot-progress watchdog (both tiers). - self.mark_awaiting_boot(*id); + // Released: it is now live, and owes a boot-progress signal + // (both tiers). + self.mark_released(*id); let current_kind = self.chain.get(self.cursor as usize).map(|(_, a)| a.kind); let next_idx = (self.cursor as usize).saturating_add(1); if self.advance_to_next_ungated(ctx, next_idx) { @@ -545,12 +599,20 @@ } } Event::VerificationPassed(id) => { + // Only the component currently under verification + // (`chain[cursor]`) may be released; a verdict for any other + // id is stale or out-of-turn and is dropped (cf. INV9 for + // `ComponentReady`). + if self.chain.get(self.cursor as usize).map(|(c, _)| c) != Some(id) { + return Outcome::Handled; + } // The component passed its check — it has recovered, so its // consecutive-failure streak ends (INV7: consecutive only). self.clear_retry(*id); ctx.emit(Effect::ReleaseReset(*id)); - // Released: arm its boot-progress watchdog (both tiers). - self.mark_awaiting_boot(*id); + // Released: it is now live, and owes a boot-progress signal + // (both tiers). + self.mark_released(*id); let next_idx = (self.cursor as usize).saturating_add(1); if self.advance_to_next_ungated(ctx, next_idx) { // `Handled` preserves the current payload: `awaiting` is @@ -755,6 +817,12 @@ fn entry_action(&mut self, state: State, ctx: &mut Sink<E>) { match state { State::PreSupervision => { + // Recovery is a full platform re-boot: quiesce every live + // component before the walk, so verification always covers code + // at rest, never a component whose earlier pass says nothing + // about what it is currently running. Empty at the initial + // power-on walk (nothing live yet), so cold boot is unchanged. + self.quiesce_all(ctx); let _ = self.advance_to_next_ungated(ctx, 0); } State::Updating => { @@ -771,8 +839,13 @@ self.pending_commit = false; // The component under recovery is being restored, not booting; // drop any pending boot-progress watchdog so a late `Timeout` - // can't re-enter recovery for it. + // can't re-enter recovery for it. It is also held (not live) + // while the platform restores it, so it is not quiesced again on + // the re-walk. self.clear_awaiting_boot(failed); + if let Some(i) = self.status_index(failed) { + self.statuses[i].released = false; + } ctx.emit(Effect::RecoverComponent(failed)); } State::Locked => { @@ -815,6 +888,13 @@ /// - **Honest, complete feedback.** The reducer's correctness rests entirely on /// the event stream the shell feeds back; dropping, reordering, or /// synthesizing events silently breaks the state machine's invariants. +/// - **`AssertReset` holds, it does not pulse.** A reset must keep the component +/// quiesced and non-executing until its matching `ReleaseReset`. The reducer's +/// at-rest verification guarantee depends on this: it re-asserts reset on +/// every live component before a recovery re-walk (`quiesce_all`) so that +/// `VerifyFirmware` covers code that cannot run or rewrite its own flash +/// between the check and the release. A reset that merely pulses would let a +/// component resume before verification and void that guarantee. /// - **A failed [`Effect::LatchLockdown`] is a hard fault.** Lockdown is the top /// of the escalation ladder — the reducer has nothing stronger to emit and /// will *believe* it is `Locked`. The shell must treat that failure as
diff --git a/services/orchestrator/sm/src/tests.rs b/services/orchestrator/sm/src/tests.rs index b479509..60bf6ef 100644 --- a/services/orchestrator/sm/src/tests.rs +++ b/services/orchestrator/sm/src/tests.rs
@@ -191,6 +191,112 @@ assert_eq!(state, State::PreSupervision); } +/// Recovery is a full platform re-boot: a live sibling is held in reset before +/// the re-walk re-verifies, so `VerifyFirmware` never runs against executing +/// code. Here C0 and C1 both boot and go live; C0 is then corrupted and +/// restored. The re-walk must `AssertReset(C1)` (quiesce the live sibling) +/// before it re-reads and re-verifies C0 from a fully-held state. +#[test] +fn recovery_rewalk_quiesces_live_siblings_first() { + let (effects, state) = drive( + passive_required(&[C0, C1]), + &[ + BOOT, + Event::VerificationPassed(C0), + Event::VerificationPassed(C1), // both live → Ready + Event::CorruptionDetected(C0), // required → Recovering(C0) + Event::Restored(C0), // re-walk: quiesce C1, then re-verify C0 + ], + ); + // The re-walk holds the live sibling before any re-verification. + let tail = &effects[effects.len() - 3..]; + assert_eq!( + tail, + &[ + Effect::AssertReset(C1), + Effect::ReadFirmware(C0), + Effect::VerifyFirmware(C0), + ], + ); + assert_eq!(state, State::PreSupervision); +} + +/// `quiesce_all` holds *every* live component, not just the immediate +/// neighbor: with three live parts, recovering one asserts reset on both +/// siblings before the re-walk re-verifies anything. +#[test] +fn recovery_rewalk_quiesces_all_live_siblings() { + let (effects, state) = drive( + passive_required(&[C0, C1, C2]), + &[ + BOOT, + Event::VerificationPassed(C0), + Event::VerificationPassed(C1), + Event::VerificationPassed(C2), // all live → Ready + Event::CorruptionDetected(C0), // required → Recovering(C0) + Event::Restored(C0), // re-walk: quiesce C1 and C2 first + ], + ); + // Both live siblings are held before the re-walk re-reads the chain. + let rewalk_read = effects + .iter() + .rposition(|e| *e == Effect::ReadFirmware(C0)) + .unwrap(); + let hold_c1 = effects + .iter() + .position(|e| *e == Effect::AssertReset(C1)) + .unwrap(); + let hold_c2 = effects + .iter() + .position(|e| *e == Effect::AssertReset(C2)) + .unwrap(); + assert!(hold_c1 < rewalk_read); + assert!(hold_c2 < rewalk_read); + assert_eq!(state, State::PreSupervision); +} + +/// The TOCTOU closure: a live sibling is not trusted across a recovery on +/// its old pass. The re-walk holds it (`AssertReset`), re-verifies it from +/// that held state (`ReadFirmware`/`VerifyFirmware`), and only then releases +/// it again — so the sibling is verified twice and released twice, with the +/// hold in between. +#[test] +fn recovery_rewalk_reverifies_live_sibling_at_rest() { + let (effects, state) = drive( + passive_required(&[C0, C1]), + &[ + BOOT, + Event::VerificationPassed(C0), + Event::VerificationPassed(C1), // both live → Ready + Event::CorruptionDetected(C0), // required → Recovering(C0) + Event::Restored(C0), // re-walk: quiesce C1 + Event::VerificationPassed(C0), // re-release C0, re-read C1 + Event::VerificationPassed(C1), // re-verify C1 at rest → Ready + ], + ); + assert_eq!(state, State::Ready); + let count = |target: Effect| effects.iter().filter(|e| **e == target).count(); + // C1 is held once (quiesce), and verified + released a second time. + assert_eq!(count(Effect::AssertReset(C1)), 1); + assert_eq!(count(Effect::VerifyFirmware(C1)), 2); + assert_eq!(count(Effect::ReleaseReset(C1)), 2); + // The re-verification and re-release both come after the hold. + let hold = effects + .iter() + .position(|e| *e == Effect::AssertReset(C1)) + .unwrap(); + let reverify = effects + .iter() + .rposition(|e| *e == Effect::VerifyFirmware(C1)) + .unwrap(); + let rerelease = effects + .iter() + .rposition(|e| *e == Effect::ReleaseReset(C1)) + .unwrap(); + assert!(hold < reverify); + assert!(reverify < rerelease); +} + /// `PreSupervision` reacts to `CorruptionDetected` directly (via /// [`Rot::handle_corruption`]), even though it isn't linked to /// `SupervisingPlatform` (so `AttestationChallenge` is still discarded @@ -675,7 +781,15 @@ .count(), 1, ); - assert!(effects.contains(&Effect::AssertReset(C1))); + // C1 is held exactly once (the gate). `quiesce_all` skips it on the + // recovery re-walk because it is already held — no duplicate reset. + assert_eq!( + effects + .iter() + .filter(|e| **e == Effect::AssertReset(C1)) + .count(), + 1, + ); } /// A durable gate must survive a return to `Ready`. The gate set is *not* @@ -1720,3 +1834,135 @@ "a Restored for a non-target component must not be credited to the current recovery", ); } + +// --------------------------------------------------------------------------- +// Property / model test +// +// Instead of enumerating hand-picked traces, drive the machine with thousands +// of *arbitrary* event sequences — including nonsensical and adversarial +// orderings a hostile platform could inject — and assert the one safety +// invariant that no example-based test generalizes across the whole input +// space. It complements the example suite: those pin *behavior*, this pins +// *safety* over every ordering. +// +// The lockdown-absorbing and membership properties are intentionally *not* +// re-checked here — they are already covered by dedicated example tests +// (`self_verification_failure_latches_immediately`, the boundary-guard +// `*_out_of_chain_id_is_dropped` cases), so repeating them under the fuzzer +// would add cost without signal. +// +// Invariant checked: +// INV8 Verify-before-release. A component is released (`ReleaseReset`) +// only if it was verified (`VerifyFirmware`) since its most recent +// hold. A component starts held; `AssertReset` and `RecoverComponent` +// re-hold it. So a component is never released on a stale verification +// from before it was last taken down — the whole-input-space form of +// "recovery is a re-boot" / "no live component trusted without an +// at-rest recheck". This is the property the quiesce change introduced +// and the one no single example trace captures. +// --------------------------------------------------------------------------- + +/// SplitMix64 — a tiny, dependency-free deterministic PRNG. `no_std`/bazel +/// friendly: no external proptest/quickcheck crate required. +struct SplitMix64(u64); + +impl SplitMix64 { + fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + + /// Uniform-ish value in `0..n`. + fn below(&mut self, n: u32) -> u32 { + (self.next_u64() % n as u64) as u32 + } +} + +/// Build one random event over the given id palette. Id-less events ignore it. +fn random_event(rng: &mut SplitMix64, ids: &[ComponentId]) -> Event { + let id = ids[rng.below(ids.len() as u32) as usize]; + match rng.below(15) { + 0 => Event::VerificationPassed(id), + 1 => Event::VerificationFailed(id), + 2 => Event::ComponentReady(id), + 3 => Event::Booted(id), + 4 => Event::BootConfirmed(id), + 5 => Event::CorruptionDetected(id), + 6 => Event::Restored(id), + 7 => Event::Timeout(id), + 8 => Event::AttestationChallenge, + 9 => Event::UpdateRequest, + 10 => Event::UpdateVerified, + 11 => Event::UpdateRejected, + 12 => Event::RecoveryFailed, + 13 => Event::CommitTimeout, + _ => Event::EffectFailed, + } +} + +#[test] +fn property_verify_before_release_holds_under_random_sequences() { + const RUNS: u64 = 4000; + const MAX_LEN: u32 = 24; + + // C0..C2 are in-chain; C3 is intentionally out-of-chain — fed as noise so + // the fuzzer also exercises the dispatch-boundary guard, but membership is + // asserted by the dedicated boundary-guard example tests, not here. + let palette = [C0, C1, C2, C3]; + + for seed in 0..RUNS { + let mut rng = SplitMix64(seed.wrapping_mul(0xD1B5_4A32_D192_ED03).wrapping_add(1)); + + let ch = chain(&[ + (C0, ComponentAttrs::passive_required()), + (C1, ComponentAttrs::active_isolable()), + (C2, ComponentAttrs::passive_required()), + ]); + let mut orch = + Orchestrator::<CAPACITY, ECAP>::new(ch.try_into().expect("valid chain"), MAX_RETRY); + let mut platform = Recorder::new(); + + // Power on first — usually a clean provisioned boot, occasionally a + // degraded power-on result so lockdown paths get exercised too. + let boot = match rng.below(12) { + 0 => Event::PowerGood(PowerOnResult::Unprovisioned), + 1 => Event::PowerGood(PowerOnResult::SelfVerificationFailed), + _ => BOOT, + }; + orch.dispatch(&mut platform, boot); + + let len = 1 + rng.below(MAX_LEN); + for _ in 0..len { + let event = random_event(&mut rng, &palette); + orch.dispatch(&mut platform, event); + } + + // Post-hoc structural scan over the full effect trace. + let trace = &platform.recorded; + + // INV8: verify-before-release. A component starts held; AssertReset + // and RecoverComponent re-hold it; VerifyFirmware clears it for release. + let mut verified = [false; CAPACITY]; + + for effect in trace { + match effect { + Effect::AssertReset(id) | Effect::RecoverComponent(id) => { + verified[id.get() as usize] = false; + } + Effect::VerifyFirmware(id) => { + verified[id.get() as usize] = true; + } + Effect::ReleaseReset(id) => { + assert!( + verified[id.get() as usize], + "seed {seed}: released {id:?} without a verify since its last hold", + ); + } + _ => {} + } + } + } +}