I11 · A session’s cumulative effect is classified at least as high as any single transition pr…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
A session’s cumulative effect is classified at least as high as any single transition producing it.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof) | 2 : 2 (baseline 2 : 2, not degraded) | 1 entry, 1 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 |
|---|---|---|---|
i11_non_routine_session_asks | proof fn | I11 (classification): when this change’s diff, or the session’s cumulative diff, touches a non-Routine option, the decision is AskFirst or a Reject. | proofs.rs:95 |
i11_session_only_raises | proof fn | I11 (monotonicity): a change inside a session is decided at least as strictly as the same change on its own. | proofs.rs:118 |
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, I16, I19, I21, I22 |
| V2 | Value is an opaque external type (external_type_specification); nothing about it is assumed | Proof-validity | I5, I16, I21 |
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-i11-session-carries-its-sensitivity | fake | In one session, an administrator changes the firewall (Security: approved by root at a terminal, committed), then asks for a display-scale change, Routine on its own. The session’s cumulative effect includes the firewall change, so the second is classified at least as high: AskFirst, not as itself. | txn: Committed ApplyChange, ApplyChange | 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 | Restored principles (now 12) and invariants (I1–I14) that v3 referenced but omitted |
| v4.4 | rule 4’s preserve list extended to I10–I20 |