amadan
spec: fleet-internal engines rev 4 (Astra R3: 2 P1, 1 P2, all accepted)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+104
−10
docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md+62 −10docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R3.md+42 −0
CI cancelled — superseded by a newer push — run details
CI log
=== gate === cd launchctx && go vet ./... && go test ./... -count=1 ok amadan.net/carlos/platform.git/launchctx 0.011s ? amadan.net/carlos/platform.git/launchctx/controlname [no test files] ? amadan.net/carlos/platform.git/launchctx/wireid [no test files] go vet ./... gofmt -l .: clean go test ./... -count=1 -timeout 30m amadan: job cancelled — a newer push superseded it
diff --git a/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md b/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md| index 794a21432..84e01a7e8 100644 |
| --- a/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md |
| +++ b/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md |
| @@ -1,9 +1,17 @@ |
| # Fleet-internal engines: a doc engine nobody on the internet can call |
| **Date:** 2026-10-21 |
| -**Revision:** 3. |
| +**Revision:** 4. |
| **Discussion:** amadan carlos/platform #335. Related: #328 (per-app egress allow). |
| +- **Rev 4** answers Astra round 3 (`CODEX-FINDINGS-ENGINES-R3.md`, reject, |
| + two P1s and a P2, all accepted). The barrier's acknowledgement now also |
| + covers public requests admitted before the mark: the edge cancels them and |
| + waits for them to finish before it acknowledges (R3-1). Engine sockets |
| + open only on a box with no flat instance at all, because a flat tenant can |
| + write a nested sibling's files and run code inside its slice (R3-2). Every |
| + deploy target gets a watch ticket, not only declaring releases (R3-3). |
| + Marked **(codex R3-n)**. |
| - **Rev 3** answers Astra round 2 (`CODEX-FINDINGS-ENGINES-R2.md`, reject, |
| three P1s and two P2s, all accepted). The mark gains an "unclassified" |
| state and a serving barrier: set before the release switch, cleared after |
| @@ -177,11 +185,23 @@ and the edge serves an in-memory map refreshed on a 2 s registry poll |
| (`edge.go:2298`). So the order is explicit: |
| - **Becoming internal** (the incoming release declares `doc_engine`, the |
| - route is `0`): adoption writes `1`, then waits until the edge reports a |
| - loaded registry state that includes that write, then repoints and |
| - restarts. The edge publishes the registry change it last loaded |
| - (a counter in a file under `/run/carlos` that `Reload` writes after it |
| - swaps the map in; a failed `Reload` does not advance it). The wait is |
| + route is `0`): adoption writes `1`, then waits for the edge's |
| + acknowledgement, then repoints and restarts. The edge publishes the |
| + registry change it has **fenced** (a counter in a file under |
| + `/run/carlos`), and it advances that counter only after both: |
| + 1. `Reload` has swapped in a map carrying the mark (a failed `Reload` |
| + advances nothing); and |
| + 2. **every request admitted to that route as a non-engine call before the |
| + swap has finished (codex R3-1).** Each such request holds a reference |
| + on the route's public-admission epoch from the moment it passes the |
| + internal check until its response ends, including while it waits in |
| + the activator's queue for a wake (`activator.go:1554`, `:5404`). Loading |
| + a `0`→`1` change bumps the epoch and cancels the contexts of every |
| + request holding the old one, which also drops it from the activator's |
| + queue; the counter advances when the last of them has released. A |
| + request admitted after the swap sees `1` and is refused. |
| + |
| + The wait is |
| bounded (30 s); on timeout adoption does not repoint this pass, the mark |
| stays `1`, and the next pass retries. The old, non-engine release is |
| refused publicly for that interval, which costs availability, never |
| @@ -308,7 +328,10 @@ instance: `/run/carlos/instances/<iid>/engines.sock` (at most 75 bytes). |
| route leaves the box (removal, a move's commit, a reset). It is not tied |
| to a generation and never closed by one. It exists whether or not the |
| app holds a grant, so a later grant needs no restart. Answering on a |
| - sleeping instance's socket does not wake the instance. |
| + sleeping instance's socket does not wake the instance. All of this holds |
| + only on a box with no flat instance (§6.2); elsewhere no engine socket is |
| + open, and `CARLOS_ENGINES_SOCKET` still names the path, so an app finds |
| + the socket missing rather than the variable. |
| - **Mode 0666**, because the connecting process's identity is checked |
| below, not by file permission. |
| - **Who is calling:** on every accepted connection, before a byte is read, |
| @@ -419,9 +442,11 @@ The hourly capability pass on each box logs once per pass: |
| ### 5.8 Watching an engine deploy (codex R2-4) |
| `carlos deploy` verifies a release by polling its public URL |
| -(`deploy.go:1426`, `:1536`), which an internal route now refuses. For a |
| -target whose release declares `doc_engine`, the watch carries a **watch |
| -ticket** instead: |
| +(`deploy.go:1426`, `:1536`), which an internal route now refuses. Whether a |
| +route is internal is box-local (a grant can make it so whatever the release |
| +declares), so **every deploy target's watch carries a watch ticket (codex |
| +R3-3)**. The edge honours it only on an internal route and strips it |
| +everywhere else, where the watch proceeds exactly as today: |
| - The console mints it on the deploy request it already authorizes: signed |
| with the root release key under its own domain (`carlos watch v1\n`), |
| @@ -453,6 +478,22 @@ and not solved. |
| ### 6.2 Flat layout |
| +**Engine sockets need an all-nested box (codex R3-2).** A flat tenant runs |
| +as uid carlos with write access to its nested siblings' directories |
| +(`layout/preflight.go:181`), including the instance's own environment file |
| +the launch reads (`activator/backend_exec.go:2701`). It can plant a library |
| +and an `LD_PRELOAD` there and so run code inside a granted sibling's slice, |
| +which the cgroup check then accepts as that sibling. So the edge opens |
| +engine sockets only while the box's layout intent is nested and the layout |
| +pass classifies **no** instance route on the box as flat (`layout/pass.go` |
| +`Classify`). The moment a route classifies flat (a hand-added row, a box |
| +that is not ready, a `layout revert`, `CARLOS_LAYOUT_DEFAULT=flat`), the edge |
| +closes every engine socket on the box and logs why; it reopens them once the |
| +condition holds again. Residual, stated: a nested instance's files on a box |
| +that once ran flat tenants are only as trustworthy as that period, which is |
| +true of isolation as a whole and not specific to engines; an operator who |
| +doubts a box's past rebuilds its instances from the bucket. |
| + |
| **(codex R2-3)** A flat instance cannot call an engine. It has no engine |
| socket, it cannot use a nested sibling's (its process is not in that |
| sibling's slice), and the door refuses engine calls from uid carlos. Flat |
| @@ -533,6 +574,13 @@ process, real unix sockets and a real cgroup check where the kernel allows |
| - A deploy watch with a valid ticket reads the version on `/` and the probe |
| path; the ticket on a POST, another path, an expired ticket or one for |
| another host gets the internal refusal. |
| +- A public request admitted before a `0`→`1` mark and held (mid-proxy, and |
| + queued behind a wake) is cancelled before the edge acknowledges, and never |
| + reaches the declaring release. |
| +- A box with one flat route opens no engine sockets; adding a flat route to |
| + an armed box closes them all; removing it reopens them. |
| +- A watch ticket on a public route is stripped and the watch behaves as |
| + today; on a grant-only internal route it reads the version. |
| - A socket call from a process in the instance's slice reaches the engine on |
| another edge; from a process outside the slice (a flat child, a sibling |
| slice) the connection is closed unread. |
| @@ -578,6 +626,7 @@ it, not only over a private network. |
| - Tunnel-homed engines are refused (502), not supported. |
| - Flat instances cannot call engines at all (§6.2); host-app processes |
| under their own uid use the door, enabled by the operator. |
| +- Engine sockets only on all-nested boxes, closed while any route is flat. |
| - Unclassified routes are refused publicly (fail closed) even though that |
| can make a route with no readable manifest unreachable while the bucket |
| is down. |
| @@ -607,3 +656,6 @@ it, not only over a private network. |
| | R2-3 flat callers borrow a door key | Accepted: door engine calls need a non-carlos uid; flat cannot call (§5.4, §6.2) | |
| | R2-4 deploy watch cannot verify | Accepted: watch ticket (§5.8) | |
| | R2-5 :80 on non-home boxes; unknownHost redirects | Accepted: plain 404 refusal; no-redirect scoped to the home box (§5.1) | |
| +| R3-1 requests admitted before the mark | Accepted: the acknowledgement waits for cancelled pre-mark requests to finish (§5.1) | |
| +| R3-2 flat tenant injects code into a nested caller | Accepted: engine sockets only on all-nested boxes; flat-era residual stated (§6.2) | |
| +| R3-3 grant-only routes lack a watch ticket | Accepted: every deploy target carries one (§5.8) | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R3.md b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R3.md| new file mode 100644 |
| index 000000000..f9e14d653 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R3.md |
| @@ -0,0 +1,42 @@ |
| +| Previous finding | Round 3 assessment | |
| +|---|---| |
| +| R1-1: flat tenant borrows a nested socket | Direct connection blocked by §5.4. The separate process-injection path below remains. | |
| +| R1-2: aliases and path routes remain public | Fixed at spec level by the final-route check (§5.1). | |
| +| R1-3: new box starts public | Fixed by classification before serving and refusal of `NULL` (§5.1). | |
| +| R1-4: revoked grants return after restart | Fixed for retained local state; fresh-box replay remains explicitly accepted (§5.3). | |
| +| R1-5: door exceptions fail across routing | Resolved by removing the owner exception and defining the identity transition (§5.4). | |
| +| R1-6: socket lifecycle conflicts | Fixed by instance-level listener ownership (§5.4). | |
| +| R1-7: transport and body limits | Resolved at spec level (§5.5). | |
| +| R2-1: stamp follows serving | Partly fixed: reload acknowledgement covers new lookups, but not requests retaining an earlier upstream (§5.1; finding 1 below). | |
| +| R2-2: upgrade serves unclassified engines | Fixed by classification before listeners and fail-closed handling (§5.1). | |
| +| R2-3: flat callers borrow door credentials | Direct door attack fixed by the UID check (§§5.4, 6.2). The broader identity guarantee still fails through finding 2. | |
| +| R2-4: deployment verification fails | Partly fixed: tickets cover declaring releases, but omit routes internal solely through their grant (§5.8; finding 3). | |
| +| R2-5: port-80 refusal cannot work remotely | Resolved by the narrowed contract and explicit non-redirecting refusal (§5.1). | |
| + |
| +Reviewed `295eb39f` against locally available amadan `origin/main` at `f54aa2fc`. The implementation files cited below match that revision. No files changed. |
| + |
| +1. **P1 — Reload acknowledgement does not fence requests already admitted (§§5.1, 6.3).** |
| + |
| + A public request resolves a route while its mark is `0` and passes the proposed check. Pause it before upstream dispatch. Adoption writes `1`, receives the reload acknowledgement, and starts the declaring release. Resume the request: it still holds the previous upstream and can reach the new engine. |
| + |
| + Route lookup returns an upstream value ([edge.go:1202](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:1202)); reload replaces the map without invalidating previously selected values ([edge.go:993](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:993)). Requests subsequently dispatch through their retained proxy ([edge.go:1775](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:1775)). This can also involve an actual wait: the activator queues requests behind a stopping instance, wakes it again, and then invokes the supplied proxy ([activator.go:1554](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/activator.go:1554), [activator.go:5404](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/activator.go:5404)). |
| + |
| + **Suggested fix:** Make the acknowledgement cover a per-route admission fence and the draining or cancellation of previously admitted public requests before activation. Queued requests must not cross the release switch using their previous admission. A second unsynchronised check merely moves the race. |
| + |
| +2. **P1 — A flat tenant can inject code into a granted nested caller (§§5.4, 6.1–6.2).** |
| + |
| + Put ungranted flat app A beside granted nested app B, whose executable is dynamically linked. A writes a library into B’s data directory and adds `LD_PRELOAD` pointing to it in B’s instance environment file. When B next starts, the library executes inside B’s legitimate slice and connects to B’s engine socket. The cgroup check authenticates B, and both grant checks pass. Neither the direct-socket refusal nor the door UID check intervenes. |
| + |
| + The existing layout code explicitly identifies flat tenants’ same-UID write access to sibling directories ([preflight.go:181](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/layout/preflight.go:181)). Nested launches read their instance environment files ([backend_exec.go:2701](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/backend_exec.go:2701)); `childEnv` passes their supplied variables through ([backend_exec.go:2817](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/backend_exec.go:2817)). The trampoline validates environment syntax and executes with that environment ([exec.go:116](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/instanceexec/exec.go:116)). The nested unit binds B’s data directory and runs in B’s slice ([carlos-instance@.service:33](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/units/carlos-instance@.service:33), [carlos-instance@.service:53](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/units/carlos-instance@.service:53)). |
| + |
| + **Suggested fix:** Enforce a box-wide prerequisite excluding untrusted flat processes before enabling engine caller identities, including later flat launches and reversions. Alternatively, isolate callers’ writable state from flat tenants. Filtering one loader variable would not establish that isolation. |
| + |
| +3. **P2 — Grant-only internal routes still cannot complete URL-based deployment verification (§§5.1, 5.8).** |
| + |
| + Give a route the `doc-engine` grant while its release does not declare `doc_engine`. Deploy another non-declaring release. Section 5.1 keeps the route internal because the grant remains, but §5.8 issues watch tickets only for declaring releases. The ordinary watch therefore receives the internal refusal even when the deployment is healthy. |
| + |
| + Capability grants are stored independently of release versions ([registry.go:1613](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/registry/registry.go:1613)). URL verification sends an ordinary GET ([deploy.go:1546](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/deploy.go:1546)) and requires a successful response ([deploy.go:1563](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/deploy.go:1563)). |
| + |
| + **Suggested fix:** Make watch-ticket availability cover every authorised deployment target that can be internal, including grant-only routes. Since classification is box-local, issuing narrowly scoped tickets for all authorised deploy targets avoids requiring the console to infer that classification. |
| + |
| +**Overall verdict: reject.** The remaining public-admission race and mixed-layout identity attack violate the stated anti-goals. |
| \ No newline at end of file |