I22 · Changing the generation, collecting garbage, binding drivers, resolving the recovery int…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Changing the generation, collecting garbage, binding drivers, resolving the recovery interlock and overriding a Security-sensitive unit are administrator operations; a Security-sensitive unit is changed without approval only to restore its declared state (§11); the unattributed actor holds no authority, and an agent holds exactly its user’s (§11).
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof) | 5 : 4 (baseline 5 : 4, not degraded) | 3 entries, 2 must-pass |
How it is proved
5 obligations, in crates/policy/src/proofs.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
users_cannot_change_generations | proof fn | A user who is not an administrator cannot change generations, drivers, models, snapshots or the store. | proofs.rs:276 |
only_administrators_resolve | proof fn | Only an administrator can clear the recovery interlock (§12c). | proofs.rs:266 |
security_override_held_for_administrator | proof fn | §11: a non-administrator’s override of a Security-sensitive unit is held for an administrator, never rejected as unauthorized and never run on its own; other rejections (the core, a lock) still apply. | proofs.rs:179 |
security_restart_runs_alone_only_to_restore | proof fn | §11 (owner gap G16, decided 2026-10-29): a restart of a Security-sensitive unit runs below AskFirst only when it restores a unit stopped outside Planarian and not attributed, and the unit is not also External, or is but has already failed; or when it restarts a failed network-security unit whose traffic is held (§12d; owner decision, Nov 2). | proofs.rs:196 |
agents_and_unattributed_are_refused | proof fn | Neither an agent principal with no journaled start (reserved), nor the model (until Phase B grants it anything), nor the unattributed actor is ever authorized: an inferred override never passes through decide (§11). | proofs.rs:227 |
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, I16, I19, I21 |
| P8 | The kernel and systemd are correct | Platform | I1, I2, I3, I9, I17, I20 |
| U1 | exec::derive: DerivedFacts from the evaluated generation, never from a proposal (I14’s other half; property-tested) | Internal unproven | I10, I14, I21 |
| U2 | user_authorization and the administrator lookup (planarian-admin membership, root) | Internal unproven | I17, I19 |
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-i22-user-cannot-do-admin-things | fake, vm | A seated, unprivileged user tries, in turn, to roll back, collect garbage, bind a driver and resolve the interlock. Each is refused Unauthorized; nothing executes. | no_txn_executed: true; reports: Unauthorized; txn: Rollback, CollectGarbage, BindDriver, Resolve | fake: PASS; VM: not run in this build |
residue-kill9-security | fake, vm | A raw kill -9 of sshd (Security-sensitive) is a fault under every posture: alarmed, never inferred, and back up: restored by Planarian on its own (§11; catalog-review G16, decided 2026-10-29), or by systemd where its Restart= does it first (NixOS’s sshd), which is then alarmed from systemd’s restart count. | overrides: ; reports: alarm; units: service:sshd Running | fake: PASS; VM: not run in this build |
residue-stop-security-unit | fake, vm | Root stops sshd (Security-sensitive) with systemctl stop outside Planarian. An unattributed stop of a Security unit is never taken as intended: it is restored on its own and alarmed. | overrides: ; reports: alarm; txn: service:sshd RestartUnit; units: service:sshd Running | fake: PASS; VM: not run in this build |
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| B-4 | decide is proved, but its inputs (DerivedFacts, Authorization) are computed by unproven code | Medium | Open (v4.5 §17a) | A accounting; C proof |
| 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 |
| X-10 | A program a user runs under their own uid, outside planarian agent run (an agent started by hand from a shell) | Accepted | Accepted | C |
| X-11 | An agent holds its user’s capabilities, including Administrator when an administrator starts it (owner decision, 2026-10-30) | Accepted | Accepted | — |
History
No changes section names it.