amadan
Isolated exec spec: revision 10 after codex round 9
Round 9 findings committed unedited. Both accepted: ProtectControlGroups=yes in the templates and the probe; /var/cache and /var/lib hidden from instances; a same-uid audit rule and test over the unit set.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YZ1ZvWj7naf73GjTX8MBv5
2 files changed,
+82
−3
docs/superpowers/specs/2026-09-11-isolated-exec-design.md+37 −3docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R9.md+45 −0
CI passed — run details
diff --git a/docs/superpowers/specs/2026-09-11-isolated-exec-design.md b/docs/superpowers/specs/2026-09-11-isolated-exec-design.md| index def5d1cc0..4c411ca73 100644 |
| --- a/docs/superpowers/specs/2026-09-11-isolated-exec-design.md |
| +++ b/docs/superpowers/specs/2026-09-11-isolated-exec-design.md |
| @@ -1,7 +1,7 @@ |
| # Isolated exec — every exec-backed instance in its own namespace |
| -**Date:** 2026-09-11 · **Status:** revision 9, after codex rounds 1 to 8 |
| -(19 + 14 + 7 + 4 + 3 + 1 + 1 + 1 findings, all accepted; §13) · **Requested by:** discussion |
| +**Date:** 2026-09-11 · **Status:** revision 10, after codex rounds 1 to 9 |
| +(19 + 14 + 7 + 4 + 3 + 1 + 1 + 1 + 2 findings, all accepted; §13) · **Requested by:** discussion |
| #126 (Tito, with box evidence), approved in direction by Paul on |
| 2026-09-11 |
| @@ -609,11 +609,20 @@ StandardError=inherit |
| ProtectSystem=strict |
| TemporaryFileSystem=/data:ro |
| TemporaryFileSystem=/run/carlos:ro |
| +# Every other tree a carlos-uid unit writes on the box is hidden the same |
| +# way (codex R9-2): the restore drills' cache under /var/cache, and |
| +# /var/lib as a class. An instance needs nothing from either. |
| +TemporaryFileSystem=/var/cache:ro |
| +TemporaryFileSystem=/var/lib:ro |
| BindPaths=/data/instances/%I /run/carlos/instances/%I |
| ReadWritePaths=/data/instances/%I /run/carlos/instances/%I |
| ProtectHome=yes |
| PrivateTmp=yes |
| PrivateDevices=yes |
| +# /sys/fs/cgroup read-only: the edge's delegated subtree is carlos-owned, |
| +# and its cgroup.kill / cgroup.freeze would otherwise be one write away |
| +# for a same-uid tenant (codex R9-1). |
| +ProtectControlGroups=yes |
| ProtectProc=invisible |
| ProcSubset=pid |
| PrivatePIDs=yes |
| @@ -687,6 +696,24 @@ Lines that are load-bearing and why: |
| the path is in `/run/carlos/logs`, which no tenant mount contains, and |
| that directory is on a `nosymfollow` mount, so a same-uid process |
| outside any namespace cannot turn it into a symlink either. |
| +- **`ProtectControlGroups=yes`** (codex R9-1). `ProtectSystem=strict` |
| + leaves kernel API filesystems alone and `ProtectKernelTunables=` leaves |
| + `/sys/fs/cgroup` writable; the edge unit's `Delegate=` subtree, |
| + including the `supervise/` cgroup the agent moves itself into |
| + (`internal/cgroup/cgroup.go:172`), is created by `carlos` and its |
| + `cgroup.kill` and `cgroup.freeze` are owner-writable. A same-uid |
| + tenant with a writable cgroupfs could kill or freeze the agent with |
| + no pid and no socket. Read-only cgroupfs closes that; an instance has |
| + no business in cgroupfs at all. |
| +- **`TemporaryFileSystem=/var/cache:ro` and `/var/lib:ro`** (codex |
| + R9-2). The isolation property is "no same-uid path on the box but its |
| + own", and two trees outside `/data` and `/run/carlos` are written by |
| + `carlos`-uid units: `carlos-hibernate-verify.service` and |
| + `carlos-restore-verify.service` set `CacheDirectory=carlos-verify` and |
| + restore every host's database into `/var/cache/carlos-verify` during a |
| + drill (`internal/ops/ops.go:274`, `internal/lease/check.go:79`), and |
| + `/var/lib` holds unit tenants' state. Both are hidden. §9 carries the |
| + audit rule that found them, so the next such unit is caught at review. |
| - **`/opt/carlos`** stays readable through `ProtectSystem=strict`; the |
| trampoline and the live symlink are all the instance needs from it. |
| @@ -1614,7 +1641,9 @@ instance-probe`. From inside it asserts, and reports each as a separate |
| verdict line: |
| - `/data` and `/run/carlos` list nothing but the probe's own bound |
| - directories; |
| + directories, and `/var/cache` and `/var/lib` list nothing at all; |
| +- a write to `cgroup.kill` under any cgroup directory it can name |
| + (its own included) fails with `EROFS`; |
| - `/proc` lists only itself, and its own pid is 1; |
| - a symlink it creates in its directory is refused with `ELOOP`, and |
| `/proc/self/mountinfo` shows `nosymfollow` on both bound directories; |
| @@ -1746,6 +1775,7 @@ instance as an enrolled non-`carlos` uid |
| - `internal/host/systemunits.go:34-83` (active check on the socket) |
| - `update-platform-binary.sh:52-70` (pinfra): enables the new units by name before restarting the edge |
| - `harden-host.sh` (pinfra) writes hardening drop-ins for `$TENANT_UNITS`; the instance templates carry their own and must not be listed there |
| +- **The same-uid audit** (codex R9-1, R9-2): every unit in `internal/host/units/` that runs as `User=carlos` or delegates a `carlos`-owned tree, and every path it writes, is a path an isolated instance must not see. Today: `carlos-edge.service` (`/data`, `/run/carlos`, its delegated cgroup subtree), `carlos-litestream.service` (`/data`), `carlos-hibernate-verify.service` and `carlos-restore-verify.service` (`/var/cache/carlos-verify`). A test over `unitsFS` lists every `User=carlos` unit's `ReadWritePaths=`, `CacheDirectory=`, `StateDirectory=`, `RuntimeDirectory=` and `Delegate=` and asserts each resulting tree is covered by a `TemporaryFileSystem=`, `InaccessiblePaths=` or `ProtectControlGroups=` line in the templates, so a future unit that writes somewhere new fails the build until the templates hide it |
| **Tests that pin the flat layout** (§10): `internal/activator/activator_test.go` (20 fixture sites), `backend_exec_test.go` (4), `admintoken_test.go` (8, path-agnostic), `internal/appconfig/syncexec_test.go` (50), `internal/ops/ops_test.go` (52), `internal/provision/reconcile_test.go` (20), `internal/host/movespass_test.go` (1), `schedule_wiring_test.go` (1), `schedule_token_fence_test.go` (2), root `e2e_test.go` (24), `instances_e2e_test.go`, `config_e2e_test.go`, `deploy_e2e_test.go`. For this release they keep passing on the flat path; each gains a nested twin. |
| @@ -2033,3 +2063,7 @@ rollback runs the old binary). |
| - **Round 8** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R8.md`, 1 new |
| finding, every prior item resolved, verdict request changes). Accepted: |
| R8-1 the wake re-reads the row before `Acquire` and runs on it; the layout pass reloads routing before releasing the fence (§6.8, §8.2). |
| +- **Round 9** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R9.md`, 2 new |
| + findings, every prior item resolved, verdict request changes). Both accepted: |
| + R9-1 `ProtectControlGroups=yes` in the templates and the probe; the probe writes `cgroup.kill` and expects `EROFS` (§4.1, §8.5); |
| + R9-2 `/var/cache` and `/var/lib` hidden; the same-uid audit rule and its test added to §9 (§4.1, §8.5, §9). |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R9.md b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R9.md| new file mode 100644 |
| index 000000000..f52a7e670 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R9.md |
| @@ -0,0 +1,45 @@ |
| +| Prior finding | Disposition at `d76f5364` | |
| +|---|---| |
| +| R8-1 | **Resolved at spec level.** Wake refreshes the committed row before `Acquire`; migration reloads routing before releasing admission (§§6.8, 8.2). | |
| +| R5-2 | **Resolved.** Downgrade checks every row’s paths regardless of flags; unflagging nested rows is refused (§8.2). | |
| +| R5-3 | **Resolved.** Unit and socket names use the bounded `InstanceID` (§§3.1, 5.3). | |
| +| R2-4 | **Resolved.** Blocking seed execution and `RemainAfterExit=yes` retain identity and results through capture (§§4.2, 5.3). | |
| +| R2-5 | **Resolved.** Completion requires terminal state and cgroup emptiness; uncertain stops retain replication and the lease (§§6.3, 6.5). | |
| +| R2-7 | **Resolved.** Recovery derives both endpoints from journal direction, completes that transaction, then converges to current intent (§8.2). | |
| +| R2-9 | **Resolved.** Flat minting, explicit reversal and downgrade guards cover the reported failures (§§8.1–8.2). | |
| +| R2-14 | **Resolved at spec level.** The IPv6 exception is explicit, bounded, rechecked and reported (§8.5). | |
| +| R1-4 | **Resolved.** Completion is independent of log EOF; blocking observations remain outside the activator mutex (§§6.4–6.7). | |
| +| R1-5 | **Resolved.** Preparation, execution budget, cancellation, result retention and termination-before-cleanup are specified (§§6.1–6.5). | |
| +| R1-8 | **Resolved under the recorded decision.** Shared tier limits remain; per-service OOM families are an explicit difference (§4.3). | |
| +| R1-12 | **Resolved.** Consumer fences and bidirectional recovery cover interrupted migration (§8.2). | |
| +| R1-13 | **Resolved.** Reverse recovery and completed-reversal downgrade guards address the reported defects (§8.2). | |
| +| R1-15 | **Resolved for the reported PID/IMDS defects.** No unsafe fallback remains; the behavioural gate is specified (§8.5). | |
| +| R1-18 | **Resolved under the recorded ruling.** Remote operations and reporting are specified; the `foreign` repair residual remains explicitly accepted (§§8.3–8.4). | |
| + |
| +**R9-1 — P1 — §§5.4, 4.1, 6.6: A tenant can stop the agent without using the authenticated channel.** |
| + |
| +Retain §5.4’s process-authenticated control service. The namespace leaves a separate process-control path available. |
| + |
| +The [template’s hardening block](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:608) omits `ProtectControlGroups=`. `ProtectSystem=strict` excludes kernel API filesystems, and systemd explicitly leaves `/sys/fs/cgroup` writable under `ProtectKernelTunables=yes` unless control-group protection is enabled. [systemd namespace implementation](https://raw.githubusercontent.com/systemd/systemd/v257/src/core/namespace.c). |
| + |
| +Section 6.6 retains the delegation machinery for this release. That machinery [creates `supervise/` as `carlos` and moves the agent into it](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/cgroup/cgroup.go:172). Linux creates its control files with the creator’s ownership and owner-write permission. Consequently, the specified tenant can write `1` to: |
| + |
| +```text |
| +/sys/fs/cgroup/carlos.slice/carlos-edge.service/supervise/cgroup.kill |
| +``` |
| + |
| +That kills the agent; writing to the adjacent `cgroup.freeze` freezes it. These operations require no visible target PID and no connection to the control service. PID isolation therefore does not prevent them. [Linux ownership and kill implementation](https://raw.githubusercontent.com/torvalds/linux/v6.12/kernel/cgroup/cgroup.c), [cgroup control semantics](https://docs.kernel.org/6.12/admin-guide/cgroup-v2.html). |
| + |
| +**Correction:** add `ProtectControlGroups=yes` to all three tenant templates and the probe, preserving the agent’s delegation separately. Require a behavioural check that a tenant cannot write the agent’s delegated cgroup controls. |
| + |
| +**R9-2 — P1 — §§4.1, 8.5, 9: Restore drills expose sibling databases outside the hidden data tree.** |
| + |
| +Both [hibernate verification](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/host/units/carlos-hibernate-verify.service:38) and [ordinary restore verification](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/host/units/carlos-restore-verify.service:35) set `CacheDirectory=carlos-verify`, `TMPDIR=%C/carlos-verify` and `User=carlos`. This creates a host directory at `/var/cache/carlos-verify`, owned by the same uid as every isolated tenant. `PrivateTmp=yes` isolates `/tmp` and `/var/tmp`; it does not hide that cache directory. [systemd execution semantics](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.exec.xml). |
| + |
| +The [hibernate drill creates its temporary directory there](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/ops/ops.go:274), then [restores each sibling’s database into `verify-<host>.db`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/lease/check.go:79). A tenant can enumerate and read those files while verification runs. Mode 0700 does not separate identical uids, and the tenant’s read-only view still permits reading. The ordinary drill exposes its restored database set through the same directory. |
| + |
| +The §8.5 probe can pass throughout: it checks `/data` and `/run/carlos`, while these copies live under `/var/cache`. |
| + |
| +**Correction:** hide the verifier workspace from every tenant role, retaining disk-backed restores. Add both verification units to §9’s isolation audit and test sibling-database unreadability while a restore drill holds a restored copy. |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |