I13 · A unit under an override is never a repair target while the override holds
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
A unit under an override is never a repair target while the override holds.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A, C (proof) | 3 : 2 (baseline 0 : 1, not degraded) | 2 entries, 1 must-pass |
How it is proved
3 obligations, in crates/exec/src/kani.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
residue_security_is_never_intended | Kani harness | A security-sensitive unit’s stop is never taken as intended: it is alarmed (§11, Q5). | kani.rs:94 |
residue_crashes_are_faults | Kani harness | Crash signals, exit statuses and OOM kills of a failed unit are faults, never a person’s stop (§11, Q5). | kani.rs:105 |
residue_is_inferred_only_where_allowed | Kani harness | What Planarian did itself, or what went down with a crash, is never a residue; nor is anything under a posture that does not infer intent, a unit systemd restarts, or one that must keep running. | kani.rs:116 |
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 |
|---|---|---|---|
| P6 | systemd reports unit state truthfully over D-Bus and honors X-RestartIfChanged / X-StopIfChanged | Platform | I4, I20, I24 |
| U3 | The residue classifier (§11: which unit endings are a person’s stop) | Internal unproven | — |
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), V11 (Kani and its back end CBMC are sound within the stated bounds).
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
en-i13-overridden-unit-is-not-repaired | fake, vm | An administrator stops gym-web until they say otherwise. For the next ten minutes gym-web stays stopped and under the override: no repair is proposed for it, and nothing restarts it. | overrides: service:gym-web; txn: Committed StopAndSuppress, service:gym-web RestartUnit; units: service:gym-web Overridden | fake: PASS; VM: not run in this build |
intent-user-stops-service | fake, vm | An admin asks to stop gym-web until they say otherwise. It stays stopped. The override is journaled before the stop, so there is no window in which a repair can race it. | journal_order: Override(service:gym-web), stop(service:gym-web); no_autonomous_txn: true; overrides: service:gym-web; txn: Committed StopAndSuppress; units: service:gym-web Overridden | fake: PASS; VM: not run in this build |
Also tested by incident tests.
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 |
See also
—