amadan
Isolated exec spec: revision 5 after codex round 4
Round 4 findings committed unedited. All accepted: /data/.instances bound onto /data/instances so the migration rename stays on one mount; the root-peer dial rule replaced by a path allowlist plus getpeername equality; only host-named files at the platform's paths ever move; the v6 IMDS answer comes from sendto, no route query; seed correlation via start --no-block; journals validated at both endpoints.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YZ1ZvWj7naf73GjTX8MBv5
2 files changed,
+252
−97
docs/superpowers/specs/2026-09-11-isolated-exec-design.md+193 −97docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R4.md+59 −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 dfb734168..9a6d2066e 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 4, after codex rounds 1 to 3 |
| -(19 + 14 + 7 findings, all accepted; §13) · **Requested by:** discussion |
| +**Date:** 2026-09-11 · **Status:** revision 5, after codex rounds 1 to 4 |
| +(19 + 14 + 7 + 4 findings, all accepted; §13) · **Requested by:** discussion |
| #126 (Tito, with box evidence), approved in direction by Paul on |
| 2026-09-11 |
| @@ -262,7 +262,8 @@ scoped to the three instance templates and does not extend to |
| ### 3.1 Layout |
| ``` |
| -/data/instances/ bind mount of itself, nosymfollow (§3.2); 0755 carlos:carlos |
| +/data/.instances/ the RAW directory: 0700 carlos:carlos; opened by the layout pass only (§3.2, §8.2) |
| +/data/instances/ nosymfollow bind mount OF /data/.instances (§3.2); the view everything else uses |
| /data/instances/<host>/ 0700 carlos:carlos, created by the agent |
| <host>.db the database (+ -wal, -shm) |
| .activator-<host>.db-litestream/ the in-process replicator's shadow |
| @@ -368,7 +369,7 @@ Before=carlos-edge.service carlos-instance-control.service carlos-litestream.ser |
| Conflicts=umount.target |
| Before=umount.target |
| [Mount] |
| -What=/data/instances |
| +What=/data/.instances |
| Where=/data/instances |
| Type=none |
| Options=bind,nosymfollow,nosuid,nodev,noexec |
| @@ -376,13 +377,33 @@ Options=bind,nosymfollow,nosuid,nodev,noexec |
| WantedBy=multi-user.target |
| ``` |
| +**The source is a different directory from the mountpoint** (codex |
| +R4-2). `rename(2)` refuses to cross a mount boundary with `EXDEV` even |
| +when both sides are one filesystem, so a bind of `/data/instances` onto |
| +itself would make the migration's rename from `/data/<host>.db` into it |
| +impossible. Binding `/data/.instances` onto `/data/instances` keeps the |
| +raw directory reachable on the `/data` mount: the layout pass renames |
| +`/data/<host>.db` → `/data/.instances/<host>/<host>.db` on one mount, |
| +atomically, and the file appears at `/data/instances/<host>/<host>.db` |
| +through the protected view. The raw path is opened by **exactly one |
| +caller**, the layout pass, and only as `openat2(RESOLVE_NO_SYMLINKS | |
| +RESOLVE_BENEATH)` directory fds for `renameat`, so no lookup through it |
| +ever follows a symlink either; a CI test greps the tree for the literal |
| +`.instances` and fails on any other occurrence. |
| + |
| `run-carlos-instances.mount` and `run-carlos-logs.mount` are the same |
| -text for `/run/carlos/instances` and `/run/carlos/logs`, with |
| -`After=systemd-tmpfiles-setup.service` and no `RequiresMountsFor=`. |
| +shape for `/run/carlos/.instances` → `/run/carlos/instances` and |
| +`/run/carlos/.logs` → `/run/carlos/logs`, with |
| +`After=systemd-tmpfiles-setup.service` and no `RequiresMountsFor=`; |
| +nothing is ever renamed into those, so their raw directories have no |
| +caller at all. |
| ``` |
| -d /data/instances 0755 carlos carlos - |
| -d /data/layout 0700 carlos carlos - |
| +d /data/.instances 0700 carlos carlos - |
| +d /data/instances 0755 carlos carlos - |
| +d /data/layout 0700 carlos carlos - |
| +d /run/carlos/.instances 2750 carlos carlos-sockets - |
| +d /run/carlos/.logs 0700 carlos carlos - |
| d /run/carlos/instances 2750 carlos carlos-sockets - |
| d /run/carlos/logs 0700 carlos carlos - |
| d /run/carlos-control 0750 root carlos - |
| @@ -429,9 +450,10 @@ What this closes, race-free and for every reader at once: |
| The flat tenants' own sockets under `/run/carlos` itself are not on such |
| a mount (the directory holds flat sockets, the apps subtree and more, and |
| this release does not change it). A flat tenant can therefore still point |
| -its socket at any socket on the box and have the edge dial it. §5.4 says |
| -why that no longer reaches the control service, and §6.1 adds the one |
| -check the edge makes on every unix dial. |
| +its socket at any socket on the box, by symlink or by editing the |
| +registry row it can reach as `carlos`, and have the edge dial it. §5.4 |
| +says why that no longer reaches the control service, and §6.1 names the |
| +two checks the edge and the agent make on every unix dial. |
| Belt and braces in the agent, cheap and testable: |
| @@ -784,7 +806,7 @@ itself: |
| | Verb | What it runs | Returns | Agent deadline | |
| |---|---|---|---| |
| | `POST /start?host=H&role=run\|sidecar&memory_max=N` | `systemctl set-property --runtime carlos-instances-<esc>.slice MemoryMax=N MemoryHigh=0.9N MemorySwapMax=N`; `systemctl start <unit>` (blocking: the start job completes) | 200 with `{invocation_id}` from `systemctl show -p InvocationID <unit>`, read immediately after the start returns; or 502 with systemctl's stderr | 30s | |
| -| `POST /seed?host=H&memory_max=N` | the same, on `carlos-instance-seed@<esc>.service` (oneshot: `start` blocks until exit or `TimeoutStartSec`); then `systemctl show -p InvocationID,Result,ExecMainStatus,ExecMainCode` | 200 with `{invocation_id, result, status, code}` if the unit is still loaded, else 200 with `{invocation_id: ""}` and the agent reads the exit record (§6.5) | 150s: 120s seed budget plus `TimeoutStopSec` and slack (R3-5) | |
| +| `POST /seed?host=H&memory_max=N` | the same `set-property`; `systemctl start --no-block` on `carlos-instance-seed@<esc>.service`; **immediately** `systemctl show -p InvocationID` (the unit is `activating` and has one); then wait until the unit is terminal and its cgroup empty (§6.5's rule, applied by the service as root), then `systemctl show -p Result,ExecMainStatus,ExecMainCode` | 200 with `{invocation_id, result, status, code}`; `result` is `unknown` if the unit unloaded before the final `show` | 150s: 120s seed budget plus `TimeoutStopSec` and slack (R3-5) | |
| | `POST /stop?host=H&role=run\|seed\|sidecar` | `systemctl stop <unit>` (blocking; also cancels a pending start job) | 204 | 30s | |
| | `POST /reset?host=H&role=…` | `systemctl reset-failed <unit>`, tolerating "not loaded" | 204 | 30s | |
| | `GET /ready` | nothing | 204 once the probe verdict (§8.5) is `ready`; 503 with the verdict otherwise | 5s | |
| @@ -852,19 +874,34 @@ can is **systemd's own record of which process is the agent**: |
| the socket at all. |
| - The edge is the agent, so a request the edge *proxies* for a tenant |
| (a flat tenant pointing its own socket at `control.sock`, §3.2) would |
| - pass that check. It does not get that far: **the edge refuses any unix |
| - dial whose peer is uid 0** (`SO_PEERCRED` after `connect`, before a |
| - byte is sent; `edge.go:2000-2014`'s `unixProxy` and the activator's |
| - health and control dials, §6.1). Instances are `carlos` or a |
| - DynamicUser; the only root-owned listener the platform ever wants a |
| - tenant's traffic near is none. A proxied request therefore never |
| - reaches the service, and the service never sees a connection from |
| - anything but the agent's own goroutines. |
| - |
| -No token. The file it lived in is gone, and with it the question of who |
| -can read it. The two checks are each one syscall and one cached |
| -`systemctl show`, both testable with a fake peer, and both hold on a box |
| -that still runs flat tenants, which is the whole transition. |
| + pass that check. It does not get that far, because of two checks on |
| + **every unix dial the edge and the agent make** (`edge.go:2000-2014`'s |
| + `unixProxy`, the activator's health and control dials, §6.1): |
| + 1. **the path is allowed before the dial**: it must be under |
| + `/run/carlos/` (flat sockets, `instances/`, `apps/`), so a registry |
| + row pointing at `/run/carlos-control/control.sock` is refused |
| + before `connect()`; |
| + 2. **the listener answers to the path that was dialled**: after |
| + `connect()` and before a byte is sent, `getpeername()` on the |
| + connected socket returns the address the *listener* bound, which is |
| + its real path however it was reached; if that is not byte-equal to |
| + the path the edge dialled, the connection is closed. A symlink at |
| + `/run/carlos/<host>.sock` pointing anywhere, including a sibling's |
| + socket or the control socket, therefore yields a mismatch. |
| + Revision 4's rule, "refuse a peer whose uid is 0", is withdrawn: a |
| + listener created by PID 1 for `carlos-app@.socket` reports root |
| + credentials in `SO_PEERCRED` however the fd is later passed |
| + (codex R4-1), so that rule would have refused every unit-backed app. |
| + The two checks above do not look at credentials at all. |
| + |
| +A proxied request therefore never reaches the service, and the service |
| +never sees a connection from anything but the agent's own goroutines. |
| +No token: the file it lived in is gone, and with it the question of who |
| +can read it. Each check is one syscall or one cached `systemctl show`, |
| +each is testable with a real socket pair, and all of them hold on a box |
| +that still runs flat tenants, which is the whole transition. They also |
| +end, as a side effect, the flat-tenant socket impersonation §1.2 names, |
| +which a symlink could otherwise still perform during this release. |
| --- |
| @@ -901,7 +938,7 @@ included (R1-5, R2-12): |
| `Start` is then: `prepare(rt, "run")`; `POST /start` with the route's |
| tier; `waitHealthyCtx(ctx, rt.Socket, spawnHealthTimeout)` (unchanged, |
| -with the peer-uid check of §5.4 on its dial); the `0660` normalisation of |
| +with the path and `getpeername` checks of §5.4 on its dial); the `0660` normalisation of |
| `app.sock` (unchanged); on failure `POST /stop`, wait for the proc's |
| `done`, and clean up, exactly as the current failure path stops the |
| child; return a `unitProc` carrying the invocation id. |
| @@ -1086,12 +1123,24 @@ not a lease release. |
| An `InvocationID` that is neither the proc's own nor empty means someone |
| restarted the unit outside the activator, which `Restart=no` does not |
| -forbid. The goroutine logs `unit restarted outside the activator`, |
| -treats its own invocation as gone (terminal, status unknown) once its |
| -own cgroup emptiness cannot be told apart from the newcomer's, and the |
| -sweeper's stand-down then `POST /stop`s whatever is running; the agent |
| -owns these units and any other invocation is an anomaly to end, not to |
| -adopt. |
| +forbid. The goroutine logs `unit restarted outside the activator` and |
| +**`POST /stop`s the unit itself**, then keeps waiting: `done` closes |
| +only when the unit is terminal and its cgroup is empty, whichever |
| +invocation the processes belonged to (codex R2-5 disposition). The |
| +agent owns these units and any other invocation is an anomaly to end, |
| +not to adopt; the invocation id decides the event line's wording and |
| +nothing about whether a writer is gone. |
| + |
| +**The seed's status is the one place a record is more than wording.** |
| +`/seed` returns systemd's `result`/`status` when the unit was still |
| +loaded at the final `show`, and `unknown` otherwise (§5.3). In the |
| +`unknown` case the agent reads the seed's exit record and takes its |
| +status. That record is tenant-writable, but a seed is the tenant's own |
| +code seeding the tenant's own database: a forged "success" leaves the |
| +tenant with whatever database its seed produced, and a forged "failure" |
| +deletes the tenant's own fresh database and restores nothing. The only |
| +party a seed record can deceive is its author, so it is allowed to |
| +decide the seed's outcome and nothing else. |
| `sweepOnce`'s existing dead-child check (`activator.go:1105-1122`) sees a |
| flag, never a blocking call. `Restart=no` in the template is what makes |
| @@ -1255,7 +1304,6 @@ The exec backend classifies each activator-managed route on every |
| | `DBPath == DefaultDBPath` (flat), `Socket == DefaultSocket` (flat) | `flat` | today's `childProc`, unchanged, unisolated | |
| | `DBPath == NestedDBPath`, `Socket == NestedSocket` | `nested` | `unitProc` (§6) | |
| | a journal exists in `/data/layout/<host>.json` | `fenced` | refuses to wake; reason from the journal | |
| -| `DBPath` under `DataDir` and `Socket` under `SocketDir`, otherwise | `custom` | today's `childProc`; migrated from its actual paths by the pass (§8.3) | |
| | anything else | `foreign` | today's `childProc`; reported for the operator (§8.3) | |
| A fleet rolled to this release behaves byte-for-byte as before until an |
| @@ -1286,23 +1334,33 @@ needed) and, per host in scope, in this order: |
| route with a socket is an externally supervised process (titogo's |
| router family is the live example); its files and rows are **not |
| touched**, it is not isolated by this change, and status reports it |
| - `external`. Under mode `nested`, `flat` and `custom` rows migrate; |
| - under mode `flat`, `nested` rows revert; `fenced` rows recover first; |
| - `foreign` rows are reported and skipped. |
| + `external`. Under mode `nested`, `flat` rows migrate; under mode |
| + `flat`, `nested` rows revert; `fenced` rows recover first; `foreign` |
| + rows are reported and skipped. |
| 2. **Quiesce.** The pass asks the activator to stop the host |
| (`Bounce`-class stop with replication closed and the lease released, |
| the same sequence `stop()` runs, including §6.3's refusal to release |
| over an unproven stop) and to refuse wakes for it until the pass is |
| done. Nothing is writing. |
| -3. **Plan, in memory, from the row and the host name only.** Sources are |
| - the row's actual `DBPath` and `Socket` (for a `flat` row these are the |
| - flat defaults; for a `custom` row whatever the operator stamped, as |
| - long as they are under `DataDir` and `SocketDir`) and the siblings |
| - derived from them (`-wal`, `-shm`, the litestream shadow dir, |
| - `<host>.env`, `<host>-sidecar.env`, `<host>.config.env`, |
| - `<host>.db.corrupt` in the source directory); destinations are the |
| - §3.1 helpers. Nothing is read from the instance directory to build |
| - the plan (§3.3). |
| +3. **Plan, in memory, from the row and the host name only, and only |
| + for files named after the host.** Each source follows its existing |
| + contract (codex R4-3): the database is the row's `DBPath`, and |
| + `-wal`, `-shm`, the litestream shadow dir and `.corrupt` are derived |
| + from it (`backend_exec.go:273, 1041-1057`, `lease.go:286`); the three |
| + env files are `DataDir`-relative regardless of `DBPath` |
| + (`backend_exec.go:785-794, 865-868`). The socket is the row's |
| + `Socket`. And every source must be **a file named `<host>` plus a |
| + platform suffix, directly under `DataDir` or `SocketDir`**: the row's |
| + `DBPath` must be `<DataDir>/<host>.db` and its `Socket` |
| + `<SocketDir>/<host>.sock`, which is what `flat` means (§8.1). A row |
| + naming any other path is `foreign` (§8.3) and the pass does not touch |
| + it, because during the transition the registry is writable by every |
| + flat tenant (same uid, §1.3) and a row is therefore not a trustworthy |
| + instruction to move an arbitrary file: a tenant that could point its |
| + `DBPath` at `/data/console/console.db` and have the pass move it |
| + into the tenant's directory would have the platform's own database. |
| + Destinations are the §3.1 helpers. Nothing is read from the instance |
| + directory to build the plan (§3.3). |
| 4. **Ownership preflight** (R2-8). For every flat source name, compute |
| every route on the box that could own that name under the flat |
| rules: `<host>.config.env` is `host`'s sync-owned bundle **unless** a |
| @@ -1345,12 +1403,20 @@ needed) and, per host in scope, in this order: |
| `Socket` up on its next registry poll (`edge.go:449-451`, ~2s). |
| **Recovery is the journal, and it is exact, and it is checked** (R2-7, |
| -R3-1). On agent start and at the top of every layout pass, for each |
| -journal: recompute the plan from the row (step 3); if the journal's |
| -`from`/`to` differ from the recomputation, or its `mode` differs from |
| -the fleet's recorded intent, the journal is refused (`layout: <host>: |
| -journal does not match row or intent; not acting`), the host stays |
| -`fenced`, and status says so. Otherwise: |
| +R3-1, R4 disposition). On agent start and at the top of every layout |
| +pass, for each journal, the check is against **both endpoints**, because |
| +the row is at `from` before step 8 and at `to` after it: the journal's |
| +`to` must equal the destination the §3.1 helpers derive for that host |
| +in the journal's own `mode`, its `from` must be the host-named flat |
| +paths of step 3, and the row must currently equal either `from` or `to`. |
| +A journal that fails any of those is refused (`layout: <host>: journal |
| +does not match row; not acting`), the host stays `fenced`, and status |
| +says so. **A journal that passes is completed to its own endpoint even |
| +if the fleet's intent has since changed**: a transaction runs to its |
| +recorded end, and the host is then converged to the current intent in |
| +the same pass, before it is released to the activator, so a forged or |
| +stale journal can at most add one round trip a host never runs |
| +unisolated through. Otherwise: |
| - `phase: files`: for each artifact recorded present: at destination → |
| done; at source → rename; at neither → error, fence stays, status |
| @@ -1380,24 +1446,27 @@ the nested one, and the revert's step 5 handles the stray env files when |
| the new binary is back. The layout is never two databases: the fence |
| and the destination check see to that. |
| -### 8.3 `custom` and `foreign` rows |
| - |
| -A row whose `DBPath` or `Socket` is neither default was set by hand |
| -(`carlos add --db`; `carlos route` has no `--db` flag, `cli.go:469-475`, |
| -so it was set at add time). If both paths are still under `DataDir` and |
| -`SocketDir` the row is `custom` and **the pass migrates it from the |
| -paths it actually names** (step 3), through the console verb like every |
| -other row (R1-18). Only a row naming a path outside those trees is |
| -`foreign`: it is reported with both values, keeps running on today's |
| -flat path, and `carlos add` on the box, re-adding the route with the |
| -defaults, is the repair, box-local because the row was made box-locally. |
| -A console-provisioned row (`reconcile.go:300-301`) is never either. |
| +### 8.3 `foreign` rows |
| + |
| +A row whose `DBPath` or `Socket` is neither the flat nor the nested |
| +default was set by hand (`carlos add --db`; `carlos route` has no `--db` |
| +flag, `cli.go:469-475`, so it was set at add time). The pass does not |
| +move it, for the reason step 3 gives: while flat tenants share the |
| +agent's uid, a row is not a trustworthy instruction to move an arbitrary |
| +file, and the only files the pass will move are the ones named after |
| +the host at the platform's own paths. A `foreign` row is reported with |
| +both values, keeps running on today's flat path, and `carlos add` on |
| +the box, re-adding the route with the defaults, is the repair: box-local |
| +because the row was made box-locally, and because a remote verb that |
| +moved operator-named files would be the primitive this section refuses |
| +to build (R1-18, accepted as the residual). A console-provisioned row |
| +(`reconcile.go:300-301`) is never `foreign`. |
| ### 8.4 Status, through the API (codex R1-18) |
| `internal/status/snapshot.go` gains a per-route `layout` field with one |
| of `flat`, `nested`, `fenced` (with the journal's phase and reason), |
| -`custom`, `foreign` (with both values), `external`, and a box-level |
| +`foreign` (with both values), `external`, and a box-level |
| `layout_mode` (`flat`, `nested`, or `none` before any intent). `carlos |
| status`, `carlos instances --layout` and the console's instance page |
| render them; a box that predates the field shows `unknown (box predates |
| @@ -1431,25 +1500,29 @@ verdict line: |
| dropped retries and times out rather than returning `EPERM` |
| (`tcp_connect`, `net/ipv4/tcp_output.c`). So the probe sends a UDP |
| datagram, where the filter's verdict comes straight back from |
| - `sendmsg`: `sendto(169.254.169.254:80)` must fail with `EPERM`, and |
| - `sendto([fd00:ec2::254]:80)` must fail with `EPERM` **or**, if the |
| - host has no IPv6 route at all (the control service reads `ip -6 route |
| - show default` and passes the answer in as the probe's environment), |
| - with `ENETUNREACH`, which is then reported as `v6: no route, deny not |
| - exercised` rather than `enforced`. As a control, `sendto(127.0.0.1:9)` |
| - must succeed (the network stack is live and the filter, not the |
| - stack, said no). A 2s TCP `connect()` to the IPv4 address must not |
| - succeed. Any success on a metadata address, or any errno other than |
| - those named, is `not enforced`. |
| + `sendmsg`: `sendto(169.254.169.254:80)` must fail with `EPERM`; |
| + `sendto([fd00:ec2::254]:80)` must fail with `EPERM` (`v6: enforced`) |
| + or with `ENETUNREACH` (`v6: unverified, no route to the address`): |
| + the kernel's own answer for that exact destination, so no route query |
| + is needed and none is made (codex R4-4; the service's |
| + `RestrictAddressFamilies=AF_UNIX` stands). As a control, |
| + `sendto(127.0.0.1:9)` must succeed (the network stack is live and the |
| + filter, not the stack, said no). A 2s TCP `connect()` to the IPv4 |
| + address must not succeed. Any success on a metadata address, or any |
| + errno other than those named, is `not enforced`. |
| The service records the verdict; `GET /ready` returns it; the agent |
| refuses every nested wake with the verdict's failing line until it is |
| -204. The probe cannot pass while an instance would not be isolated, |
| -because it runs under the same unit text (a test asserts the probe's |
| -namespace block equals the templates'), and it fails only on a line |
| -that names the property that is missing. It can fail while instances |
| -would be isolated only on a box with no IPv6 route whose operator has |
| -somehow made `ENETUNREACH` not the answer, which the verdict line names. |
| +204. `v6: unverified` does not block readiness on its own, because the |
| +boxes have no IPv6 route to that address today and a box with no route |
| +cannot reach it; it is **bounded and watched**: the probe re-runs every |
| +five minutes and on `daemon-reload`, the verdict is part of the status |
| +snapshot (§8.4), and the moment a v6 route appears and the answer is not |
| +`EPERM` the verdict flips to `not enforced` and nested wakes stop |
| +(codex R2-14 disposition). The probe cannot pass while an instance |
| +would not be isolated, because it runs under the same unit text (a test |
| +asserts the probe's namespace block equals the templates'), and it |
| +fails only on a line that names the property that is missing. |
| ### 8.6 Rollout order |
| @@ -1509,8 +1582,9 @@ R3-1, R3-6: |
| (`DefaultSocket`, `DefaultDBPath`, flat in this release), plus |
| `InstanceDir`, `InstanceRunDir`, `NestedDBPath`, `NestedSocket`, |
| `LogSocket` |
| -- `internal/activator/backend_exec.go:160-162` `defaultDBPath` (deleted); `:350, 507, 579, 607, 786, 790` (`<host>.env`, `<host>.config.env`); `:865-868` (`<host>-sidecar.env`); `:744-750` (socket normalisation, unchanged); every nested read through `instancefs`; the classification of §8.1; the peer-uid check on the health and control dials (§5.4) |
| -- `internal/edge/edge.go:2000-2014` (`unixProxy`: the peer-uid check on every dial, §5.4) |
| +- `internal/activator/backend_exec.go:160-162` `defaultDBPath` (deleted); `:350, 507, 579, 607, 786, 790` (`<host>.env`, `<host>.config.env`); `:865-868` (`<host>-sidecar.env`); `:744-750` (socket normalisation, unchanged); `:273, 1041-1057` (quarantine and artifact paths, the migration's source contract); every nested read through `instancefs`; the classification of §8.1; the path and `getpeername` checks on the health and control dials (§5.4) |
| +- `internal/edge/edge.go:2000-2014` (`unixProxy`: the path and `getpeername` checks on every dial, §5.4) |
| +- the layout pass's raw-directory renames (`/data/.instances`, §3.2): the one caller, pinned by a grep test |
| - `internal/appconfig/syncexec.go:389-395, 465, 872, 921-926` (nested routes into the directory; flat and addr routes flat; `O_EXCL` temp); `:977-1024` `reapConfigEnv` walks both |
| - `internal/schedule/runner.go:461` and `internal/host/schedule_wiring.go:163` (admin token path, by classification) |
| - `internal/host/movespass.go:285-305` — rebuilds `<DataDir>/<host>.db` from the record; reads `rt.DBPath` from the row instead, and refuses a `fenced` host |
| @@ -1567,18 +1641,22 @@ Unit level, all runnable in CI (no systemd needed): |
| `systemd-escape` fixtures. |
| - `instancefs`: refuses a symlink at every component, refuses `..`, |
| `O_EXCL` temp plus rename, the mountinfo check for all three mounts. |
| -- `internal/edge` and `internal/activator` dials: a listener whose peer |
| - is uid 0 is refused before a byte is sent; a `carlos` or DynamicUser |
| - peer is accepted. |
| +- `internal/edge` and `internal/activator` dials, with real socket |
| + pairs: a path outside `/run/carlos/` is refused before `connect()`; a |
| + symlink under `/run/carlos` to another listener yields a `getpeername` |
| + mismatch and is closed before a byte is sent; a listener created by |
| + another process and passed over (the `carlos-app@.socket` shape) is |
| + accepted when its bound path is the one dialled. |
| - `instance-control`: a connection whose peer pid is not the edge's |
| `MainPID`, or whose uid is not `carlos`, is closed without a response; |
| every 400 (bad host, bad role, bad limit); the unit and slice names it |
| builds for a host with a dash; `set-property` (three properties) → |
| `start` ordering with no `reset-failed`; `/reset` tolerating "not |
| - loaded"; `/seed` returning the show fields when loaded and an empty id |
| - when not; `/ready` from the probe verdict; with a fake `systemctl` |
| - runner and a fake peer. |
| -- `internal/activator`: classification of the five row shapes; |
| + loaded"; `/seed` starting `--no-block`, reading the invocation id |
| + while `activating`, waiting for terminal state plus empty cgroup, and |
| + returning `unknown` when the unit unloaded first; `/ready` from the |
| + probe verdict; with a fake `systemctl` runner and a fake peer. |
| +- `internal/activator`: classification of the four row shapes; |
| `prepare` mints the token for seed and run, writes `launch.<role>.json` |
| with the deduplicated env and the exact argv (the existing |
| env-composition tests move their assertion to the effective |
| @@ -1609,15 +1687,22 @@ Unit level, all runnable in CI (no systemd needed): |
| logged, line cap, EOF ends collection without marking exit. |
| - Layout pass: eligibility by the activator's predicate (flagged only; |
| external, tunnel, unit-backed untouched); convergence on every serial |
| - move; a later-flagged row migrating on the next pass; `custom` rows |
| - migrated from their actual paths; `foreign` rows reported; quiesce |
| + move; a later-flagged row migrating on the next pass; `foreign` rows |
| + (a custom basename, a subdirectory, a path outside the trees, a row |
| + pointing at the console database) reported and never moved; quiesce |
| before plan; the ownership preflight for `x`/`x.config` in both |
| directions; DB destination collision refused, env destination moved |
| - aside; the journal's phases and every crash boundary (before files, |
| + aside; the rename performed through the raw `.instances` directory |
| + fds and never through the bind mount (a test with a real bind mount |
| + where `EXDEV` would otherwise fire, skipped where the CI host cannot |
| + mount); the journal's phases and every crash boundary (before files, |
| mid-files, after files, after CAS, before journal removal) recovered |
| - exactly, with absent optional artifacts; a journal whose paths or mode |
| - do not match the recomputed plan and the fleet's intent refused; a CAS |
| - conflict keeps the fence; a second clean start does nothing; every |
| + exactly, with absent optional artifacts, with the row at either |
| + endpoint; a journal whose `to` is not the host's derived destination |
| + or whose `from` is not the host's flat paths refused; a journal |
| + completed to its own endpoint and the host then converged to a changed |
| + intent before release; a CAS conflict keeps the fence; a second clean |
| + start does nothing; every |
| fenced consumer (`Start`, `Seed`, `Restore`, moves pass, `SyncExec`, |
| litestream generator) refuses a fenced host; a partial rename followed |
| by a `MoveCutting` pass does not complete the flip; revert restores the |
| @@ -1751,7 +1836,7 @@ rollback runs the old binary). |
| R1-15 no `PrivatePIDs=` fallback; behavioural gate and probe (§8.5); |
| R1-16 env deduplication, effective-value test (§6.2); |
| R1-17 nested glob is discovery, not reporting (§9); |
| - R1-18 `layout` status through the API and CLI; `custom` rows migrated through the verb; `docs/site/cli.md` (§8.3, §8.4); |
| + R1-18 `layout` status through the API and CLI; `docs/site/cli.md`; the box-local repair of a `foreign` row accepted as the residual, with the reason (§8.3, §8.4); |
| R1-19 `UnitBackend` claim removed (§1.4, §11). |
| - **Round 2** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R2.md`, 14 new |
| findings, verdict request changes). All accepted: |
| @@ -1771,10 +1856,21 @@ rollback runs the old binary). |
| R2-14 probe distinguishes enforcement from unreachability (§8.5, reworked by R3-4). |
| - **Round 3** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R3.md`, 7 new |
| findings, verdict request changes). All accepted: |
| - R3-1 no token; the control service authenticates the edge's `MainPID`; the edge refuses root peers; `/run/carlos/logs` on a `nosymfollow` mount; journals checked against the recomputed plan and the fleet's intent (§3.2, §3.3, §5.4); |
| + R3-1 no token; the control service authenticates the edge's `MainPID`; every dial checks path and `getpeername` (the root-peer rule of revision 4 withdrawn by R4-1); `/run/carlos/logs` on a `nosymfollow` mount; journals checked against both endpoints (§3.2, §3.3, §5.4); |
| R3-2 exit record from `ExecStopPost=` without `+`, advisory only, in the run directory (§4.1, §6.5); |
| R3-3 no manual `memory.oom.group`; per-service families, difference recorded (§4.3); |
| R3-4 UDP `EPERM` probe with a loopback control and a no-route rule for v6 (§8.5); |
| R3-5 150s seed deadline (§5.3); |
| R3-6 nothing minted nested in this release; unflagged routes flat by contract (§3.1, §8.1, §8.6); |
| R3-7 the record lives where the agent can delete it (§6.5). |
| +- **Round 4** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R4.md`, 4 new |
| + findings plus partials, verdict request changes). All accepted: |
| + R4-1 root-peer rule withdrawn; path allowlist before the dial and `getpeername` equality after it (§5.4, §6.1); |
| + R4-2 `/data/.instances` bound onto `/data/instances`; the pass renames on one mount through raw directory fds (§3.1, §3.2); |
| + R4-3 sources follow each file's existing contract; only host-named files at the platform's paths move; everything else is `foreign` (§8.2, §8.3); |
| + R4-4 no route query; the v6 answer comes from `sendto` itself; the probe re-runs and the verdict is watched (§8.5); |
| + R2-4 `/seed` correlates by `--no-block` then `InvocationID`; a seed record may decide a seed's outcome because it can deceive only its author (§5.3, §6.5); |
| + R2-5 a foreign invocation is stopped and `done` waits for the cgroup (§6.5); |
| + R2-7 journals validated against both endpoints and completed to their own end before convergence (§8.2); |
| + R2-14 `v6: unverified` bounded by the five-minute re-run and reported in status (§8.5); |
| + R1-18 the `foreign` residual accepted with its reason (§8.3). |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R4.md b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R4.md| new file mode 100644 |
| index 000000000..762778bf7 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R4.md |
| @@ -0,0 +1,59 @@ |
| +| Prior finding | Disposition at `b6a35685` | |
| +|---|---| |
| +| R3-1 | **Resolved for the reported token and root-stdout attacks.** Process authentication and the protected log mount address them. The replacement dial restriction introduces R4-1 below. | |
| +| R3-2 | **Resolved.** `ExecStopPost=` now writes inside its actual namespace, to the instance’s run directory. | |
| +| R3-3 | **Resolved.** The unsupported slice write is removed; per-service OOM families are an explicit design decision. | |
| +| R3-4 | **Resolved for the TCP false-negative defect.** UDP observes the packet-filter error directly. The remaining IPv6 evidence gap is under R2-14; the new route-query defect is R4-4. | |
| +| R3-5 | **Resolved.** The seed request has a 150-second deadline. | |
| +| R3-6 | **Resolved.** Both minting paths retain flat defaults; externally supervised routes retain their existing contract. | |
| +| R3-7 | **Resolved.** The agent can remove records from their new directory. | |
| +| R2-4 | **Partially resolved.** Unloaded-unit termination is covered, but `/seed` still obtains identity after completion and can return an empty ID. Its fallback consumes an exit record that §6.5 expressly limits to event wording. The seed’s correlated completion result remains inconsistent between [§5.3](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:787) and [§6.5](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1053). | |
| +| R2-5 | **Partially resolved.** Ordinary stops now retain the lease on uncertainty. However, the [foreign-invocation branch](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1087) declares completion before the replacement’s cgroup is empty. Separate “replacement detected” from `done`; termination must remain unproven until that writer stops. | |
| +| R2-7 | **Regressed to partially resolved.** The new [recovery precheck](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1347) recomputes `from` from the current row before recognizing a committed CAS. After CAS, that row already names `to`, so validation rejects the legitimate journal. Changing fleet intent to `flat` likewise rejects an unfinished `nested` transaction. Validate both endpoint states and distinguish transaction intent from subsequently requested mode. | |
| +| R2-9 | **Resolved for the reported upgrade and destination-collision defects.** Flat minting protects the first upgrade; the explicit revert order and env-aside rule cover the described downgrade recovery. The new migration failures are identified separately. | |
| +| R2-14 | **Partially resolved.** IPv4 enforcement is tested, but [§8.5](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1434) permits readiness with IPv6 denial unexercised. Readiness is not invalidated when routing changes. Preserve unavailable evidence as unverified, or bound and monitor the no-route exception. | |
| +| R1-4 | **Partially resolved.** EOF and mutex defects are resolved; the completion exception remains under R2-5. | |
| +| R1-5 | **Partially resolved.** Preparation, execution budget, cancellation and stop-before-cleanup are specified. The seed completion-result inconsistency remains under R2-4. | |
| +| R1-8 | **Resolved.** Shared tier limits are restored; the changed family OOM behavior is explicitly bounded and documented. | |
| +| R1-12 | **Partially resolved.** Consumer fences are specified; recovery regresses as described under R2-7. | |
| +| R1-13 | **Resolved for the reported missing reverse mechanism and database-history selection.** Explicit reversal and collision refusal replace those defects. | |
| +| R1-15 | **Partially resolved.** The unsafe PID-namespace fallback remains removed. The remaining readiness issues are R2-14 and R4-4. | |
| +| R1-18 | **Partially resolved.** Reporting and custom-row migration are remote. [Foreign-row repair](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1390) still explicitly requires a box-local command. | |
| + |
| +**R4-1 — P1 — §§5.4, 6.1, 9: Retain the authenticated control service, but replace the blanket root-peer rejection.** |
| + |
| +The new rule rejects every application connection whose `SO_PEERCRED` uid is zero. Existing `carlos-app@.socket` listeners are created by PID 1 and passed to DynamicUser services. Their peer credentials remain the credentials recorded at `listen()`: root. `SocketUser=carlos` changes the socket file’s ownership, not those credentials. Consequently, the proposed check rejects legitimate unit-backed application traffic and health checks. |
| + |
| +Evidence: [the new restriction](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:853), [existing socket-activation contract](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/host/units/carlos-app@.socket:1), [Linux `SO_PEERCRED` semantics](https://man7.org/linux/man-pages/man7/unix.7.html), [systemd socket ownership semantics](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.socket.xml). |
| + |
| +**Correction:** keep process authentication and define an anti-proxy check that distinguishes the control endpoint from legitimate systemd-created application listeners. Do not substitute a general root-peer exception. Verify both permitted socket activation and refused control-channel proxying with real sockets. |
| + |
| +**R4-2 — P1 — §§3.2, 8.2: The required bind mount prevents migration by rename.** |
| + |
| +`/data/instances` is a bind mount before the agent starts. Moving `/data/H.db` to `/data/instances/H/H.db` therefore crosses mount points. Linux rejects that rename with `EXDEV`, even though both paths refer to the same underlying filesystem. Reverse migration fails for the same reason. |
| + |
| +The first database rename consequently fails after the journal has fenced the host. Repeating the prescribed recovery cannot complete it. |
| + |
| +Evidence: [the bind mount](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:370), [the migration’s `os.Rename` requirement](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1336), [Linux `rename(2)` and `EXDEV`](https://man7.org/linux/man-pages/man2/rename.2.html). |
| + |
| +**Correction:** specify a protected migration view in which both endpoints share one mount, preserving the approved rename approach and ordinary consumers’ `nosymfollow` protection. Verify both directions with the actual mounts installed. |
| + |
| +**R4-3 — P2 — §§8.2–8.3: Custom-path migration looks for environment files in the wrong directory.** |
| + |
| +For a custom database such as `/data/sub/store.db`, step 3 takes environment artifacts from its source directory. The existing backend instead reads `/data/<host>.env`, `/data/<host>.config.env` and `/data/<host>-sidecar.env`, independently of `DBPath`. |
| + |
| +The pass therefore records those artifacts as absent, moves the database, and starts the nested instance without its existing overrides or sidecar configuration. Token preparation mints a replacement token. The quarantine source is also wrong for a custom basename: existing code uses `dbPath + ".corrupt"`. |
| + |
| +Evidence: [migration source derivation](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1297), [environment composition](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/backend_exec.go:785), [sidecar path](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/backend_exec.go:865), [quarantine path](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/backend_exec.go:273). |
| + |
| +**Correction:** derive each source from its existing contract: database-relative WAL, SHM, shadow and quarantine; `DataDir`-relative environment files. Verify a custom database with both a subdirectory and a different basename. |
| + |
| +**R4-4 — P2 — §§5.2, 8.5: The control service forbids the route query its probe requires.** |
| + |
| +The control service must run `ip -6 route show default`, but its unit permits only `AF_UNIX`. The `ip` command opens an `AF_NETLINK` socket and inherits the service’s restriction. It cannot obtain the routing evidence specified by the readiness protocol. |
| + |
| +Evidence: [service restriction](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:763), [required query](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1435), [iproute2 socket creation](https://raw.githubusercontent.com/iproute2/iproute2/main/lib/libnetlink.c), [systemd address-family restrictions](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.exec.xml). |
| + |
| +**Correction:** permit the required route-query socket in the control service or assign the query to an appropriately permitted helper. Treat query failure separately from an empty result. An empty default-route list also does not establish the absence of more-specific IPv6 routes. |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |