I25 · Post-commit bookkeeping (security-floor derivation, the committed generation’s override …
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Post-commit bookkeeping (security-floor derivation, the committed generation’s override content, session accounting) runs on every path that writes
Committedfor a generation transaction: the daemon’s, the watchdog’s, the boot-only confirmation’s. A commit whose floor record cannot be appended does not commit (§12, §12e).— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Tested, not proved | A | 0 : 2 (baseline 0 : 2, not degraded) | 3 entries, 3 must-pass |
How it is proved
No obligation discharges it: nothing about it is proved.
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 |
|---|---|---|---|
| P1 | Backend Outcome is honest: Succeeded means applied; Unknown means the backend cannot say | Platform | I3, I12 |
| P4 | Journal fsync is durable and the preallocation is writable | Platform | I6, I7, I12, I15, I18, I24 |
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
floor-moves-via-boot-only | fake | A security update that also needs a reboot takes the boot-only path: published to boot once, the machine restarts, the boot is confirmed and the change commits. The floor moves to it, as on the live path. | security_floor: candidate; txn: Committed ApplyChange | fake: PASS |
floor-moves-via-watchdog | fake | The daemon is killed once the security update is Promoted and stays down; the watchdog completes the commit. The floor moves to the fixing generation: the floor record is part of the commit, whoever writes Committed. | security_floor: candidate; txn: Committed ApplyChange | fake: PASS |
revert-to-older-sets-no-floor | fake | gym-newlib 1.0 is added, then a release makes it 2.0, which carries knownVulnerabilities. Undoing back to the 1.0 generation is a Revert to an older generation that merely lacks the newer package: it sets no security floor (§12e). | security_floor: none; txn: Committed Revert | 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
| Spec | Change |
|---|---|
| v4.6 | I25: post-commit bookkeeping on every commit path |
| v4.6 | rule 4’s preserve list to I25 [D5] |