I14 · Policy facts (sensitivity, affected units, manifest-touching, caller identity) are deriv…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Policy facts (sensitivity, affected units, manifest-touching, caller identity) are derived by the executor from the evaluated generation and the authenticated peer, never read from a proposal or from any other request field.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof of the decide half; the request half by test) | 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 |
|---|---|---|---|
i14_facts_caller_is_not_authority | proof fn | I14: the caller recorded in the derived facts carries no authority; only the daemon-established Authorization does. | proofs.rs:290 |
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 |
|---|---|---|---|
| U1 | exec::derive: DerivedFacts from the evaluated generation, never from a proposal (I14’s other half; property-tested) | Internal unproven | I10, I21, I22 |
| V3 | Serde impls are unverified (external_derive) | Proof-validity | I5, I6 |
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 |
|---|---|---|---|---|
approve-needs-real-terminal | fake, vm | Root approves a pending AskFirst change from a process with no controlling terminal (a new session, as a service would be). The daemon reads the terminal from the peer’s pidfd, finds none, and refuses: the change is still waiting at the end. The request carries no terminal field to claim. | txn: pending ApplyChange; units: service:sshd Running | fake: PASS; VM: not run in this build |
authz-forged-actor-overwritten | fake, vm | alice submits a SetOverride for her own pipewire with by = Daemon. SO_PEERCRED overwrites the actor to user:1000; the override is allowed and attributed to her. | overrides: service@1000:pipewire | fake: PASS; VM: not run in this build |
catalog-change-carries-unbuilt-owner-edit | fake | An administrator has edited the owner’s configuration to enable a service but not rebuilt. alice then asks for a user-controllable change (font scale). The candidate would also bring the new service, which the override does not explain, so the change is Security-sensitive: it waits for approval instead of activating on its own. | generation: base; reports: NeedsApproval | fake: PASS |
en-i14-forged-fields-ignored | fake, vm | An administrator who is not root submits a change to sshd whose request also claims caller root, sensitivity Routine and no affected units. The claims are ignored: the change is decided on derived facts (Security, sshd affected), held at AskFirst for approval, and not run. | txn: ApplyChange; units: service:sshd Running | fake: PASS; VM: not run in this build |
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| B-4 | decide is proved, but its inputs (DerivedFacts, Authorization) are computed by unproven code | Medium | Open (v4.5 §17a) | A accounting; C proof |
| 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 | Policy facts derived by the executor from the evaluated generation (I14) |
| v4.4 | rule 4’s preserve list extended to I10–I20 |
| v4.5 | §7: principle 6 and I14 extended from proposals to every request field (B-3) |