I5 · Forbidden actions are unrepresentable as transitions
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Forbidden actions are unrepresentable as transitions;
Decision::Rejectis never converted to any tier by any setting.— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof) | 4 : 3 (baseline 4 : 3, not degraded) | 1 entry, 1 must-pass |
How it is proved
4 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 |
|---|---|---|---|
decide | verified fn | (no doc comment) | lib.rs:869 |
i5_autonomy_never_touches_reject | proof fn | I5: the autonomy setting never turns a Reject into a tier or a tier into a Reject, never changes a Reject’s reason, never yields a tier above itself other than AskFirst, and raising it never makes a decision stricter. | proofs.rs:73 |
unauthorized_is_refused_first | proof fn | Unauthorized callers are refused before anything else is considered. | proofs.rs:246 |
core_is_never_a_target | proof fn | The core is never a target. | proofs.rs:255 |
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 | I10, I11, I16, I19, I21, I22 |
| V2 | Value is an opaque external type (external_type_specification); nothing about it is assumed | Proof-validity | I11, I16, I21 |
| V3 | Serde impls are unverified (external_derive) | Proof-validity | I6, I14 |
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-i5-reject-survives-every-setting | fake | With autonomy at its maximum, a change touching Planarian’s own unit is refused, not raised to a tier; with the setting changed and the change asked again, it is refused again. No setting turns the refusal into an approval to ask for. | txn: 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
See also
planarian_policy in rustdoc · planarian_policy::proofs in rustdoc