amadan
spec: fleet-internal engines rev 5 (Astra R4: 2 P1, 1 P2, all accepted)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+125
−23
docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md+76 −23docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R4.md+49 −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.012s ? 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 84e01a7e8..c42c68cdd 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,16 @@ |
| # Fleet-internal engines: a doc engine nobody on the internet can call |
| **Date:** 2026-10-21 |
| -**Revision:** 4. |
| +**Revision:** 5. |
| **Discussion:** amadan carlos/platform #335. Related: #328 (per-app egress allow). |
| +- **Rev 5** answers Astra round 4 (`CODEX-FINDINGS-ENGINES-R4.md`, reject, |
| + two P1s and a P2, all accepted). "No flat route" becomes a positive, |
| + operator-armed box state that also excludes `foreign` instances and |
| + workers, and refuses unisolated launches while armed (R4-1). An engine |
| + call is dispatched only to the engine hostname's own route, never through |
| + a path map (R4-2). Watch tickets are renewed for as long as the watch runs |
| + (R4-3). Marked **(codex R4-n)**. |
| - **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 |
| @@ -329,7 +336,7 @@ instance: `/run/carlos/instances/<iid>/engines.sock` (at most 75 bytes). |
| 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. All of this holds |
| - only on a box with no flat instance (§6.2); elsewhere no engine socket is |
| + only on an armed box (§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 |
| @@ -389,8 +396,13 @@ way in, so only an edge can speak it. |
| **On the engine box.** An engine-marked request reaches a route only if the |
| route is internal, the mark's engine names the request's hostname in the |
| -grant table, and the table grants that engine to the mark's app. Otherwise |
| -the internal refusal (§5.1). Then: |
| +grant table, the table grants that engine to the mark's app, **and the |
| +route is the engine hostname's own route (codex R4-2)**. An engine call is |
| +resolved by exact hostname only, never through a path map or a wildcard |
| +(`edge.go:1364`; path targets may cross apps within an account, |
| +`domains/aliases.go:395`), so a grant for one engine can never dispatch to |
| +another. An alias of the engine's hostname resolves to the same route and |
| +is fine. Otherwise the internal refusal (§5.1). Then: |
| - the per-app cap (§5.5); |
| - the import gate, unchanged; |
| @@ -454,6 +466,12 @@ everywhere else, where the watch proceeds exactly as today: |
| It is returned to the CLI with the promote response. |
| - In bucket mode, where no console is involved, the CLI signs the ticket |
| itself with the root release key it already holds to sign the promote. |
| +- **Renewal (codex R4-3):** the CLI asks for a fresh ticket for the same |
| + hostname and version every 4 minutes for as long as the watch runs |
| + (`--timeout` may be longer than one ticket's life, `deploy.go:75`). The |
| + console re-authorizes the request with the same deploy credential and |
| + refuses a hostname or version the deploy did not name; in bucket mode the |
| + CLI re-signs. |
| - The CLI sends it as `X-Carlos-Watch-Ticket` on each poll. The home box's |
| edge admits a request carrying a valid ticket to the internal route only |
| for `GET` or `HEAD` with no body, on `/` or the release's declared probe |
| @@ -478,21 +496,41 @@ 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. |
| +**Engine sockets need an armed box (codex R3-2, R4-1).** Any tenant code |
| +running as uid carlos outside an instance slice can write its nested |
| +siblings' directories (`layout/preflight.go:181`), including the |
| +environment file a nested launch reads (`activator/backend_exec.go:2701`), |
| +plant a library and an `LD_PRELOAD`, and so run code inside a granted |
| +sibling's slice, which the cgroup check then accepts as that sibling. Three |
| +launch paths run tenant code that way today: a `flat` instance, a `foreign` |
| +one (`activator/layout.go:103`; both go through the exec-child path, |
| +`backend_exec.go:1826`), and an app's worker, which spawns into |
| +`carlos-exec@<host>` whatever its layout (`StartWorker`, `opset.go`). The |
| +predicate is therefore positive: **the only tenant code on the box runs in |
| +instance slices or as unit-backed DynamicUser services** (which cannot write |
| +carlos-owned directories). |
| + |
| +- **Arming is an operator act on the box:** `carlos engines arm`. It |
| + refuses unless the box's layout intent is nested, every `instance` route |
| + classifies `nested`, no route on the box spawns workers, and every |
| + `carlos-exec@` cgroup on the box is empty. It records the armed state in |
| + the box registry. The edge opens engine sockets only on an armed box. |
| +- **While armed, the activator refuses every unisolated launch**: a flat or |
| + foreign start and a worker spawn are refused with one log line naming the |
| + route and `carlos engines disarm`. The check sits in the launch path, so |
| + no unisolated process can start on an armed box, rather than being |
| + noticed afterwards. Provisioning a route that would classify flat or |
| + foreign on an armed box leaves it unlaunched until the box is disarmed. |
| +- **Disarming** (`carlos engines disarm`) closes every engine socket first, |
| + then clears the state; launches follow. Re-arming is the same operator act |
| + as arming, with the same checks. |
| +- **Residual, stated:** arming vouches for the present, not the past. A |
| + nested instance's files on a box that ran unisolated tenants before it was |
| + armed are only as trustworthy as that period, which is true of isolation |
| + as a whole. `carlos engines arm` says so when it succeeds; an operator who |
| + doubts a box's past rebuilds its instances from the bucket first. |
| +- **Consequence, stated:** an app that uses workers cannot run on an armed |
| + box until workers move into instance slices. That is a separate change. |
| **(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 |
| @@ -535,6 +573,10 @@ so a revoke is in force once either has read it. |
| - **Boxes, then the console**, in the usual order: dev boxes, dev console, |
| check, flagship boxes, flagship console. Engine calls need the calling |
| box, the home box and the console all on this build. |
| +- **Arm the calling boxes.** On each box whose instances will call an |
| + engine, the operator runs `carlos engines arm` once the box is fully |
| + nested and runs no workers. The survey lists, per box, what blocks |
| + arming. |
| - **Then names and grants.** With no `engines.json` the grant table is empty |
| and every engine socket answers 404; nothing else changes. `carlos engines |
| add` and `grant` follow the roll, and callers switch to the socket. |
| @@ -577,8 +619,15 @@ process, real unix sockets and a real cgroup check where the kernel allows |
| - 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. |
| +- `carlos engines arm` refuses with a flat route, a foreign route, a route |
| + with workers, or a non-empty `carlos-exec@` cgroup on the box; on an |
| + armed box a flat start, a foreign start and a worker spawn are refused |
| + before any process starts; `disarm` closes every engine socket before |
| + launches resume. |
| +- An engine call with `Host: A` whose path maps to engine B's route is |
| + refused, though the caller holds A's grant. |
| +- A watch with a 10-minute timeout whose target turns healthy at minute 6 |
| + succeeds on a renewed ticket. |
| - 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 |
| @@ -626,7 +675,8 @@ 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. |
| +- Engine sockets only on boxes an operator armed; an armed box refuses |
| + flat, foreign and worker launches rather than closing sockets afterwards. |
| - Unclassified routes are refused publicly (fail closed) even though that |
| can make a route with no readable manifest unreachable while the bucket |
| is down. |
| @@ -657,5 +707,8 @@ it, not only over a private network. |
| | 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-2 flat tenant injects code into a nested caller | Accepted, then widened by R4-1: armed boxes (§6.2) | |
| | R3-3 grant-only routes lack a watch ticket | Accepted: every deploy target carries one (§5.8) | |
| +| R4-1 foreign instances and workers are unisolated too | Accepted: positive armed state, unisolated launches refused while armed (§6.2) | |
| +| R4-2 a path map widens a grant to another engine | Accepted: engine calls resolve by exact hostname to the engine's own route (§5.4) | |
| +| R4-3 watch tickets expire mid-watch | Accepted: renewal every 4 minutes (§5.8) | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R4.md b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R4.md| new file mode 100644 |
| index 000000000..19205091b |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R4.md |
| @@ -0,0 +1,49 @@ |
| +| Previous finding | Round 4 assessment | |
| +|---|---| |
| +| R1-1: flat tenant borrows a nested socket | Direct connection blocked by §5.4’s cgroup check. | |
| +| R1-2: aliases and path routes remain public | Fixed by §5.1’s final-route check. | |
| +| 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 | Fixed at spec level by the strengthened admission barrier (§5.1). | |
| +| R2-2: upgrade serves unclassified engines | Fixed by classification before listeners and refusal of unclassified routes (§5.1). | |
| +| R2-3: flat callers borrow door credentials | Direct door attack fixed by the UID restriction (§§5.4, 6.2). | |
| +| R2-4: deployment verification fails | Ticket coverage now includes every deploy target (§5.8). A separate expiry problem remains below. | |
| +| R2-5: port-80 refusal cannot work remotely | Resolved by the narrowed contract and explicit non-redirecting refusal (§5.1). | |
| +| R3-1: previously admitted requests cross the mark | Fixed at spec level: acknowledgement waits for cancellation and completion (§5.1). | |
| +| R3-2: flat tenant injects into a nested caller | **Partly fixed:** §6.2 excludes `flat`, but its specified predicate misses another unisolated execution class; finding 1 below. | |
| +| R3-3: grant-only routes lack watch tickets | Fixed: every deploy target receives a ticket (§5.8). | |
| + |
| +Reviewed spec `c0d2d531` against locally available amadan `origin/main` at `512baa59`. The implementation files cited below match that revision. No files changed. |
| + |
| +1. **P1 — The “all-nested” prerequisite permits unisolated `foreign` instances (§§5.4, 6.2).** |
| + |
| + Configure layout intent as nested, with granted nested instance B and ungranted instance A using custom database or socket paths. A classifies as `foreign`, so the prescribed “no instance route classifies flat” check succeeds and engine sockets open. A can modify B’s environment and plant a library. On B’s next launch, that code runs inside B’s legitimate slice and calls engines as B. |
| + |
| + `Classify` returns `foreign` for paths outside the two standard layouts ([layout.go:103](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/layout.go:103)). `Start` sends that class through the ordinary exec-child path ([backend_exec.go:1826](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/backend_exec.go:1826)), which inherits the edge’s `carlos` identity and writable `/data` access ([carlos-edge.service:28](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/units/carlos-edge.service:28), [backend_exec.go:2236](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/backend_exec.go:2236)). B’s launch reads its writable environment file ([backend_exec.go:2701](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/backend_exec.go:2701)). |
| + |
| + This is concurrent unisolated execution, not the stated residual from a box’s past. |
| + |
| + **Suggested fix:** Base eligibility on exclusion of every unisolated tenant execution path, including `LayoutForeign`. Require proof of nested isolation for relevant running or launchable instances instead of testing only for absence of `LayoutFlat`. |
| + |
| +2. **P1 — A grant for one engine authorizes a different engine through path routing (§§5.2, 5.4).** |
| + |
| + Put internal engines A and B in the same account on one box. Register both names, but grant caller C only A. Configure `/convert` on A’s hostname to target B’s route. C sends `POST /convert` through its socket with `Host: A`. |
| + |
| + The calling edge checks A’s grant and rewrites the hostname to A’s hostname. Path resolution selects B. Every specified receiving-side check still passes: B is internal, the mark’s engine A names the request hostname, and C has A’s grant. B receives the request despite C having no grant for B. |
| + |
| + Existing path reconciliation explicitly permits targets in another app within the same account ([aliases.go:395](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/domains/aliases.go:395)). The edge returns the selected target’s upstream ([edge.go:1364](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:1364)). Checking the requested hostname therefore does not bind authorization to the engine route actually dispatched. |
| + |
| + **Suggested fix:** Resolve the registered engine hostname to its primary route identity and require the final upstream to match that identity. Alternatively, bypass path routing for engine calls. Preserve ordinary aliases without allowing a path mapping to widen a grant. |
| + |
| +3. **P2 — Watch tickets expire before supported longer deployment watches finish (§5.8).** |
| + |
| + Run an internal-engine deployment with `--timeout 10m`. Adoption is delayed, and the target becomes healthy six minutes after promotion. Its ticket expired at five minutes. Every subsequent URL poll receives the internal refusal, so verification fails even though the deployment completed within the requested timeout. |
| + |
| + The CLI accepts a configurable watch timeout ([deploy.go:75](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/deploy.go:75)). URL watching uses that timeout as its deadline ([deploy.go:1471](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/deploy.go:1471)); the current deploy watcher retains this path for targets without rollout reports ([deploywatch.go:295](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/deploywatch.go:295)). Section 5.8 specifies one ticket returned with promotion and no renewal mechanism. |
| + |
| + **Suggested fix:** Provide authenticated ticket renewal for the same authorized hostname and version while the watch remains active, with equivalent re-signing in bucket mode. |
| + |
| +**Overall verdict: reject.** The isolation predicate and engine-target authorization still permit calls that the stated identity and grant guarantees forbid. |
| \ No newline at end of file |