carlos / platform Public

spec: fleet-internal engines rev 6 (Astra R5: accept with fixes, 3 P2 answered)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude agent, operated by paul@keymail.dev 3829dada50d201863eecdf263eddda360e6bcc00 parent ddad746
2 files changed, +93 −7
  • docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md +45 −7
  • docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R5.md +48 −0

CI cancelled — superseded by a newer push — run details

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 c42c68cdd..135b62e3a 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,14 @@
# Fleet-internal engines: a doc engine nobody on the internet can call
**Date:** 2026-10-21
-**Revision:** 5.
+**Revision:** 6.
**Discussion:** amadan carlos/platform #335. Related: #328 (per-app egress allow).
+- **Rev 6** answers Astra round 5 (`CODEX-FINDINGS-ENGINES-R5.md`, accept
+ with fixes, three P2s, all accepted). Platform-minted rows take their
+ execution owner's mark and barrier (R5-1). Arming judges exec-backed
+ routes by layout and admits unit-backed ones (R5-2). The watch ticket
+ signs the probe path the watcher uses (R5-3). Marked **(codex R5-n)**.
- **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
@@ -185,6 +190,18 @@ An `instance` route is classified from the manifest of its live release:
`1` if it declares `doc_engine`, `0` otherwise. The `doc-engine` grant also
sets `1`, whatever the manifest says. The edge treats `NULL` like `1`.
+**Platform-minted rows (codex R5-1).** A platform domain is its own
+registry row (`Platform: true`, `domains/reconcile.go:881`), copying the
+source's backend but no version, and adoption skips it
+(`release/adopt.go:1210`). Such a row never carries a mark of its own. Its
+**execution owner** is the non-platform `instance` row on the box with the
+same account, app and backend (`Socket`, or for a fleet-placed source the
+same `Region`); the edge resolves the owner at `Reload` and the row is
+internal exactly when its owner is. The admission epoch of §5.1's barrier
+is the owner's, so a minted row's in-flight requests are cancelled with the
+owner's. A minted row whose owner the edge cannot find is treated as `NULL`
+and refused, and logged by name.
+
**Set before, clear after: the serving barrier (codex R2-1).** Adoption
repoints the live symlink (`release/adopt.go:1751`), restarts
(`adopt.go:1831`) and records the version afterwards (`adopt.go:2051`),
@@ -462,10 +479,15 @@ 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`),
- bound to one hostname and one version, expiring 5 minutes after minting.
+ bound to one hostname, one version and **the probe path the watcher will
+ poll (codex R5-3)**, expiring 5 minutes after minting. The probe comes
+ from the same app setting the console already returns with the ship
+ response (`console/apicli.go:2114`, `:2285`; used at `deploy.go:404`);
+ no probe means `/` only.
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.
+ itself with the root release key it already holds to sign the promote,
+ over the probe path it is about to poll.
- **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
@@ -474,7 +496,7 @@ everywhere else, where the watch proceeds exactly as today:
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
+ for `GET` or `HEAD` with no body, on `/` or the ticket's signed probe
path, strips the header, and dispatches as usual (no cache, as the watch
already busts it). Anything else with a ticket gets the internal refusal.
- The ticket crosses a backhaul as a header and is verified only on the home
@@ -511,9 +533,15 @@ 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
+ refuses unless the box's layout intent is nested, every exec-backed
+ `instance` route classifies `nested`, no route on the box spawns workers,
+ and every `carlos-exec@` cgroup on the box is empty **(codex R5-2)**.
+ Unit-backed routes (`backing=unit`, `carlos-app@`, DynamicUser) are
+ admitted: their socket is `/run/carlos/apps/<host>.sock`, which
+ `Classify` reports as `foreign` (`activator/layout.go:103`), so they are
+ judged by backing, not layout. Platform-minted rows are judged through
+ their execution owner. An exec-backed route that classifies `foreign`
+ still blocks arming. 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
@@ -626,6 +654,13 @@ process, real unix sockets and a real cgroup check where the kernel allows
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 platform-minted hostname of an internal route is refused publicly and
+ admits engine calls exactly as the owner does; a minted hostname of a
+ public route keeps working across the upgrade.
+- `carlos engines arm` succeeds on a box with nested callers and a
+ unit-backed engine.
+- A watch with a probe of `/healthz` reads it with a ticket; the same
+ ticket on `/other` gets the internal refusal.
- 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
@@ -712,3 +747,6 @@ it, not only over a private network.
| 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) |
+| R5-1 platform-minted rows never classify | Accepted: execution owner's mark and epoch (§5.1) |
+| R5-2 arming rejects unit-backed routes | Accepted: exec-backed routes by layout, unit-backed by backing (§6.2) |
+| R5-3 no source for the probe path | Accepted: the ticket signs the watcher's probe path (§5.8) |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R5.md b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R5.md
new file mode 100644
index 000000000..c504f0627
--- /dev/null
+++ b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R5.md
@@ -0,0 +1,48 @@
+| Previous finding | Round 5 assessment |
+|---|---|
+| R1-1: flat tenant borrows a nested socket | Fixed by the cgroup check (§5.4). |
+| R1-2: aliases and path routes remain public | Fixed for attached aliases and path maps (§5.1). Platform-minted route rows present a separate classification gap below. |
+| 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 by the admission barrier (§5.1). |
+| R2-2: upgrade serves unclassified engines | Fixed by refusal of unclassified routes before listeners open (§5.1). |
+| R2-3: flat callers borrow door credentials | Fixed by the door’s UID restriction (§§5.4, 6.2). |
+| R2-4: deployment verification fails | Ticket mechanism provided (§5.8); its probe-path source has a separate integration gap below. |
+| R2-5: port-80 refusal cannot work remotely | Resolved by the narrowed contract (§5.1). |
+| R3-1: previously admitted requests cross the mark | Fixed: acknowledgement waits for cancellation and completion (§5.1). |
+| R3-2: flat tenant injects into a nested caller | Fixed at spec level by excluding unisolated execution while armed (§6.2), with historical compromise explicitly outside that guarantee. |
+| R3-3: grant-only routes lack watch tickets | Fixed: every deploy target receives a ticket (§5.8). |
+| R4-1: foreign instances and workers remain unisolated | Fixed for the reported attack (§6.2). The arming predicate also rejects supported isolated routes; see below. |
+| R4-2: path routing widens an engine grant | Fixed by exact-host engine dispatch without path routing (§5.4). |
+| R4-3: watch tickets expire mid-watch | Fixed by renewal every four minutes (§5.8). |
+
+Reviewed spec `50a1f3fc` against locally available amadan `origin/main` at `512baa59`. All implementation files cited below match that revision. No files changed.
+
+1. **P2 — Platform-minted hostnames cannot complete classification (§5.1).**
+
+ Start with an ordinary public instance and its automatically minted `<app>.<account>.<apps-domain>` hostname. Upgrade the edge. Both rows receive `NULL`, but the minted row has no live release of its own. Following the specified classifier leaves that hostname refused indefinitely, even with a healthy bucket and a readable source manifest.
+
+ Platform domains are separate registry rows: `mintedRoute` copies the backend into a new `Platform: true` row without a version ([reconcile.go:881](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/domains/reconcile.go:881)). Adoption excludes those rows expressly because they have no independently executed live symlink ([adopt.go:1210](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/release/adopt.go:1210)). The manifest loader returns nothing when that hostname has no live version ([caps_pass.go:111](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/caps_pass.go:111)). These rows therefore do not inherit the primary upstream through the separate `route_aliases` fold described in §5.1.
+
+ **Suggested fix:** Define how platform-minted rows resolve to their source route and share its classification and admission barrier. They must remain usable for public sources and become internal before an engine source activates.
+
+2. **P2 — The arming predicate rejects isolated unit-backed routes (§6.2).**
+
+ Put a granted nested caller and a DynamicUser-backed engine on the same box. Run `carlos engines arm`. Section 6.2 explicitly permits DynamicUser services, but its requirement that **every `instance` route classify `nested`** rejects the engine. The caller consequently receives no engine socket.
+
+ Unit-backed capability routes are still `Kind == "instance"` ([adopt.go:1225](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/release/adopt.go:1225), [adopt.go:1265](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/release/adopt.go:1265)). Their standard socket is `/run/carlos/apps/<host>.sock` ([carlos-app@.socket:35](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/units/carlos-app@.socket:35)). `Classify` recognises only the flat and nested exec paths, so this route classifies `foreign` ([layout.go:103](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/layout.go:103)). Platform-minted instance rows can fail the same test because they copy another hostname’s socket.
+
+ **Suggested fix:** Apply the nested-layout requirement to tenant execution owners using the exec backend. Admit the explicitly permitted isolated unit-backed class separately, and assess generated aliases through their execution owner. Retain the refusal of actual foreign exec launches and workers.
+
+3. **P2 — The home edge has no source for the specified deployment probe path (§5.8).**
+
+ Configure an internal app’s build probe as `/healthz`, then deploy it. The CLI polls `/healthz`, but §5.8 permits only `/` or “the release’s declared probe path.” No such declaration exists in the release manifest, and the proposed ticket carries only hostname, version and expiry. The home edge cannot establish that `/healthz` is allowed.
+
+ The console reads the probe from its app database and returns it with the ship response ([apicli.go:2114](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/console/apicli.go:2114), [apicli.go:2285](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/console/apicli.go:2285)). The CLI uses that value ([deploy.go:404](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/deploy.go:404)); `release.Manifest` contains no probe field ([release.go:47](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/release/release.go:47)).
+
+ **Suggested fix:** Include the authorized probe path in the signed watch ticket, sourced from the same configuration the watcher uses. Define the corresponding signed path for bucket-mode watches.
+
+**Overall verdict: accept with fixes.** The round-4 security findings are addressed at spec level; these three integration gaps remain.
\ No newline at end of file