I18 · Every journal record commits to the hash of its predecessor
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Every journal record commits to the hash of its predecessor; a broken chain is detected on read and treated as an integrity failure (§12c, §12d). This holds against damage and against anyone who cannot rewrite the whole journal and checkpoint consistently; root can, until the head is anchored off the disk (§12c).
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof, trusting SHA-256) | 5 : 3 (baseline 5 : 3, not degraded) | 3 entries, 3 must-pass |
How it is proved
5 obligations, in crates/txn/src/chain.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
follows | verified fn | The check every read path applies to each record (journal::scan). | chain.rs:97 |
verify | verified fn | Check a segment (journal::verify_chain): accepts exactly a chained segment, and otherwise reports its first break. | chain.rs:120 |
next_link | verified fn | The seq and prev the writer gives the next record (journal::append): the next seq, and the current head. | chain.rs:168 |
appending_keeps_the_chain | proof fn | I18’s writing half: a chained segment with a record appended the way next_link makes it is still chained. By induction, every journal the writer produces is chained, so a break on read is damage or an edit. | chain.rs:182 |
an_edited_record_breaks_the_chain | proof fn | An edit is caught: if a record’s next changes (its payload was edited, so its hash changed, P5) while the record after it is untouched, the segment no longer verifies. | chain.rs:214 |
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, I8 |
| P4 | Journal fsync is durable and the preallocation is writable | Platform | I6, I7, I12, I15, I24, I25 |
| U4 | Journal I/O around the verified chain: framing, torn-tail truncation, checkpoint replace | Internal unproven | — |
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-i18-deleted-record-detected | fake, vm | A retained journal record is deleted (not edited) and the rest re-framed so every frame is intact. The next read detects the break as an Integrity failure. | posture: class Integrity; reports: JournalChainBroken | fake: PASS; VM: not run in this build |
journal-record-edited | fake, vm | A retained journal record is edited on disk while the daemon runs. The next read detects the broken chain as an Integrity failure; no transaction is taken from the edited record. | invariants: I18; posture: class Integrity, target_reached planarian-failed@Integrity.target; reports: JournalChainBroken | fake: PASS; VM: not run in this build |
posture-integrity-journal-chain | vm | A record in the hash-chained journal is altered while the machine is off. The boot report finds the broken chain (I18): Integrity responses, as above. | invariants: I18, I20; posture: class Integrity, responses [“alarm”, “notify_admins”, “disable_agents”, “restrict_remote”], target_reached planarian-failed@Integrity.target; reports: BootReport(JournalChainBroken) | VM: not run in this build |
Also tested by txn journal tests.
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| B-8 | The journal hash chain is unkeyed; root can rewrite it consistently | Medium | Open (v4.5 I18, §12c) | A wording; C witness; E anchor |
| 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.4 | Invariants I16 (security floor), I17 (administrator set non-empty), I18 (hash-chained journal), I19 (no self-approval, no self-escalation), I20 (no agent without the monitor) |
| v4.4 | rule 4’s preserve list extended to I10–I20 |
| v4.5 | I18 states whom the chain holds against (B-8) |