I17 · The set of principals holding administrator capability is never empty
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
The set of principals holding administrator capability is never empty.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof, given root exists) | 2 : 2 (baseline 0 : 2, not degraded) | 1 entry, 1 must-pass |
How it is proved
2 obligations, in crates/policy/src/lib.rs, crates/policy/src/proofs.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
is_administrator | verified fn | (no doc comment) | lib.rs:1014 |
i17_administrators_never_empty | proof fn | I17 (A, given root exists): root holds the administrator capability whatever the group file says, so the set of principals holding it is never empty; no change to the group can empty it. | proofs.rs:327 |
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 |
|---|---|---|---|
| P8 | The kernel and systemd are correct | Platform | I1, I2, I3, I9, I20, I22 |
| U2 | user_authorization and the administrator lookup (planarian-admin membership, root) | Internal unproven | I19, I22 |
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-i17-root-administers-without-the-group | fake | Nobody is left in planarian-admin, so the group grants no one administrator capability. Root still holds it: root’s administrator-only change (gym-web’s listen address) is authorized and commits. | txn: Committed ApplyChange; units: service:gym-web Running | fake: PASS |
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| 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 | rule 4’s preserve list extended to I10–I20 |
| v4.6 | the Phase A proof status stated, with the residue Kani harnesses and the I17 proof named as still required [D4] |
See also
planarian_policy in rustdoc · planarian_policy::proofs in rustdoc