amadan
Isolated exec spec: revision 11 after codex round 10
Round 10 findings committed unedited. Accepted: InaccessiblePaths=/etc/carlos in the templates and the probe; the same-uid audit covers credential inputs a carlos-group process reads, not only directories it writes.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YZ1ZvWj7naf73GjTX8MBv5
2 files changed,
+62
−3
docs/superpowers/specs/2026-09-11-isolated-exec-design.md+27 −3docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R10.md+35 −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 4c411ca73..c0af6bf55 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 10, after codex rounds 1 to 9 |
| -(19 + 14 + 7 + 4 + 3 + 1 + 1 + 1 + 2 findings, all accepted; §13) · **Requested by:** discussion |
| +**Date:** 2026-09-11 · **Status:** revision 11, after codex rounds 1 to 10 |
| +(19 + 14 + 7 + 4 + 3 + 1 + 1 + 1 + 2 + 1 findings, all accepted; §13) · **Requested by:** discussion |
| #126 (Tito, with box evidence), approved in direction by Paul on |
| 2026-09-11 |
| @@ -614,6 +614,12 @@ TemporaryFileSystem=/run/carlos:ro |
| # /var/lib as a class. An instance needs nothing from either. |
| TemporaryFileSystem=/var/cache:ro |
| TemporaryFileSystem=/var/lib:ro |
| +# Root-written credentials a carlos-GROUP process may read live here: |
| +# /etc/carlos/relay-masters is root:carlos 0640 for carlos-relay.service, |
| +# and an instance's Group=carlos would read it too (codex R10-1). An |
| +# instance gets its configuration through its launch file and needs |
| +# nothing from /etc/carlos. |
| +InaccessiblePaths=/etc/carlos |
| BindPaths=/data/instances/%I /run/carlos/instances/%I |
| ReadWritePaths=/data/instances/%I /run/carlos/instances/%I |
| ProtectHome=yes |
| @@ -714,6 +720,17 @@ Lines that are load-bearing and why: |
| 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. |
| +- **`InaccessiblePaths=/etc/carlos`** (codex R10-1). `ProtectSystem=strict` |
| + makes `/etc` read-only, not unreadable. `carlos-relay.service` runs as |
| + `carlos:carlos` and reads `/etc/carlos/relay-masters` |
| + (`internal/relay/masters.go:101`), which the relay design stages as |
| + `root:carlos 0640` (`2026-09-07-relay-stun-turn-design.md:325`): a |
| + file every `Group=carlos` process can read, and the secret every |
| + app's relay key is derived from (`internal/relay/server.go:665`). |
| + The instance's group is `carlos` for the socket contract (§3.1), so |
| + the directory is hidden outright. `host.env` and `apps/*.env` there |
| + are root-0600 and were already unreadable; hiding the directory is |
| + what makes the next `0640` file safe by default. |
| - **`/opt/carlos`** stays readable through `ProtectSystem=strict`; the |
| trampoline and the live symlink are all the instance needs from it. |
| @@ -1644,6 +1661,9 @@ verdict line: |
| 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`; |
| +- `/etc/carlos` cannot be opened (`EACCES` or `ENOENT`, never a |
| + listing), and a fixture file the control service stages beforehand |
| + as `root:carlos 0640` at `/etc/carlos/probe-secret` cannot be read; |
| - `/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; |
| @@ -1775,7 +1795,8 @@ 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 |
| +- **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. |
| + **Reads count too** (codex R10-1): the same audit covers every file a `User=carlos` or `Group=carlos` unit *reads* that is not world-readable by design, which today is `/etc/carlos/relay-masters` (`root:carlos 0640`, `internal/relay/masters.go:101`) and the alternate path the relay design allows for it; the audit's second table lists each such file, its owner and mode, and the template line that hides it (`InaccessiblePaths=/etc/carlos`). A new credential input for a `carlos`-group reader is added to that table, or the test fails |
| **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. |
| @@ -2067,3 +2088,6 @@ rollback runs the old binary). |
| 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). |
| +- **Round 10** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R10.md`, 1 new |
| + finding, every prior item resolved, verdict request changes). Accepted: |
| + R10-1 `InaccessiblePaths=/etc/carlos` in the templates and the probe; the audit extends to credential inputs a `carlos`-group process reads (§4.1, §8.5, §9). |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R10.md b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R10.md| new file mode 100644 |
| index 000000000..df8a53916 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R10.md |
| @@ -0,0 +1,35 @@ |
| +| Prior finding | Disposition at `251e4d3c` | |
| +|---|---| |
| +| R9-1 | **Resolved.** `ProtectControlGroups=yes` covers all tenant roles and the probe; §8.5 requires a refused cgroup-control write. | |
| +| R9-2 | **Resolved for the reported restore-drill exposure.** `/var/cache` and `/var/lib` are hidden (§§4.1, 8.5). | |
| +| R8-1 | **Resolved.** 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.** Directory, socket, unit and slice 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 the journal’s 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). | |
| + |
| +**R10-1 — P1 — §§4.1, 8.5, 9: Isolated tenants can read the platform relay’s region master.** |
| + |
| +Retain §5.4’s process-authenticated control service. Extend the filesystem boundary to platform credential inputs. |
| + |
| +The [tenant template](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:609) leaves `/etc/carlos` visible. `ProtectSystem=strict` makes that directory read-only; it does not prevent reading its files. [systemd execution semantics](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.exec.xml). |
| + |
| +The existing [relay unit](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/host/units/carlos-relay.service:18) runs as `carlos:carlos`. Its [masters reader](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/relay/masters.go:101) opens `/etc/carlos/relay-masters` directly. The [relay design specifies `root:carlos`, mode `0640`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-07-relay-stun-turn-design.md:325), so every isolated tenant’s `Group=carlos` grants the same read. |
| + |
| +On a box armed according to that contract, a tenant can therefore read and exfiltrate the region master. This exposes the secret from which the relay [derives each app’s authentication key](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/relay/server.go:665), including other accounts’ keys. |
| + |
| +The probe can pass throughout. The new [§9 audit](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1778) inventories writable directories, so it misses a root-written credential that a platform process only reads. |
| + |
| +**Correction:** hide `/etc/carlos` from all three tenant templates and the probe. Extend §9’s audit to credential inputs, including the relay masters file and supported alternate locations. Require a behavioural check that a tenant cannot read a fixture master staged with the relay’s actual ownership and permissions. |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |