I24 · An agent’s authority is bound to the one AgentStarted record for the unit instance it …
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
An agent’s authority is bound to the one
AgentStartedrecord for the unit instance it runs in, identified by that instance (not by name); a second start under the same name neither rebinds a running agent nor is journaled before it has succeeded (§11, §16).— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Tested, not proved | A | 0 : 3 (baseline 0 : 3, not degraded) | 1 entry, 1 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 |
|---|---|---|---|
| P4 | Journal fsync is durable and the preallocation is writable | Platform | I6, I7, I12, I15, I18, I25 |
| P6 | systemd reports unit state truthfully over D-Bus and honors X-RestartIfChanged / X-StopIfChanged | Platform | I4, I13, I20 |
| U5 | Identity resolution (§10): peer credentials and pidfd to logind session, seat, terminal | Internal unproven | I19, I21 |
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
agent-name-collision | fake, vm | alice (uid 1000) starts an agent named helper. An administrator then runs planarian agent run helper too: refused, naming alice as its owner. alice’s agent stays alice’s: its stop of gym-web, a system unit she may not stop, is refused. Authority is bound to the instance a start journaled, never the name (I24). | reports: AgentNameInUse; txn: service:gym-web StopAndSuppress; units: service:gym-web Running | fake: PASS; VM: not run in this build |
Also tested by daemon core 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-10 | A program a user runs under their own uid, outside planarian agent run (an agent started by hand from a shell) | Accepted | Accepted | C |
History
| Spec | Change |
|---|---|
| v4.6 | I24: agent authority bound per instance |