I16 · No automatic revert, rollback, or boot fallback selects a generation below the security …
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
No automatic revert, rollback, or boot fallback selects a generation below the security floor; going below it requires administrator approval (§12e). The floor is derived from the whole system closure (§12e); a fix outside the inspected set does not move it.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof of the decide and target-selection parts; the bootloader part by test) | 2 : 3 (baseline 2 : 3, not degraded) | 5 entries, 5 must-pass |
How it is proved
2 obligations, in crates/policy/src/proofs.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
i16_below_floor_needs_administrator | proof fn | I16 (the decide part): a transition whose target generation is below the security floor is AskFirst for an administrator, or refused, whatever the autonomy setting, the transition kind, or the caller. | proofs.rs:161 |
administrator_class_only_on_ask_first | proof fn | An Administrator approver class only ever comes with AskFirst. | proofs.rs:170 |
What it rests on
If any of these is false, the proof no longer describes the real machine.
| Id | Assumption | Kind | Also relied on by |
|---|---|---|---|
| V1 | vstd’s specifications of Vec, String::as_str, str::unicode_len, str::get_char | Proof-validity | I5, I10, I11, I19, I21, I22 |
| V2 | Value is an opaque external type (external_type_specification); nothing about it is assumed | Proof-validity | I5, I11, I21 |
| P3 | publish_boot and the override promotion rename are idempotent | Platform | I1, I23 |
Every proof also rests on V7 (The specifications the proofs prove against (decide_spec, step_spec, inv, chained, the lemma statements) say what the SPEC’s English means), V8 (Verus is sound: what it reports verified holds of the code), V9 (Z3, the solver Verus calls, is sound), V10 (rustc compiles the verified code to a program with the semantics Verus checked).
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
en-i16-boot-fallback-respects-floor | fake | After a security update raises the floor, the machine restarts and the boot fails. The automatic fallback does not select a generation below the floor: the boot default and the generation that boots are the floor. | boot_default: candidate; generation: candidate; security_floor: candidate | fake: PASS |
floor-manual-rollback-needs-admin | fake | After the security update, an administrator asks to roll back below the floor: AskFirst for an Administrator approver. The proposer cannot approve it (I19); root at a terminal can. | generation: base; security_floor: candidate; txn: Committed Rollback | fake: PASS |
floor-moves-via-watchdog | fake | The daemon is killed once the security update is Promoted and stays down; the watchdog completes the commit. The floor moves to the fixing generation: the floor record is part of the commit, whoever writes Committed. | security_floor: candidate; txn: Committed ApplyChange | fake: PASS |
floor-revert-blocked | fake | A security update (gym-vulnlib 1.0 → 1.1, the old build carries knownVulnerabilities) commits and raises the floor. gym-web then crashes and fails every restart. The only rollback target, known_good, is below the floor: no Rollback runs, the incident escalates with RevertBlockedByFloor, and the boot default stays at the floor. | boot_default: candidate; escalation: RevertBlockedByFloor; generation: candidate; incident: service:gym-web; invariants: I1, I16; security_floor: candidate; txn: Committed ApplyChange, Rollback | fake: PASS |
floor-service-package-fix | vm | A change whose only security fix is in a service’s package (gym-vulnsvc 1.0 -> 1.1; services.gym-vulnsvc.package, never in environment.systemPackages) commits. The security floor moves to it: the inspected set is the configuration’s whole package set, not environment.systemPackages. | security_floor: candidate; txn: Committed ApplyChange | VM: not run in this build |
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| B-19 | A package referenced only by a store-path string (an ExecStart= naming /nix/store/… directly, a script’s interpolated path) has no meta to read at evaluation, so a fix to it does not move the security floor | Medium | Open | B |
| X-1 | Root edits the store, /boot, the binaries, the journal or the posture state | Accepted | Accepted | E |
| X-2 | A nixos-rebuild outside Planarian | Accepted | Accepted | C |
| X-4 | Physical access | Accepted | Accepted | E |
| X-6 | The supply chain: nixpkgs content, cache signatures, input-addressed store paths | Accepted | Accepted | — |
| X-7 | Backends report success falsely; systemd or the kernel misbehave (P1, P6, P8) | Accepted | Accepted | D, E |
History
| Spec | Change |
|---|---|
| v4.4 | Invariants I16 (security floor), I17 (administrator set non-empty), I18 (hash-chained journal), I19 (no self-approval, no self-escalation), I20 (no agent without the monitor) |
| v4.4 | Phase A proof targets add I16 (in decide and target selection) and I19 |
| v4.4 | rule 4’s preserve list extended to I10–I20 |
| v4.5 | I16 states the inspected set (B-2) |