I10 · No change that removes or alters a canonical probe executes below AskFirst, and canonica…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
No change that removes or alters a canonical probe executes below AskFirst, and canonical probes are evaluated from the installed core package regardless of the active generation.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A | 1 : 2 (baseline 1 : 2, not degraded) | 4 entries, 4 must-pass |
How it is proved
1 obligation, in crates/policy/src/proofs.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
i10_canonical_probe_changes_ask | proof fn | I10, and probe tampering (§17a): a change to a canonical probe’s definition never runs below AskFirst. | proofs.rs:237 |
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, I11, I16, I19, I21, I22 |
| U1 | exec::derive: DerivedFacts from the evaluated generation, never from a proposal (I14’s other half; property-tested) | Internal unproven | I14, I21, 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-i10-a-canonical-probe-cannot-be-removed | fake | A configuration change drops sshd’s canonical probe from the manifest (removes it, not weakens it). Below AskFirst it may run, but the probe does not go: the probe definitions the daemon evaluates are the same afterwards, because the core ships the canonical probe and puts it back. | probe_definitions_unchanged: true | fake: PASS |
gen-disable-reenable-canonical | fake, vm | An admin disables sshd (which has a canonical Readiness probe) and later re-enables it. Disabling makes the probe inapplicable without tampering with it, so neither change is reverted. | journal_agrees: true; no_incident_on: service:sshd; override_source: candidate; txn: Committed ApplyChange, Committed ApplyChange; units: service:sshd Running | fake: PASS; VM: not run in this build |
manifest-weaken-out-of-band | vm | The owner weakens sshd’s probe in their own config and rebuilds outside Planarian. Canonical probes are still evaluated from the core package, so a later sshd fault is still detected. | canonical_probe_source: core; status_seen: service:sshd [“Degraded”] | VM: not run in this build |
manifest-weaken-via-proposal | fake, vm | A proposal tries to raise sshd’s canonical probe timeout to 600 s and mark it Diagnostic. No catalog entry can express that, so it is rejected and never executed. | generation: base; probe_definitions_unchanged: true; txn: ApplyChange | fake: PASS; VM: not run in this build |
Also tested by state 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 |