I20 · No agent (the on-device model, a remote relay, or any agent started by `planarian agent …
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
No agent (the on-device model, a remote relay, or any agent started by
planarian agent run) starts whileplanarian-ready.targetis not reached, and every running agent is stopped when a failure posture engages, in every posture (§12d). Agents the launcher creates are inside this rule exactly as the units declared inservices.planarian.agentUnits(the model service and any relay) are.— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Tested, not proved | A | 0 : 2 (baseline 0 : 2, not degraded) | 7 entries, 7 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 |
|---|---|---|---|
| P6 | systemd reports unit state truthfully over D-Bus and honors X-RestartIfChanged / X-StopIfChanged | Platform | I4, I13, I24 |
| P8 | The kernel and systemd are correct | Platform | I1, I2, I3, I9, I17, I22 |
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
posture-absent-masked | vm | planariad is masked and the machine rebooted. planarian-ready.target times out; Standard’s Absent responses apply; the agent stand-in never starts; unmasking and a clean ready lifts them. | invariants: I20; not_started: service:gym-agent; posture: class Absent, not [“restrict_login”, “halt_to_recovery”, “alarm_dismissable”], responses [“alarm”, “notify_admins”, “disable_agents”, “restrict_remote”], target… | VM: not run in this build |
posture-crashed-budget | vm | planariad reaches ready, then is killed until its restart budget is spent. OnFailure= reaches planarian-failed@Crashed; responses as Absent; agents stop; an administrator’s acknowledgement is journaled with identity. | invariants: I20; posture: class Crashed, not [“restrict_login”], responses [“alarm”, “notify_admins”, “disable_agents”, “restrict_remote”], target_reached planarian-failed@Crashed.target; reports: AlarmAcknowledged(use… | VM: not run in this build |
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 |
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 |
posture-integrity-undeclared-early-unit | vm | A unit outside the generation’s closure is planted to start before planarian-ready. The boot report names it and Integrity responses apply. (Phase A’s boot report checks units only, and planariad stops on the finding rather than opening an incident: catalog review G18.) | posture: class Integrity, responses [“alarm”, “notify_admins”, “disable_agents”, “restrict_remote”], target_reached planarian-failed@Integrity.target; reports: BootReport(UndeclaredEarly: service:gym-planted) | VM: not run in this build |
posture-stops-launched-agents | vm | An administrator launches an agent with planarian agent run (in planarian-agents.slice). planariad then crash-loops past its restart budget: planarian-failed@Crashed stops the agents’ slice as a whole, so the launched agent stops too, not only the declared agent units. | invariants: I20; posture: class Crashed, responses [“disable_agents”], target_reached planarian-failed@Crashed.target; unit_after_failure: service:planarian-agent-launched Stopped | VM: not run in this build |
Also tested by vm-posture.
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| B-9 | Posture alarms and notification are local; root can clear them and a stopped planariad can go unnoticed | Medium | Open (v4.5 §12d) | C |
| B-10 | The boot report checks units, not processes | Medium | Open (v4.5 §10) | C |
| 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.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.6 | I20: launched agents inside the rule [R05] |