I8 · A tier-3 transition executes only with an approval token bound to the concrete candidate…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
A tier-3 transition executes only with an approval token bound to the concrete candidate (§12), re-validated immediately before execution. “Immediately before execution” includes the moment a transaction leaves
Builtafter waiting for an activation window: facts are re-derived,decidere-run and the stale check repeated there too, not only at approval.— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A, C (proof) | 1 : 1 (baseline 1 : 1, not degraded) | 4 entries, 4 must-pass |
How it is proved
1 obligation, in crates/exec/src/kani.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
approval_tokens_expire_after_their_lifetime | Kani harness | Approval tokens (§12 step 4), timed on the boot clock (§12h: the values here are CLOCK_BOOTTIME, which moving the wall clock cannot move): never expired at or before issue, expired exactly once 24 hours have passed, and once expired they stay expired. No clock value makes the check overflow. | kani.rs:14 |
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 |
|---|---|---|---|
| P5 | SHA-256 is collision-resistant (the journal’s hash chain, I18) | Platform | I2, I18 |
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 |
|---|---|---|---|---|
approval-token-expired | fake | A parked AskFirst change gets no approval for 24 h. It ends Rejected, its GC root is released, and any waiting incident reopens. | gc_root_released: true; txn: ApplyChange | fake: PASS |
approval-token-invalidated | fake | A token is issued for a parked AskFirst change, then the policy version changes. Re-validation invalidates the token and re-requests approval, and replaying the old token is refused. | reports: ApprovalInvalidated, TokenReplayRefused; txn: ApplyChange | fake: PASS |
en-i8-token-bound-to-candidate | fake, vm | An AskFirst change is approved; before it runs, the owner edits the configuration so the candidate it would build differs. The token, bound to the old candidate, does not authorise the new one. | txn: Rejected(Stale) ApplyChange | fake: PASS; VM: not run in this build |
token-wall-clock-moved-back | fake | An approval token is held, then the wall clock is moved back 48 h and 24 h pass. The token still expires 24 h after issue, timed on CLOCK_BOOTTIME (§12h): presenting it is refused and the parked change ends Rejected. | txn: ApplyChange | fake: PASS |
Also tested by exec 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 |
| X-8 | The approver: fatigue, social engineering, persuasion by a model | Accepted | Accepted | — |
History
| Spec | Change |
|---|---|
| v4 | Restored principles (now 12) and invariants (I1–I14) that v3 referenced but omitted |
| v4.6 | I8: re-validation also when leaving Built [C2, P1] |