I19 · No principal approves its own proposal, and no principal grants itself, or a principal i…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
No principal approves its own proposal, and no principal grants itself, or a principal it controls, a capability it does not hold.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof), C | 3 : 3 (baseline 3 : 3, not degraded) | 3 entries, 3 must-pass |
How it is proved
3 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 |
|---|---|---|---|
i19_no_self_approval | proof fn | I19: no approver approves its own proposal, and an Administrator class is approved only by an administrator; nobody grants a capability to themselves or one they do not hold. | proofs.rs:215 |
may_approve | verified fn | (no doc comment) | lib.rs:923 |
may_grant | verified fn | (no doc comment) | lib.rs:942 |
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, I21, I22 |
| U2 | user_authorization and the administrator lookup (planarian-admin membership, root) | Internal unproven | I17, I22 |
| U5 | Identity resolution (§10): peer credentials and pidfd to logind session, seat, terminal | Internal unproven | I21, I24 |
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 |
|---|---|---|---|---|
authz-user-overrides-firewall | fake | From her session, alice overrides the firewall (sshd’s stand-in in the fake: a Security unit) to stopped. Held for an administrator; it stays up. alice cannot approve her own request (I19); root at a terminal approves, and the override holds, attested and attributed to alice. | invariants: I19; overrides: service:sshd; txn: Committed SetOverride | fake: PASS |
en-i19-no-self-approval | fake, vm | Root proposes an AskFirst change and then, at a terminal, tries to approve it: refused, and the change never runs. (A principal granting itself a capability has no request to make in Phase A: capabilities come from group membership only.) | txn: pending ApplyChange; units: service:sshd Running | fake: PASS; VM: not run in this build |
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 |
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 | Phase A proof targets add I16 (in decide and target selection) and I19 |
| v4.4 | rule 4’s preserve list extended to I10–I20 |
See also
planarian_policy in rustdoc · planarian_policy::proofs in rustdoc