I2 · The installed core package’s hash equals the hash recorded in its signature
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
The installed core package’s hash equals the hash recorded in its signature. In A–D the reference hash is recorded by the build and covers every Planarian binary and script (§12d); it detects a swapped file, not a rebuilt generation.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Tested, not proved | E | 0 : 2 (baseline 0 : 2, not degraded) | 2 entries, 2 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 |
|---|---|---|---|
| P5 | SHA-256 is collision-resistant (the journal’s hash chain, I18) | Platform | I8, I18 |
| P8 | The kernel and systemd are correct | Platform | I1, I3, I9, I17, I20, I22 |
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
posture-integrity-core-hash | vm | The recorded core hash no longer matches its signature (I2). planarian-recovery’s independent check fails the boot as Integrity: tamper alarm, notify, no agents, remote access off; local login proceeds with the warning. Only an administrator clears it. | invariants: I2, I20; not_started: service:gym-agent; posture: class Integrity, not [“halt_to_recovery”], responses [“alarm”, “notify_admins”, “disable_agents”, “restrict_remote”], target_reached planarian-failed@Integr… | VM: not run in this build |
posture-integrity-core-script | vm | One posture script (planarian-ack), not planariad, no longer matches its line in the core-hash record. planarian-recovery checks every Planarian binary and script, so the boot fails as Integrity all the same (B-12). | invariants: I2; posture: class Integrity, target_reached planarian-failed@Integrity.target | VM: not run in this build |
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-3 | Firmware, bootloader and initrd run before planarian-ready.target | Accepted | Accepted | C, E |
| 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.5 | I2 states what the A–D core hash detects (B-12) |