amadan
spec: fleet-internal engines, Astra round 12 findings (reject, 2 P1: own-bound port, shared-backend service row)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+65
−0
docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R12.md+65 −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 ok github.com/carlosframework/platform 105.567s ? github.com/carlosframework/platform/cmd/changelog [no test files] ok github.com/carlosframework/platform/cmd/console 2.923s ok github.com/carlosframework/platform/cmd/moveprobe 93.371s ok github.com/carlosframework/platform/cmd/zddprobe 0.718s amadan: job cancelled — a newer push superseded it
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R12.md b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R12.md| new file mode 100644 |
| index 000000000..cc75460e4 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R12.md |
| @@ -0,0 +1,65 @@ |
| +| Previous finding | Round 12 assessment | |
| +|---|---| |
| +| R1-1: flat tenant borrows a nested socket | Fixed by peer-cgroup authentication (§5.4). | |
| +| R1-2: aliases and path routes remain public | Fixed for aliases and path maps by checking the final upstream (§5.1). | |
| +| R1-3: new box starts public | Fixed by classification before serving (§5.1). | |
| +| R1-4: revoked grants return after restart | Fixed with retained state; fresh-box replay remains an explicit residual (§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 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 startup classification and refusal of `NULL` (§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 | Fixed by watch tickets (§5.8). | |
| +| R2-5: port-80 refusal cannot work remotely | Resolved by the narrowed contract (§5.1). | |
| +| R3-1: previously admitted requests cross the mark | Fixed by waiting for cancellation and completion before acknowledging the fence (§5.1). | |
| +| R3-2: flat tenant injects into a nested caller | Fixed by excluding unisolated execution while armed; historical compromise remains explicitly excluded (§6.2). | |
| +| 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 by arming prerequisites and launch refusals (§6.2). | |
| +| R4-2: path routing widens an engine grant | Fixed by exact-host engine dispatch (§5.4). | |
| +| R4-3: watch tickets expire mid-watch | Fixed by renewal (§5.8). | |
| +| R5-1: platform-minted hostnames cannot classify | Fixed by execution-owner inheritance (§5.1). | |
| +| R5-2: arming rejects isolated unit-backed routes | Fixed by distinguishing backing from layout (§6.2). | |
| +| R5-3: home edge lacks the probe path | Fixed by signing the probe path (§5.8). | |
| +| R6-1: minted row’s own grant is ignored | Fixed by aggregating group grants (§5.1). | |
| +| R6-2: static platform domains are refused | Fixed by restricting inheritance to minted instance rows (§5.1). | |
| +| R7-1: clearing exposes a still-serving generation | Fixed by stopping the group and proving its cgroups empty (§5.1). | |
| +| R7-2: TCP-backed minted rows have no owner | Fixed by explicit ownership and unique non-empty backend matching (§5.1). | |
| +| R8-1: upgrade classifies a running declaring build public | Reported case fixed by scanning staged manifests; missing-manifest exposure remains an explicit residual (§5.1). | |
| +| R8-2: sleeping unit-backed route cannot clear | Resolved by operator-controlled stop-and-clear (§5.1). | |
| +| R9-1: recovery launches a declaring `GoodVersion` after clearing | Fixed by gating the actual selected build (§5.1). | |
| +| R10-1: a written but unfenced `1` permits recovery launch | Fixed: every declaring launch waits for the current mark’s fence (§5.1). | |
| +| R11-1: granted TCP sockets bypass the edge | Reported generated-listener path addressed by the capability exclusion and listener removal. Autonomous starts are covered by the live-link constraint (§5.1). A separate application-bound listener path remains below. | |
| + |
| +Reviewed `a2f71f5f` against locally available amadan `origin/main` at `771ca01b`. All implementation files cited below match that revision. Static review; no files changed. |
| + |
| +**1. P1 — An application-bound high port remains public while I1 holds (§§5.1, 6.3).** |
| + |
| +Concrete sequence: |
| + |
| +1. Deploy a unit-backed HTTP engine declaring `doc_engine`, with no `ports` declaration or port grant. Configure its server to bind all interfaces on port `9000`, on a deployment whose firewall permits public ingress there. |
| +2. Complete the launch gate: mark the group internal, load the serving map, finish the fence, then start the declaring build. |
| +3. The application binds port `9000` itself. A public client connects directly and reaches the engine. |
| + |
| +**I1 holds:** the process starts after its group is fenced, and the mark never clears. Neither new protection applies: there is no `ports` capability to reject and no generated TCP socket unit to remove. |
| + |
| +This is a supported execution shape. The service template explicitly permits TCP-only apps to bind their own ports ([carlos-app@.service:21](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/units/carlos-app@.service:21)). The capability validator limits `ports` to `1..1023` and states that a high port needs no platform assistance ([caps.go:401](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/caps/caps.go:401)). The service permits `AF_INET` and `AF_INET6` without a bind restriction ([carlos-app@.service:66](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/units/carlos-app@.service:66)); the engine’s generated network restrictions deny private ranges, leaving public addresses outside that deny list ([render.go:88](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/caps/render.go:88), [render.go:225](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/caps/render.go:225)). |
| + |
| +**Suggested fix:** Enforce the ingress restriction on sockets the engine creates itself, including its children’s sockets. Assign a kernel-enforced network boundary that preserves required outbound access and engine-local communication while preventing direct public ingress. Establish that boundary before acknowledging the fence. Test an engine with no `ports` declaration that attempts to serve on a high port. |
| + |
| +**2. P1 — A separate public service row can proxy to the fenced engine (§§5.1, 6.3).** |
| + |
| +Concrete sequence: |
| + |
| +1. Have an ordinary unit-backed instance E serving HTTP at `127.0.0.1:9000`. A separate, non-platform `service` row S uses that same upstream—for example, a pre-existing alternate hostname. |
| +2. Adopt a declaring build on E. Complete its launch gate and fence E’s execution group before starting the build. |
| +3. S remains `0` because §5.1 classifies service rows public by construction. Its ownership mechanism includes only E and platform-minted instance rows. |
| +4. Send a public request to S’s hostname. The final resolved route is S, whose public check passes; its proxy connects directly to E’s loopback listener. |
| + |
| +**I1 holds:** E’s process started after its group was fenced, and that group remains internal. This path also satisfies “every way in goes through the edge”; the edge checks a different route row pointing to the same process. |
| + |
| +Existing code permits this configuration. `carlos add` accepts `service` and an explicit upstream address, then stores those values on an independent row ([cli.go:126](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/cli.go:126), [cli.go:276](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/cli.go:276)). The edge builds its TCP proxy from that row’s address ([edge.go:760](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:760)) and retains that same row as the upstream’s route identity ([edge.go:889](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:889)). Dispatch invokes the proxy directly ([edge.go:1790](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:1790)); it does not resolve the destination back through E’s hostname. Engine loopback access is deliberately retained ([render.go:69](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/caps/render.go:69)). |
| + |
| +**Suggested fix:** Extend execution ownership and fencing to every local route that targets the protected backend, including independently created service rows, or refuse those duplicate backend bindings. Apply the rule to existing rows and later route changes. Test a public service hostname sharing an engine’s TCP address or Unix socket. |
| + |
| +**Overall verdict: reject.** Both paths let the public reach a declaring build while the revised I1 holds. |
| \ No newline at end of file |