From 0f6ad4e0a0b08b29033a4636cb3ef06e0d4e4222 Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 08:24:04 -0400
Subject: [PATCH 1/8] spec: model segment-exact exec and create matching (#49)

---
 spec/README.md  |  34 +++++++++++-----
 spec/router.qnt | 106 +++++++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 119 insertions(+), 21 deletions(-)

diff --git a/spec/README.md b/spec/README.md
index 13fef2b..693e675 100644
--- a/spec/README.md
+++ b/spec/README.md
@@ -9,7 +9,7 @@ This directory contains a [Quint](https://quint-lang.org/) formal specification
 | `docker_socket_policy.qnt` | Request-handling spec: policy types, state machine, endpoint routing table, 9 invariants (6 P0 / 3 P1), 6 attack scenario simulations |
 | `listener.qnt` | Listening-socket startup: flag/group selection, existing-path checks, single-instance lock, 6 invariants, one `run` test per design-table row. Instances `listener_locked` (Go, Rust) and `listener_unlocked` (TypeScript) |
 | `listener-design.md` | Design of the listening socket (dockerd parity) that `listener.qnt` models |
-| `router.qnt` | The percent-encoded path deny, container-name extraction and the container-lifecycle branch of the router only, not the full router. The daemon's percent-decoding as a fixed table. One `run` test per table row. Instances `router` (Go, TypeScript, and Rust after #48 and #53), `router_pre48` (Rust's extraction rule before #48) and `router_pre53` (Rust and TypeScript before #53, routing on the raw path) |
+| `router.qnt` | The percent-encoded path deny, the segment-exact exec deny and `POST /containers/create` route, container-name extraction and the container-lifecycle branch of the router only, not the full router. The daemon's percent-decoding as a fixed table. One `run` test per table row. Instances `router` (Go, TypeScript, and Rust after #48 and #53), `router_pre48` (Rust's extraction rule before #48) and `router_pre53` (Rust and TypeScript before #53, routing on the raw path) |
 
 ## How to Run
 
@@ -84,12 +84,15 @@ quint run spec/listener.qnt --main=listener_unlocked --max-steps=30 --invariant
 
 ### Router path parsing (`router.qnt`)
 
-A path is a list of raw, still percent-encoded segments with the query string removed, so `/containers/` is `["containers", ""]`, `/containers//start` is `["containers", "", "start"]` and `/containers/%2F` is `["containers", "%2F"]`. The first check in `route` denies any path with an encoded segment, for every method (#53). After it, the second segment is a container name unless it is empty or one of `create`, `json`, `exec`. Both properties check every method in `GET`, `POST`, `DELETE` against every path of 1 to 3 segments:
+A path is a list of raw, still percent-encoded segments with the query string removed, so `/containers/` is `["containers", ""]`, `/containers//start` is `["containers", "", "start"]` and `/containers/%2F` is `["containers", "%2F"]`. The first check in `route` denies any path with an encoded segment, for every method (#53). The second denies exec, for every method, as `denyExec` (#49): when the first segment is `exec` (the `/exec/<id>/…` namespace), or when the first segment is `containers` and any later segment is exactly `exec`. A segment that only starts with or contains `exec`, such as `exec-runner`, is not matched. The third routes `POST` with exactly the segments `["containers", "create"]` to `routeCreate`; a longer path falls through. After these, the second segment is a container name unless it is empty or one of `create`, `json`, `exec`. Every property checks every method in `GET`, `POST`, `DELETE` against every path of 1 to 3 segments:
 
 - `lifecycleOnlyTargetsRealNames` holds when each lifecycle allow (`allowKnown` or `allowUnknown`) targets a non-empty, non-reserved name.
 - `routerSeesWhatDaemonSees` holds when every request the router does not deny reads the same to the daemon: decoding leaves its path unchanged. The daemon's decoding is the table `DAEMON_DECODING`: `%2F` and `%2f` decode to `["", ""]` (a `/` splits the segment), `%6A%73%6F%6E` to `["json"]`, and `beacon%2Fstart` to `["beacon", "start"]`.
+- `execNeverAllowed` holds when every path with `exec` in an exec position is denied. The exec positions are written out in the property, not taken from `route`'s `isExecPath`.
+- `execPrefixNamesRoute` holds when renaming `exec-runner` to the plain unknown name `mycontainer`, wherever it appears in the path, never changes the outcome.
+- `createOnlyExact` holds when `routeCreate` is the outcome for exactly `POST /containers/create`.
 
-On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames` and `percentSoundTest` asserts `routerSeesWhatDaemonSees`.
+On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames`, `percentSoundTest` asserts `routerSeesWhatDaemonSees`, `execSoundTest` asserts `execNeverAllowed`, `execPrefixSoundTest` asserts `execPrefixNamesRoute` and `createExactSoundTest` asserts `createOnlyExact`.
 
 | Row (`run <row>Test`) | Request | Outcome | Instances |
 |-----|---------|---------|-----------|
@@ -98,7 +101,7 @@ On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames` and `percentSou
 | `emptyNameGetAllowed` | `GET /containers/` | allow (passthrough) | all |
 | `reservedJsonDeleteDenied` | `DELETE /containers/json` | deny | all |
 | `reservedCreateDeleteDenied` | `DELETE /containers/create` | deny | all |
-| `reservedExecDeleteDenied` | `DELETE /containers/exec` | deny | all |
+| `reservedExecDeleteDenied` | `DELETE /containers/exec` | deny (exec) | all |
 | `realNameDeleteAllowed` | `DELETE /containers/mycontainer` | allow (unknown container) | all |
 | `reservedInSubpathAllowed` | `GET /containers/mycontainer/json` | allow | all |
 
@@ -113,7 +116,20 @@ Rows for the percent-encoded path deny ([#53](https://github.com/ChainSafe/docke
 | `percentSubpathStartDenied` (pin) | `POST /containers/beacon%2Fstart` | deny | `POST /containers/beacon/start` |
 | `percentGetDenied` | `GET /containers/%2F` | deny | `GET /containers//` |
 
-Each implementation's router tests use the same row names in comments (added with the #48 and #53 fixes). `router_pre48` runs `pre48UnsoundTest`, which asserts that `lifecycleOnlyTargetsRealNames` fails and that both `emptyName*Denied` requests are allowed as an unknown container ([#48](https://github.com/ChainSafe/docker-socket-policy/issues/48)). `router_pre53` runs `pre53UnsoundTest`, which asserts that `routerSeesWhatDaemonSees` fails, that `DELETE /containers/%2F` and `POST /containers/%2F/start` are allowed as an unknown container, and that `GET /containers/%2F` is allowed through the passthrough.
+Rows for segment-exact exec and create matching ([#49](https://github.com/ChainSafe/docker-socket-policy/issues/49)), all instances. "deny (exec)" is the outcome `denyExec`, which the implementations report as `exec is not allowed`:
+
+| Row (`run <row>Test`) | Request | Outcome |
+|-----|---------|---------|
+| `execSubpathDeleteDenied` | `DELETE /containers/mycontainer/exec` | deny (exec) |
+| `execSubpathPostDenied` | `POST /containers/mycontainer/exec` | deny (exec) |
+| `execPrefixNameStartAllowed` | `POST /containers/exec-runner/start` | allow (unknown container) |
+| `execPrefixNameDeleteAllowed` | `DELETE /containers/exec-runner` | allow (unknown container) |
+| `execPrefixNameGetAllowed` | `GET /containers/exec-runner/json` | allow (read) |
+| `execNamespaceGetDenied` | `GET /exec/abc/json` | deny (exec) |
+| `execNamespacePostDenied` | `POST /exec/abc/start` | deny (exec) |
+| `createSubpathDenied` | `POST /containers/create/extra` | deny (default, not the create route) |
+
+Each implementation's router tests use the same row names in comments (added with the #48, #53 and #49 fixes). `router_pre48` runs `pre48UnsoundTest`, which asserts that `lifecycleOnlyTargetsRealNames` fails and that both `emptyName*Denied` requests are allowed as an unknown container ([#48](https://github.com/ChainSafe/docker-socket-policy/issues/48)). `router_pre53` runs `pre53UnsoundTest`, which asserts that `routerSeesWhatDaemonSees` fails, that `DELETE /containers/%2F` and `POST /containers/%2F/start` are allowed as an unknown container, and that `GET /containers/%2F` is allowed through the passthrough.
 
 ### Modeling Notes
 
@@ -130,11 +146,9 @@ Two invariants are structurally tautological within the Quint model — they can
 - **The query string is outside the model.** Paths are segment lists with the query string already removed, so the model says nothing about `%` in the query. The implementations never inspect the query string for this rule; encoded queries such as `?filters=%7B…%7D` are routine and must still be forwarded. That is pinned by the language handler tests and the integration tests, not by the model.
 - **GET is covered.** The percent check runs before the GET passthrough, and `routerSeesWhatDaemonSees` ranges over `GET` as well as `POST` and `DELETE`. On `router_pre53` the passthrough lets `GET /containers/%2F` through, and the property fails for it too.
 - **No instance models Go before #53.** Go decoded before routing, which is `route(m, decodePath(segs))`. With this table that agrees with the daemon by construction, so `routerSeesWhatDaemonSees` cannot express Go's risk: decoding that differs from the daemon's, such as encoded version segments ([#57](https://github.com/ChainSafe/docker-socket-policy/issues/57)). Go's change is covered by the language handler tests.
-- **`router.qnt` is not the full router.** `route` models the percent check, which runs first in all three routers, and the container-lifecycle branch. It leaves out the API-version strip and the checks that the routers run between those two, such as the exec, build and commit denials and `POST /containers/create`. For paths that those checks catch, the model's outcome can differ from what an implementation does:
-  - `DELETE /containers/mycontainer/exec` is `allowUnknown` in the model. Rust and TypeScript deny it with their exec checks. Go's exec check matches `exec` only in the name position, so Go sends this path down the lifecycle branch and allows it. This divergence between the languages belongs to the same family as [#24](https://github.com/ChainSafe/docker-socket-policy/issues/24) and [#48](https://github.com/ChainSafe/docker-socket-policy/issues/48). It is outside this model's scope and is tracked with the other routing divergences.
-  - `POST /containers/create` is `deny` in the model, but in reality it routes to container create.
-
-  Only the properties and the table rows are claims about the code. `reservedExecDeleteDenied` (`DELETE /containers/exec`) is decided in all three implementations by the exec check, not by the reserved set. Its language tests would therefore not catch `exec` being dropped from the reserved set.
+- **`router.qnt` is not the full router.** `route` models the percent check, which runs first in all three routers, the exec check, the exact `POST /containers/create` route and the container-lifecycle branch, in that order. It leaves out the API-version strip and the other checks that the routers run before the lifecycle branch, such as the read-only endpoints, auth, and the build and commit denials, as well as `POST /images/create` and the endpoints after the lifecycle branch. For paths that those checks catch, the model's outcome can differ from what an implementation does: `GET /build` is `allowRead` in the model, for example, while the routers deny it as `build is not allowed`. The `images` rows of #49 (`GET /images/exec` allowed, `POST /images/create/extra` denied) are therefore language-only rows. Only the properties and the table rows are claims about the code.
+- **Exec and create match whole segments (#49).** Before #49 the routers disagreed: Go matched `exec` only in the name position (`/containers/exec`), so `DELETE /containers/mycontainer/exec` went down the lifecycle branch and was allowed, and `GET /exec/<id>/json` went through the GET passthrough. Rust matched the substring `/exec` anywhere after `/containers/`, and TypeScript anywhere in the path, so both also denied containers named `exec-runner` or `executor`. Go also accepted `POST /containers/create/extra` as a container create. In the model the exec check runs before the create route, the lifecycle branch and the GET passthrough, so it denies every method, GET included: exec inspect shows the full command line. `reservedExecDeleteDenied` (`DELETE /containers/exec`) is decided by the exec check, as in all three implementations, and now asserts `denyExec`. `exec` stays in the reserved set, but no row, in the model or in the language tests, would catch it being dropped from there.
+- **The #49 properties are not vacuous.** None of them is shown on a separate instance; replacing the rule in `route` makes them fail. With a substring-style rule (a segment that starts with `exec`, modeled as the set `exec`, `exec-runner`), `execPrefixSoundTest` and the three `execPrefixName*Allowed` rows fail. With Go's rule before #49 (`exec` only as the second segment under `containers`), `execSoundTest` and the four `exec*Denied` rows fail. `execSubpathPostDenied` and `execNamespacePostDenied` fail there only because the outcome is the default `deny`, not `denyExec`: the request is still refused, as before #49, but not by the exec check. With Go's prefix match for create, `createExactSoundTest` and `createSubpathDenied` fail. `execNeverAllowed` writes out the exec positions itself instead of calling `isExecPath`, so that a narrower `isExecPath` cannot narrow the property with it.
 - **HEAD is outside the model.** `METHODS` is `GET`, `POST`, `DELETE`. The real lifecycle branches agree on those three methods only. For `HEAD /containers/x`, Go and TypeScript fall through to the GET/HEAD passthrough and allow it. Rust denies it in the lifecycle branch.
 - **Listener fault bias.** `step` crashes an instance on 1 in 10 draws instead of half of all steps, so random runs actually interleave live instances. Every crash stays reachable from every phase, so the reachable state space is unchanged.
 
diff --git a/spec/router.qnt b/spec/router.qnt
index 9299f5e..5b26ff3 100644
--- a/spec/router.qnt
+++ b/spec/router.qnt
@@ -1,13 +1,14 @@
 // ─── Module: router_model ───────────────────────────────────────────────
 //
 // How the router extracts a container name from a request path, how the
-// container-lifecycle branch routes on it (#48), and the percent-encoded
-// path deny that runs first in the router (#53). Mirrors
+// container-lifecycle branch routes on it (#48), the percent-encoded
+// path deny that runs first in the router (#53), and the segment-exact exec
+// deny and POST /containers/create route (#49). Mirrors
 // `extract_container_name` and the lifecycle branch of `Router::route` in
-// rs/src/proxy.rs. This is not the full router: the percent check is
-// modeled, but the API-version strip and the checks that run between the
-// percent check and the lifecycle branch (exec, build, commit,
-// POST /containers/create) are left out. Go (`extractContainerName`) and
+// rs/src/proxy.rs. This is not the full router: the API-version strip and
+// the other checks that run between the percent check and the lifecycle
+// branch (build, commit, the read-only endpoints, auth) are left out, as is
+// POST /images/create. Go (`extractContainerName`) and
 // TypeScript (`extractContainerName`) have the same lifecycle branch for
 // GET, POST and DELETE. HEAD differs: Go and TypeScript allow it through
 // the passthrough, Rust denies it. HEAD is outside METHODS.
@@ -91,9 +92,27 @@ module router_model {
   pure def routeByName(name: str): str =
     if (KNOWN_SERVICES.contains(name)) "allowKnown" else "allowUnknown"
 
-  // The percent check (#53) comes first, before the GET passthrough.
+  // Exec matches whole segments only (#49): the `/exec/<id>/…` namespace,
+  // or `exec` anywhere after `containers`. A segment such as `exec-runner`
+  // is a name like any other.
+  pure def isExecPath(segs: List[str]): bool =
+    if (segs.length() == 0) false
+    else or {
+      segs[0] == "exec",
+      segs[0] == "containers" and segs.indices().exists(i => i >= 1 and segs[i] == "exec"),
+    }
+
+  pure def isDenied(outcome: str): bool =
+    outcome == "deny" or outcome == "denyExec"
+
+  // The percent check (#53) comes first. The exec check (#49) follows, before
+  // the create route, the lifecycle branch and the GET passthrough, so it
+  // denies every method. POST /containers/create matches only the exact
+  // segments; a longer path falls through.
   pure def route(method: str, segs: List[str]): str =
     if (not(ALLOW_PERCENT) and hasEncodedSeg(segs)) "deny"
+    else if (isExecPath(segs)) "denyExec"
+    else if (method == "POST" and segs == ["containers", "create"]) "routeCreate"
     else if (hasContainerName(segs)) {
       val name = containerNameOf(segs)
       if (method == "POST" and BY_NAME_ACTIONS.contains(lastSeg(segs))) routeByName(name)
@@ -110,6 +129,7 @@ module router_model {
   pure val WORDS = Set(
     "containers", "", "json", "create", "exec", "mycontainer", "beacon", "start",
     "%2F", "%2f", "%6A%73%6F%6E", "beacon%2Fstart",
+    "exec-runner", "abc", "extra",
   )
   pure val METHODS = Set("GET", "POST", "DELETE")
 
@@ -134,14 +154,42 @@ module router_model {
   // decoding leaves its path unchanged (#53). Ranges over GET too.
   pure val routerSeesWhatDaemonSees: bool =
     METHODS.forall(m => PATHS.forall(segs =>
-      route(m, segs) != "deny" implies decodePath(segs) == segs
+      not(isDenied(route(m, segs))) implies decodePath(segs) == segs
+    ))
+
+  // A path with `exec` in an exec position is denied for every method (#49).
+  // Ranges over GET too. The exec positions are written out here rather
+  // than taken from isExecPath, so that a narrower rule in `route` fails it.
+  pure val execNeverAllowed: bool =
+    METHODS.forall(m => PATHS.forall(segs =>
+      segs.indices().exists(i => and {
+        segs[i] == "exec",
+        i == 0 or segs[0] == "containers",
+      }) implies isDenied(route(m, segs))
+    ))
+
+  // `exec-runner` only starts with `exec`. Renaming it to the plain unknown
+  // name `mycontainer`, wherever it appears, never changes the outcome (#49).
+  pure def renameExecLike(segs: List[str]): List[str] =
+    segs.foldl([], (acc, s) => acc.append(if (s == "exec-runner") "mycontainer" else s))
+
+  pure val execPrefixNamesRoute: bool =
+    METHODS.forall(m => PATHS.forall(segs =>
+      route(m, segs) == route(m, renameExecLike(segs))
+    ))
+
+  // The create route is taken for exactly POST /containers/create (#49).
+  pure val createOnlyExact: bool =
+    METHODS.forall(m => PATHS.forall(segs =>
+      (route(m, segs) == "routeCreate") iff (m == "POST" and segs == ["containers", "create"])
     ))
 
   // ─── Tests: one run per table row ───────────────────────────────────
   //
   // Rows whose outcome depends on neither ALLOW_EMPTY_NAME nor
-  // ALLOW_PERCENT run on every instance. The rows that do, soundTest and
-  // percentSoundTest live in `router`.
+  // ALLOW_PERCENT run on every instance. The rows that do and the property
+  // tests (soundTest, percentSoundTest, execSoundTest, execPrefixSoundTest,
+  // createExactSoundTest) live in `router`.
 
   run emptyNameGetAllowedTest =
     assert(route("GET", ["containers", ""]) == "allowRead")
@@ -152,14 +200,41 @@ module router_model {
   run reservedCreateDeleteDeniedTest =
     assert(route("DELETE", ["containers", "create"]) == "deny")
 
+  // Decided by the exec check, as in all three implementations.
   run reservedExecDeleteDeniedTest =
-    assert(route("DELETE", ["containers", "exec"]) == "deny")
+    assert(route("DELETE", ["containers", "exec"]) == "denyExec")
 
   run realNameDeleteAllowedTest =
     assert(route("DELETE", ["containers", "mycontainer"]) == "allowUnknown")
 
   run reservedInSubpathAllowedTest =
     assert(route("GET", ["containers", "mycontainer", "json"]) == "allowRead")
+
+  // Segment-exact exec and create matching (#49).
+
+  run execSubpathDeleteDeniedTest =
+    assert(route("DELETE", ["containers", "mycontainer", "exec"]) == "denyExec")
+
+  run execSubpathPostDeniedTest =
+    assert(route("POST", ["containers", "mycontainer", "exec"]) == "denyExec")
+
+  run execPrefixNameStartAllowedTest =
+    assert(route("POST", ["containers", "exec-runner", "start"]) == "allowUnknown")
+
+  run execPrefixNameDeleteAllowedTest =
+    assert(route("DELETE", ["containers", "exec-runner"]) == "allowUnknown")
+
+  run execPrefixNameGetAllowedTest =
+    assert(route("GET", ["containers", "exec-runner", "json"]) == "allowRead")
+
+  run execNamespaceGetDeniedTest =
+    assert(route("GET", ["exec", "abc", "json"]) == "denyExec")
+
+  run execNamespacePostDeniedTest =
+    assert(route("POST", ["exec", "abc", "start"]) == "denyExec")
+
+  run createSubpathDeniedTest =
+    assert(route("POST", ["containers", "create", "extra"]) == "deny")
 }
 
 // ─── Instances ──────────────────────────────────────────────────────────
@@ -202,6 +277,15 @@ module router {
 
   run percentSoundTest =
     assert(routerSeesWhatDaemonSees)
+
+  run execSoundTest =
+    assert(execNeverAllowed)
+
+  run execPrefixSoundTest =
+    assert(execPrefixNamesRoute)
+
+  run createExactSoundTest =
+    assert(createOnlyExact)
 }
 
 // Rust before #48: `/containers/` and `/containers//start` reach

From 224028887d306321d1374106e3c729dfb2bec6df Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 08:26:37 -0400
Subject: [PATCH 2/8] spec: correct the #49 history note and instance
 descriptions (#49)

---
 spec/README.md  | 6 +++---
 spec/router.qnt | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/spec/README.md b/spec/README.md
index 693e675..eaf322a 100644
--- a/spec/README.md
+++ b/spec/README.md
@@ -9,7 +9,7 @@ This directory contains a [Quint](https://quint-lang.org/) formal specification
 | `docker_socket_policy.qnt` | Request-handling spec: policy types, state machine, endpoint routing table, 9 invariants (6 P0 / 3 P1), 6 attack scenario simulations |
 | `listener.qnt` | Listening-socket startup: flag/group selection, existing-path checks, single-instance lock, 6 invariants, one `run` test per design-table row. Instances `listener_locked` (Go, Rust) and `listener_unlocked` (TypeScript) |
 | `listener-design.md` | Design of the listening socket (dockerd parity) that `listener.qnt` models |
-| `router.qnt` | The percent-encoded path deny, the segment-exact exec deny and `POST /containers/create` route, container-name extraction and the container-lifecycle branch of the router only, not the full router. The daemon's percent-decoding as a fixed table. One `run` test per table row. Instances `router` (Go, TypeScript, and Rust after #48 and #53), `router_pre48` (Rust's extraction rule before #48) and `router_pre53` (Rust and TypeScript before #53, routing on the raw path) |
+| `router.qnt` | The percent-encoded path deny, the segment-exact exec deny and `POST /containers/create` route, container-name extraction and the container-lifecycle branch of the router only, not the full router. The daemon's percent-decoding as a fixed table. One `run` test per table row. Instances `router` (Go, TypeScript, and Rust after #48, #53 and #49), `router_pre48` (Rust's extraction rule before #48) and `router_pre53` (Rust and TypeScript before #53, routing on the raw path). Every instance includes the #49 exec and create rule, so the pre instances isolate one earlier rule each rather than being full snapshots |
 
 ## How to Run
 
@@ -146,8 +146,8 @@ Two invariants are structurally tautological within the Quint model — they can
 - **The query string is outside the model.** Paths are segment lists with the query string already removed, so the model says nothing about `%` in the query. The implementations never inspect the query string for this rule; encoded queries such as `?filters=%7B…%7D` are routine and must still be forwarded. That is pinned by the language handler tests and the integration tests, not by the model.
 - **GET is covered.** The percent check runs before the GET passthrough, and `routerSeesWhatDaemonSees` ranges over `GET` as well as `POST` and `DELETE`. On `router_pre53` the passthrough lets `GET /containers/%2F` through, and the property fails for it too.
 - **No instance models Go before #53.** Go decoded before routing, which is `route(m, decodePath(segs))`. With this table that agrees with the daemon by construction, so `routerSeesWhatDaemonSees` cannot express Go's risk: decoding that differs from the daemon's, such as encoded version segments ([#57](https://github.com/ChainSafe/docker-socket-policy/issues/57)). Go's change is covered by the language handler tests.
-- **`router.qnt` is not the full router.** `route` models the percent check, which runs first in all three routers, the exec check, the exact `POST /containers/create` route and the container-lifecycle branch, in that order. It leaves out the API-version strip and the other checks that the routers run before the lifecycle branch, such as the read-only endpoints, auth, and the build and commit denials, as well as `POST /images/create` and the endpoints after the lifecycle branch. For paths that those checks catch, the model's outcome can differ from what an implementation does: `GET /build` is `allowRead` in the model, for example, while the routers deny it as `build is not allowed`. The `images` rows of #49 (`GET /images/exec` allowed, `POST /images/create/extra` denied) are therefore language-only rows. Only the properties and the table rows are claims about the code.
-- **Exec and create match whole segments (#49).** Before #49 the routers disagreed: Go matched `exec` only in the name position (`/containers/exec`), so `DELETE /containers/mycontainer/exec` went down the lifecycle branch and was allowed, and `GET /exec/<id>/json` went through the GET passthrough. Rust matched the substring `/exec` anywhere after `/containers/`, and TypeScript anywhere in the path, so both also denied containers named `exec-runner` or `executor`. Go also accepted `POST /containers/create/extra` as a container create. In the model the exec check runs before the create route, the lifecycle branch and the GET passthrough, so it denies every method, GET included: exec inspect shows the full command line. `reservedExecDeleteDenied` (`DELETE /containers/exec`) is decided by the exec check, as in all three implementations, and now asserts `denyExec`. `exec` stays in the reserved set, but no row, in the model or in the language tests, would catch it being dropped from there.
+- **`router.qnt` is not the full router.** `route` models the percent check, which runs first in all three routers, the exec check, the exact `POST /containers/create` route and the container-lifecycle branch, in that order. It leaves out the API-version strip and the other checks that the routers run before the lifecycle branch, such as the read-only endpoints, auth, and the build and commit denials, as well as `POST /images/create` and the endpoints after the lifecycle branch. For paths that those checks catch, the model's outcome can differ from what an implementation does: `GET /build` is `allowRead` in the model, for example, while the routers deny it as `build is not allowed`. The `images` rows of #49 (`GET /images/exec` allowed, `POST /images/create/extra` denied) are therefore language-only rows, as are `GET /containers/myexec/json` and `DELETE /containers/executor`: the model's words are atoms, so it cannot express a name that merely contains `exec`. Only the properties and the table rows are claims about the code.
+- **Exec and create match whole segments (#49).** Before #49 the routers disagreed: Go matched `exec` only in the name position (`/containers/exec`), so `DELETE /containers/mycontainer/exec` went down the lifecycle branch and was allowed. Rust matched the substring `/exec` anywhere after `/containers/`, so both Go and Rust let `GET /exec/<id>/json` through the GET passthrough; and TypeScript anywhere in the path, so both also denied containers named `exec-runner` or `executor`. Go also accepted `POST /containers/create/extra` as a container create. In the model the exec check runs before the create route, the lifecycle branch and the GET passthrough, so it denies every method, GET included: exec inspect shows the full command line. `reservedExecDeleteDenied` (`DELETE /containers/exec`) is decided by the exec check, as in all three implementations, and now asserts `denyExec`. `exec` stays in the reserved set, but no row, in the model or in the language tests, would catch it being dropped from there.
 - **The #49 properties are not vacuous.** None of them is shown on a separate instance; replacing the rule in `route` makes them fail. With a substring-style rule (a segment that starts with `exec`, modeled as the set `exec`, `exec-runner`), `execPrefixSoundTest` and the three `execPrefixName*Allowed` rows fail. With Go's rule before #49 (`exec` only as the second segment under `containers`), `execSoundTest` and the four `exec*Denied` rows fail. `execSubpathPostDenied` and `execNamespacePostDenied` fail there only because the outcome is the default `deny`, not `denyExec`: the request is still refused, as before #49, but not by the exec check. With Go's prefix match for create, `createExactSoundTest` and `createSubpathDenied` fail. `execNeverAllowed` writes out the exec positions itself instead of calling `isExecPath`, so that a narrower `isExecPath` cannot narrow the property with it.
 - **HEAD is outside the model.** `METHODS` is `GET`, `POST`, `DELETE`. The real lifecycle branches agree on those three methods only. For `HEAD /containers/x`, Go and TypeScript fall through to the GET/HEAD passthrough and allow it. Rust denies it in the lifecycle branch.
 - **Listener fault bias.** `step` crashes an instance on 1 in 10 draws instead of half of all steps, so random runs actually interleave live instances. Every crash stays reachable from every phase, so the reachable state space is unchanged.
diff --git a/spec/router.qnt b/spec/router.qnt
index 5b26ff3..35a6c67 100644
--- a/spec/router.qnt
+++ b/spec/router.qnt
@@ -239,7 +239,7 @@ module router_model {
 
 // ─── Instances ──────────────────────────────────────────────────────────
 
-// Go, TypeScript, and Rust after #48 and #53: an empty segment is not a
+// Go, TypeScript, and Rust after #48, #53 and #49: an empty segment is not a
 // name, and a percent-encoded path is denied.
 module router {
   import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false).*

From 3ff44e2c902ea95ec8a7d61af5e37567cda2f5b2 Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 08:32:44 -0400
Subject: [PATCH 3/8] test: pin segment-exact exec and create matching (#49)

---
 deploy/test.sh                   | 17 ++++++++
 go/internal/proxy/router_test.go | 69 ++++++++++++++++++++++++++++++++
 rs/src/proxy.rs                  | 52 ++++++++++++++++++++++++
 ts/src/proxy.test.ts             | 47 ++++++++++++++++++++++
 4 files changed, 185 insertions(+)

diff --git a/deploy/test.sh b/deploy/test.sh
index 9fbffdf..f0e9e9a 100755
--- a/deploy/test.sh
+++ b/deploy/test.sh
@@ -369,6 +369,23 @@ check "DELETE /containers/%2F -> 403 (percent-encoded path)" "403" "$S"
 S=$(get_status "$PROXY/v1.45/containers/json?filters=%7B%22status%22%3A%5B%22running%22%5D%7D")
 check "GET /v1.45/containers/json?filters=<encoded> -> 200 (query not inspected)" "200" "$S"
 
+# #49: exec and create are matched on whole path segments. Exec is denied for
+# every method under /containers/<name>/exec and /exec/, GET included (exec
+# inspect leaks command lines). A name that only starts with exec reaches the
+# daemon (404, no such container — not a proxy 403). A create path with extra
+# segments is not the create endpoint, even with an allowed image.
+S=$(delete_status "$PROXY/containers/no-such/exec")
+check "DELETE /containers/*/exec -> 403 (exec subpath, any method)" "403" "$S"
+
+S=$(post_json '{"Image":"chainsafe/lodestar:beacon","Cmd":["--rcConfig","/data/config.yml"]}' "$PROXY/containers/create/extra")
+check "POST /containers/create/extra -> 403 (not the create endpoint)" "403" "$S"
+
+S=$(post_empty "$PROXY/containers/exec-nosuch/start")
+check "POST /containers/exec-nosuch/start -> 404 (daemon answered, not proxy 403)" "404" "$S"
+
+S=$(get_status "$PROXY/exec/0000000000000000000000000000000000000000000000000000000000000000/json")
+check "GET /exec/*/json -> 403 (exec inspect denied)" "403" "$S"
+
 # ─── Summary ──────────────────────────────────────────
 
 echo ""
diff --git a/go/internal/proxy/router_test.go b/go/internal/proxy/router_test.go
index 089d1fd..3475e77 100644
--- a/go/internal/proxy/router_test.go
+++ b/go/internal/proxy/router_test.go
@@ -530,6 +530,75 @@ allowed_image_prefixes:
 	}
 }
 
+// TestRouteExecAndExactEndpoints is the cross-language parity guard for #49.
+//
+// Exec and create are matched on whole path segments. Exec is denied for every
+// method when the first segment is exec, or when the first segment is
+// containers and a later segment is exactly exec; a name that only contains
+// exec routes normally. POST /containers/create and POST /images/create match
+// only with exactly two segments. Rows mirror the exec* and create* runs in
+// spec/router.qnt.
+func TestRouteExecAndExactEndpoints(t *testing.T) {
+	m := newTestManager(t, map[string]string{
+		"beacon.yaml": `
+service_name: beacon
+allowed_image_prefixes:
+  - chainsafe/lodestar
+`,
+	})
+	r := NewRouter(m)
+	createBody := map[string]interface{}{"Image": "chainsafe/lodestar:next"}
+	pullBody := map[string]interface{}{"fromImage": "chainsafe/lodestar:next"}
+
+	tests := []struct {
+		method  string
+		path    string
+		body    map[string]interface{}
+		want    Action
+		wantMsg string
+	}{
+		// execSubpathDeleteDeniedTest (#49)
+		{"DELETE", "/containers/mycontainer/exec", nil, ActionDeny, "exec is not allowed"},
+		// execSubpathPostDeniedTest (#49)
+		{"POST", "/containers/mycontainer/exec", nil, ActionDeny, "exec is not allowed"},
+		// execPrefixNameStartAllowedTest (#49): an unknown container.
+		{"POST", "/containers/exec-runner/start", nil, ActionAllow, ""},
+		// execPrefixNameDeleteAllowedTest (#49): an unknown container.
+		{"DELETE", "/containers/exec-runner", nil, ActionAllow, ""},
+		// execPrefixNameGetAllowedTest (#49)
+		{"GET", "/containers/exec-runner/json", nil, ActionAllow, ""},
+		// execNamespaceGetDeniedTest (#49): exec inspect leaks command lines.
+		{"GET", "/exec/abc/json", nil, ActionDeny, "exec is not allowed"},
+		// execNamespacePostDeniedTest (#49)
+		{"POST", "/exec/abc/start", nil, ActionDeny, "exec is not allowed"},
+		// createSubpathDeniedTest (#49): an allowed image, so only the path decides.
+		{"POST", "/containers/create/extra", createBody, ActionDeny, ""},
+		// Exec is matched under containers or exec only (#49, language-only).
+		{"GET", "/images/exec", nil, ActionAllow, ""},
+		// An allowed image, so only the path decides (#49, language-only).
+		{"POST", "/images/create/extra", pullBody, ActionDeny, ""},
+		// A name ending in exec is a plain name (#49, language-only).
+		{"GET", "/containers/myexec/json", nil, ActionAllow, ""},
+		// A name starting with exec is a plain name (#49, language-only).
+		{"DELETE", "/containers/executor", nil, ActionAllow, ""},
+	}
+	for _, tt := range tests {
+		t.Run(tt.method+" "+tt.path, func(t *testing.T) {
+			got := r.Route(tt.method, tt.path, tt.body)
+			if got.Action != tt.want {
+				t.Fatalf("Route(%s, %s) = %v, want %v (deny msg: %q)",
+					tt.method, tt.path, got.Action, tt.want, got.DenyMsg)
+			}
+			// Exact match: the default deny for POST /containers/x/exec ends in
+			// "exec is not allowed" too, so a substring check passes vacuously.
+			if tt.wantMsg != "" && got.DenyMsg != tt.wantMsg {
+				t.Fatalf("Route(%s, %s) deny msg = %q, want %q",
+					tt.method, tt.path, got.DenyMsg, tt.wantMsg)
+			}
+		})
+	}
+}
+
 func TestExtractContainerNameSkipsEmptySegment(t *testing.T) {
 	for _, path := range []string{"/containers/", "/containers//start"} {
 		if got := extractContainerName(path); got != "" {
diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs
index c4fa623..03a587f 100644
--- a/rs/src/proxy.rs
+++ b/rs/src/proxy.rs
@@ -634,6 +634,58 @@ mod tests {
         }
     }
 
+    /// Cross-language parity guard for #49. Exec and create are matched on
+    /// whole path segments. Exec is denied for every method when the first
+    /// segment is exec, or when the first segment is containers and a later
+    /// segment is exactly exec; a name that only contains exec routes
+    /// normally. POST /containers/create and POST /images/create match only
+    /// with exactly two segments. Rows mirror the exec* and create* runs in
+    /// spec/router.qnt.
+    #[test]
+    fn test_route_exec_and_exact_endpoints() {
+        let router = Router::new(make_manager(vec!["alpine"]));
+        let create_body: HashMap<String, serde_json::Value> =
+            serde_json::from_value(serde_json::json!({"Image": "alpine:latest"})).unwrap();
+        let pull_body: HashMap<String, serde_json::Value> =
+            serde_json::from_value(serde_json::json!({"fromImage": "alpine:latest"})).unwrap();
+        let exec = Some("exec is not allowed");
+        let cases = [
+            // execSubpathDeleteDeniedTest (#49)
+            ("DELETE", "/containers/mycontainer/exec", None, Action::Deny, exec),
+            // execSubpathPostDeniedTest (#49)
+            ("POST", "/containers/mycontainer/exec", None, Action::Deny, exec),
+            // execPrefixNameStartAllowedTest (#49): an unknown container.
+            ("POST", "/containers/exec-runner/start", None, Action::Allow, None),
+            // execPrefixNameDeleteAllowedTest (#49): an unknown container.
+            ("DELETE", "/containers/exec-runner", None, Action::Allow, None),
+            // execPrefixNameGetAllowedTest (#49)
+            ("GET", "/containers/exec-runner/json", None, Action::Allow, None),
+            // execNamespaceGetDeniedTest (#49): exec inspect leaks command lines.
+            ("GET", "/exec/abc/json", None, Action::Deny, exec),
+            // execNamespacePostDeniedTest (#49)
+            ("POST", "/exec/abc/start", None, Action::Deny, exec),
+            // createSubpathDeniedTest (#49): an allowed image, so only the path decides.
+            ("POST", "/containers/create/extra", Some(&create_body), Action::Deny, None),
+            // Exec is matched under containers or exec only (#49, language-only).
+            ("GET", "/images/exec", None, Action::Allow, None),
+            // An allowed image, so only the path decides (#49, language-only).
+            ("POST", "/images/create/extra", Some(&pull_body), Action::Deny, None),
+            // A name ending in exec is a plain name (#49, language-only).
+            ("GET", "/containers/myexec/json", None, Action::Allow, None),
+            // A name starting with exec is a plain name (#49, language-only).
+            ("DELETE", "/containers/executor", None, Action::Allow, None),
+        ];
+        for (method, path, body, want, want_msg) in cases {
+            let got = router.route(method, path, body);
+            assert_eq!(got.action, want, "route({} {}) deny msg = {:?}", method, path, got.deny_msg);
+            // Exact match: the default deny for POST /containers/x/exec ends in
+            // "exec is not allowed" too, so a substring check passes vacuously.
+            if let Some(want_msg) = want_msg {
+                assert_eq!(got.deny_msg.as_deref(), Some(want_msg), "route({} {})", method, path);
+            }
+        }
+    }
+
     #[test]
     fn test_extract_container_name_skips_empty_segment() {
         for path in ["/containers/", "/containers//start"] {
diff --git a/ts/src/proxy.test.ts b/ts/src/proxy.test.ts
index ed06dfd..0aad535 100644
--- a/ts/src/proxy.test.ts
+++ b/ts/src/proxy.test.ts
@@ -319,4 +319,51 @@ describe("Router", () => {
       }
     }
   });
+
+  // Cross-language parity guard for #49. Exec and create are matched on whole
+  // path segments. Exec is denied for every method when the first segment is
+  // exec, or when the first segment is containers and a later segment is
+  // exactly exec; a name that only contains exec routes normally.
+  // POST /containers/create and POST /images/create match only with exactly
+  // two segments. Rows mirror the exec* and create* runs in spec/router.qnt.
+  it("matches exec and create endpoints on whole path segments", () => {
+    const createBody = { Image: "nginx:latest" };
+    const pullBody = { fromImage: "nginx:latest" };
+    const exec = "exec is not allowed";
+    const cases: [string, string, Record<string, unknown> | undefined, Action, string | undefined][] = [
+      // execSubpathDeleteDeniedTest (#49)
+      ["DELETE", "/containers/mycontainer/exec", undefined, Action.Deny, exec],
+      // execSubpathPostDeniedTest (#49)
+      ["POST", "/containers/mycontainer/exec", undefined, Action.Deny, exec],
+      // execPrefixNameStartAllowedTest (#49): an unknown container.
+      ["POST", "/containers/exec-runner/start", undefined, Action.Allow, undefined],
+      // execPrefixNameDeleteAllowedTest (#49): an unknown container.
+      ["DELETE", "/containers/exec-runner", undefined, Action.Allow, undefined],
+      // execPrefixNameGetAllowedTest (#49)
+      ["GET", "/containers/exec-runner/json", undefined, Action.Allow, undefined],
+      // execNamespaceGetDeniedTest (#49): exec inspect leaks command lines.
+      ["GET", "/exec/abc/json", undefined, Action.Deny, exec],
+      // execNamespacePostDeniedTest (#49)
+      ["POST", "/exec/abc/start", undefined, Action.Deny, exec],
+      // createSubpathDeniedTest (#49): an allowed image, so only the path decides.
+      ["POST", "/containers/create/extra", createBody, Action.Deny, undefined],
+      // Exec is matched under containers or exec only (#49, language-only).
+      ["GET", "/images/exec", undefined, Action.Allow, undefined],
+      // An allowed image, so only the path decides (#49, language-only).
+      ["POST", "/images/create/extra", pullBody, Action.Deny, undefined],
+      // A name ending in exec is a plain name (#49, language-only).
+      ["GET", "/containers/myexec/json", undefined, Action.Allow, undefined],
+      // A name starting with exec is a plain name (#49, language-only).
+      ["DELETE", "/containers/executor", undefined, Action.Allow, undefined],
+    ];
+    for (const [method, path, body, want, wantMsg] of cases) {
+      const r = router.route(method, path, body);
+      assert.equal(r.action, want, `route(${method} ${path}) deny msg = ${JSON.stringify(r.denyMsg)}`);
+      // Exact match: the default deny for POST /containers/x/exec ends in
+      // "exec is not allowed" too, so a substring check passes vacuously.
+      if (wantMsg !== undefined) {
+        assert.equal(r.denyMsg, wantMsg, `route(${method} ${path})`);
+      }
+    }
+  });
 });

From 7ae6d5d055bdf58e92e810e4bfdb17ccdcb40bc3 Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 08:36:12 -0400
Subject: [PATCH 4/8] test: pin the reserved exec name and a top-level exec
 prefix (#49)

---
 go/internal/proxy/router_test.go | 29 +++++++++++++++++++----------
 rs/src/proxy.rs                  | 23 +++++++++++++++--------
 ts/src/proxy.test.ts             | 13 ++++++++++---
 3 files changed, 44 insertions(+), 21 deletions(-)

diff --git a/go/internal/proxy/router_test.go b/go/internal/proxy/router_test.go
index 3475e77..c819e37 100644
--- a/go/internal/proxy/router_test.go
+++ b/go/internal/proxy/router_test.go
@@ -316,26 +316,27 @@ allowed_image_prefixes:
 	r := NewRouter(m)
 
 	tests := []struct {
-		method string
-		path   string
-		want   Action
+		method  string
+		path    string
+		want    Action
+		wantMsg string
 	}{
 		// Reserved: must not be mistaken for a container to remove.
 		// reservedJsonDeleteDeniedTest
-		{"DELETE", "/containers/json", ActionDeny},
+		{"DELETE", "/containers/json", ActionDeny, ""},
 		// reservedCreateDeleteDeniedTest
-		{"DELETE", "/containers/create", ActionDeny},
+		{"DELETE", "/containers/create", ActionDeny, ""},
 		// reservedExecDeleteDeniedTest: denied by the exec check, before the lifecycle branch.
-		{"DELETE", "/containers/exec", ActionDeny},
+		{"DELETE", "/containers/exec", ActionDeny, "exec is not allowed"},
 		// Listing and inspecting stay allowed via the GET/HEAD passthrough.
-		{"GET", "/containers/json", ActionAllow},
+		{"GET", "/containers/json", ActionAllow, ""},
 		// A real container name is still routed as a container.
 		// realNameDeleteAllowedTest
-		{"DELETE", "/containers/mycontainer", ActionAllow},
-		{"GET", "/containers/mycontainer", ActionAllow},
+		{"DELETE", "/containers/mycontainer", ActionAllow, ""},
+		{"GET", "/containers/mycontainer", ActionAllow, ""},
 		// The reserved word as a *sub*-resource is a normal inspect.
 		// reservedInSubpathAllowedTest
-		{"GET", "/containers/mycontainer/json", ActionAllow},
+		{"GET", "/containers/mycontainer/json", ActionAllow, ""},
 	}
 	for _, tt := range tests {
 		t.Run(tt.method+" "+tt.path, func(t *testing.T) {
@@ -344,6 +345,10 @@ allowed_image_prefixes:
 				t.Fatalf("Route(%s, %s) = %v, want %v (deny msg: %q)",
 					tt.method, tt.path, got.Action, tt.want, got.DenyMsg)
 			}
+			if tt.wantMsg != "" && got.DenyMsg != tt.wantMsg {
+				t.Fatalf("Route(%s, %s) deny msg = %q, want %q",
+					tt.method, tt.path, got.DenyMsg, tt.wantMsg)
+			}
 		})
 	}
 }
@@ -581,6 +586,10 @@ allowed_image_prefixes:
 		{"GET", "/containers/myexec/json", nil, ActionAllow, ""},
 		// A name starting with exec is a plain name (#49, language-only).
 		{"DELETE", "/containers/executor", nil, ActionAllow, ""},
+		// The reserved name, decided by the exec check (#49, language-only).
+		{"GET", "/containers/exec/json", nil, ActionDeny, "exec is not allowed"},
+		// A top-level name starting with exec is not the exec namespace (#49, language-only).
+		{"GET", "/executor", nil, ActionAllow, ""},
 	}
 	for _, tt := range tests {
 		t.Run(tt.method+" "+tt.path, func(t *testing.T) {
diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs
index 03a587f..e4faa62 100644
--- a/rs/src/proxy.rs
+++ b/rs/src/proxy.rs
@@ -477,24 +477,27 @@ mod tests {
         let cases = [
             // Reserved: must not be mistaken for a container to remove.
             // reservedJsonDeleteDeniedTest
-            ("DELETE", "/containers/json", Action::Deny),
+            ("DELETE", "/containers/json", Action::Deny, None),
             // reservedCreateDeleteDeniedTest
-            ("DELETE", "/containers/create", Action::Deny),
+            ("DELETE", "/containers/create", Action::Deny, None),
             // reservedExecDeleteDeniedTest: denied by the exec check, before the lifecycle branch.
-            ("DELETE", "/containers/exec", Action::Deny),
+            ("DELETE", "/containers/exec", Action::Deny, Some("exec is not allowed")),
             // Listing stays allowed, via the GET/HEAD passthrough.
-            ("GET", "/containers/json", Action::Allow),
+            ("GET", "/containers/json", Action::Allow, None),
             // A real container name is still routed as a container.
             // realNameDeleteAllowedTest
-            ("DELETE", "/containers/mycontainer", Action::Allow),
-            ("GET", "/containers/mycontainer", Action::Allow),
+            ("DELETE", "/containers/mycontainer", Action::Allow, None),
+            ("GET", "/containers/mycontainer", Action::Allow, None),
             // Reserved words are only reserved in the name position.
             // reservedInSubpathAllowedTest
-            ("GET", "/containers/mycontainer/json", Action::Allow),
+            ("GET", "/containers/mycontainer/json", Action::Allow, None),
         ];
-        for (method, path, want) in cases {
+        for (method, path, want, want_msg) in cases {
             let got = router.route(method, path, None);
             assert_eq!(got.action, want, "route({} {})", method, path);
+            if let Some(want_msg) = want_msg {
+                assert_eq!(got.deny_msg.as_deref(), Some(want_msg), "route({} {})", method, path);
+            }
         }
     }
 
@@ -674,6 +677,10 @@ mod tests {
             ("GET", "/containers/myexec/json", None, Action::Allow, None),
             // A name starting with exec is a plain name (#49, language-only).
             ("DELETE", "/containers/executor", None, Action::Allow, None),
+            // The reserved name, decided by the exec check (#49, language-only).
+            ("GET", "/containers/exec/json", None, Action::Deny, exec),
+            // A top-level name starting with exec is not the exec namespace (#49, language-only).
+            ("GET", "/executor", None, Action::Allow, None),
         ];
         for (method, path, body, want, want_msg) in cases {
             let got = router.route(method, path, body);
diff --git a/ts/src/proxy.test.ts b/ts/src/proxy.test.ts
index 0aad535..80187ec 100644
--- a/ts/src/proxy.test.ts
+++ b/ts/src/proxy.test.ts
@@ -182,14 +182,14 @@ describe("Router", () => {
   // lifecycle path, where an unknown container is allowed through — Go allowed
   // DELETE /containers/json for exactly that reason.
   it("does not treat reserved path segments as container names", () => {
-    const cases: [string, string, Action][] = [
+    const cases: [string, string, Action, string?][] = [
       // Reserved: must not be mistaken for a container to remove.
       // reservedJsonDeleteDeniedTest
       ["DELETE", "/containers/json", Action.Deny],
       // reservedCreateDeleteDeniedTest
       ["DELETE", "/containers/create", Action.Deny],
       // reservedExecDeleteDeniedTest: denied by the exec check, before the lifecycle branch.
-      ["DELETE", "/containers/exec", Action.Deny],
+      ["DELETE", "/containers/exec", Action.Deny, "exec is not allowed"],
       // Listing stays allowed, via the GET/HEAD passthrough.
       ["GET", "/containers/json", Action.Allow],
       // A real container name is still routed as a container.
@@ -200,9 +200,12 @@ describe("Router", () => {
       // reservedInSubpathAllowedTest
       ["GET", "/containers/mycontainer/json", Action.Allow],
     ];
-    for (const [method, path, want] of cases) {
+    for (const [method, path, want, wantMsg] of cases) {
       const r = router.route(method, path);
       assert.equal(r.action, want, `route(${method} ${path})`);
+      if (wantMsg !== undefined) {
+        assert.equal(r.denyMsg, wantMsg, `route(${method} ${path})`);
+      }
     }
   });
 
@@ -355,6 +358,10 @@ describe("Router", () => {
       ["GET", "/containers/myexec/json", undefined, Action.Allow, undefined],
       // A name starting with exec is a plain name (#49, language-only).
       ["DELETE", "/containers/executor", undefined, Action.Allow, undefined],
+      // The reserved name, decided by the exec check (#49, language-only).
+      ["GET", "/containers/exec/json", undefined, Action.Deny, exec],
+      // A top-level name starting with exec is not the exec namespace (#49, language-only).
+      ["GET", "/executor", undefined, Action.Allow, undefined],
     ];
     for (const [method, path, body, want, wantMsg] of cases) {
       const r = router.route(method, path, body);

From 5504a6ddef7074e26fd155cb093da6978b425861 Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 08:54:44 -0400
Subject: [PATCH 5/8] fix: match exec and create endpoints on whole path
 segments (#49)

---
 README.md                   |  7 +++++--
 go/internal/proxy/router.go | 18 ++++++++----------
 rs/src/proxy.rs             | 12 +++++++++++-
 ts/src/proxy.ts             |  8 +++++++-
 4 files changed, 31 insertions(+), 14 deletions(-)

diff --git a/README.md b/README.md
index 3546af2..4cd4d2d 100644
--- a/README.md
+++ b/README.md
@@ -208,17 +208,20 @@ docker pull attacker/malware:latest  # denied: image not in allowlist
 | POST | `/containers/create` | Validated by middleware chain |
 | POST | `/containers/{name}/start\|stop\|restart\|kill\|wait\|pause\|unpause` | Allowed on known containers |
 | DELETE | `/containers/{name}` | Allowed on known containers |
-| POST | `/containers/{name}/exec` | **DENIED** |
+| Any | `/containers/{name}/exec` | **DENIED** |
+| Any | `/exec/*` | **DENIED** |
 | POST | `/containers/{name}/rename\|update` | **DENIED** |
 | POST | `/images/create` | Validated by registry gate |
 | POST | `/auth` | **DENIED** |
 | POST | `/build` | **DENIED** |
 | POST | `/commit` | **DENIED** |
-| GET/HEAD | Any path without `%` | Allowed (read-only) |
+| GET/HEAD | Any other path without `%` | Allowed (read-only) |
 | Other | Other | **DENIED** |
 
 Any request whose path contains a percent-encoded byte (`%`) is denied with 403 for every method, GET and HEAD included, because the daemon decodes the path before routing. The query string is not inspected, so filters such as `docker ps --filter …` still work. The Go implementation also denies paths that contain raw characters it must re-encode, such as non-ASCII bytes or `{`; the Docker CLI never sends these. A consequence is that networks whose names need percent-encoding (for example a space or `%`) cannot be inspected by name through the proxy; inspecting them by ID still works, and other network operations are denied regardless.
 
+Exec is matched on whole path segments, so containers named like `exec-runner` work normally, and exec inspect (`GET /exec/{id}/json`) is denied too.
+
 ## Configuration
 
 ### CLI Flags
diff --git a/go/internal/proxy/router.go b/go/internal/proxy/router.go
index 7be33a7..3d4414a 100644
--- a/go/internal/proxy/router.go
+++ b/go/internal/proxy/router.go
@@ -2,6 +2,7 @@ package proxy
 
 import (
 	"fmt"
+	"slices"
 	"strings"
 
 	"github.com/ChainSafe/docker-socket-policy/go/internal/policy"
@@ -49,7 +50,7 @@ func (r *Router) Route(method, path string, body map[string]interface{}) *RouteR
 		return &RouteResult{Action: ActionDeny, DenyMsg: "auth endpoint is not allowed"}
 	}
 
-	if matchEndpoint(path, "containers", "exec") {
+	if isExecPath(path) {
 		return &RouteResult{Action: ActionDeny, DenyMsg: "exec is not allowed"}
 	}
 
@@ -61,7 +62,7 @@ func (r *Router) Route(method, path string, body map[string]interface{}) *RouteR
 		return &RouteResult{Action: ActionDeny, DenyMsg: "commit is not allowed"}
 	}
 
-	if matchEndpoint(path, "containers", "create") && method == "POST" {
+	if path == "/containers/create" && method == "POST" {
 		return r.routeCreate(body)
 	}
 
@@ -94,7 +95,7 @@ func (r *Router) Route(method, path string, body map[string]interface{}) *RouteR
 		}
 	}
 
-	if matchEndpoint(path, "images", "create") && method == "POST" {
+	if path == "/images/create" && method == "POST" {
 		return r.routeImagePull(body)
 	}
 
@@ -192,13 +193,10 @@ func scanDigits(s string, i int) int {
 	return i
 }
 
-func matchEndpoint(path, resource, endpoint string) bool {
-	path = strings.TrimPrefix(path, "/")
-	parts := strings.SplitN(path, "/", 3)
-	if len(parts) < 2 {
-		return false
-	}
-	return parts[0] == resource && parts[1] == endpoint
+// isExecPath matches exec on whole segments, so a name like exec-runner is not exec (#49).
+func isExecPath(path string) bool {
+	segs := strings.Split(strings.TrimPrefix(path, "/"), "/")
+	return segs[0] == "exec" || segs[0] == "containers" && slices.Contains(segs[1:], "exec")
 }
 
 // reservedContainerSegments are Docker endpoints that sit where a container
diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs
index e4faa62..888fcbd 100644
--- a/rs/src/proxy.rs
+++ b/rs/src/proxy.rs
@@ -58,7 +58,7 @@ impl Router {
         if path.starts_with("/auth") {
             return deny("auth endpoint is not allowed");
         }
-        if path == "/containers/exec" || path.starts_with("/containers/") && path.contains("/exec") {
+        if is_exec_path(path) {
             return deny("exec is not allowed");
         }
         if path.starts_with("/build") {
@@ -232,6 +232,16 @@ fn strip_api_version(path: &str) -> &str {
     path
 }
 
+// Exec is matched on whole segments, so a name like exec-runner is not exec (#49).
+fn is_exec_path(path: &str) -> bool {
+    let mut segs = path.strip_prefix('/').unwrap_or(path).split('/');
+    match segs.next() {
+        Some("exec") => true,
+        Some("containers") => segs.any(|s| s == "exec"),
+        _ => false,
+    }
+}
+
 fn extract_container_name(path: &str) -> Option<&str> {
     let path = path.strip_prefix('/').unwrap_or(path);
     let parts: Vec<&str> = path.split('/').collect();
diff --git a/ts/src/proxy.ts b/ts/src/proxy.ts
index 743049f..1f321af 100644
--- a/ts/src/proxy.ts
+++ b/ts/src/proxy.ts
@@ -34,7 +34,7 @@ export class Router {
 
     // Denied endpoints
     if (path.startsWith("/auth")) return { action: Action.Deny, denyMsg: "auth endpoint is not allowed" };
-    if (path.includes("/exec")) return { action: Action.Deny, denyMsg: "exec is not allowed" };
+    if (isExecPath(path)) return { action: Action.Deny, denyMsg: "exec is not allowed" };
     if (path.startsWith("/build")) return { action: Action.Deny, denyMsg: "build is not allowed" };
     if (path.startsWith("/commit")) return { action: Action.Deny, denyMsg: "commit is not allowed" };
 
@@ -123,6 +123,12 @@ function stripAPIVersion(path: string): string {
   return match ? path.slice(match[0].length - 1) : path;
 }
 
+// Exec is matched on whole segments, so a name like exec-runner is not exec (#49).
+function isExecPath(path: string): boolean {
+  const [first, ...rest] = path.replace(/^\//, "").split("/");
+  return first === "exec" || (first === "containers" && rest.includes("exec"));
+}
+
 function extractContainerName(path: string): string | undefined {
   const parts = path.replace(/^\//, "").split("/");
   if (parts[0] === "containers" && parts[1] && !["create", "json", "exec"].includes(parts[1])) {

From 5a7ffe25286c6bcb4a3641537a935e973574c2a8 Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 08:54:45 -0400
Subject: [PATCH 6/8] docs: update test coverage counts (#49)

---
 AGENTS.md | 10 +++++-----
 README.md |  6 +++---
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/AGENTS.md b/AGENTS.md
index eacc1f4..5fae961 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -37,17 +37,17 @@ deploy/ — Docker Compose + integration tests
 - Zero external deps where possible (Go: yaml.v3, Rust: tokio/hyper/serde/clap, TS: yaml)
 
 ## Test Coverage
-- Go: 107 unit tests (main/listener: 24, policy: 10, middleware: 29, proxy: 40, audit: 4)
-- Rust: 144 unit tests (main/listener: 23, policy: 15, middleware: 50, proxy: 43, handler: 7, audit: 4, transport: 2)
-- TypeScript: 161 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 41, proxy: 30, policy: 10, handler: 9, shutdown: 5, transport: 5, audit: 4)
-- Integration, per implementation: 39 tests via deploy/test.sh and 15 socket tests via deploy/test-sock.sh (docker-compose)
+- Go: 108 unit tests (main/listener: 24, policy: 10, middleware: 29, proxy: 41, audit: 4)
+- Rust: 145 unit tests (main/listener: 23, policy: 15, middleware: 50, proxy: 44, handler: 7, audit: 4, transport: 2)
+- TypeScript: 162 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 41, proxy: 31, policy: 10, handler: 9, shutdown: 5, transport: 5, audit: 4)
+- Integration, per implementation: 43 tests via deploy/test.sh and 15 socket tests via deploy/test-sock.sh (docker-compose)
 - Quint: `make test-spec` runs the `spec/listener.qnt` `run` tests (instances `listener_locked`, `listener_unlocked`) and the `spec/router.qnt` `run` tests (instances `router`, `router_pre48`, `router_pre53`)
 
 ## Test Conventions
 - Go: stdlib `testing` package, `go test ./...`
 - Rust: `#[cfg(test)]` inline modules, `cargo test`
 - TypeScript: `node:test` framework, `npm run build && node --test dist/*.test.js`
-- Integration: `make test-integration` (39 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
+- Integration: `make test-integration` (43 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
 
 ## Contribution Workflow
 
diff --git a/README.md b/README.md
index 4cd4d2d..5d8a7d5 100644
--- a/README.md
+++ b/README.md
@@ -100,9 +100,9 @@ All three implementations expose the same API surface, share the same [Quint spe
 
 | Language | Directory | Tests | Stack |
 |----------|-----------|-------|-------|
-| Go | [go/](go/) | 107 unit + 39 integration | stdlib net/http + yaml.v3 |
-| Rust | [rs/](rs/) | 144 unit | tokio, hyper, serde, clap |
-| TypeScript | [ts/](ts/) | 161 unit (1 skipped) | Node 22 ESM, built-in http |
+| Go | [go/](go/) | 108 unit + 43 integration | stdlib net/http + yaml.v3 |
+| Rust | [rs/](rs/) | 145 unit | tokio, hyper, serde, clap |
+| TypeScript | [ts/](ts/) | 162 unit (1 skipped) | Node 22 ESM, built-in http |
 
 ### Build All
 

From 90da0b4d5921425a725210e65e214a48ce600aea Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 15:10:44 -0400
Subject: [PATCH 7/8] spec: clarify the #49 history note (#49)

---
 spec/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/README.md b/spec/README.md
index eaf322a..d18a2c1 100644
--- a/spec/README.md
+++ b/spec/README.md
@@ -147,7 +147,7 @@ Two invariants are structurally tautological within the Quint model — they can
 - **GET is covered.** The percent check runs before the GET passthrough, and `routerSeesWhatDaemonSees` ranges over `GET` as well as `POST` and `DELETE`. On `router_pre53` the passthrough lets `GET /containers/%2F` through, and the property fails for it too.
 - **No instance models Go before #53.** Go decoded before routing, which is `route(m, decodePath(segs))`. With this table that agrees with the daemon by construction, so `routerSeesWhatDaemonSees` cannot express Go's risk: decoding that differs from the daemon's, such as encoded version segments ([#57](https://github.com/ChainSafe/docker-socket-policy/issues/57)). Go's change is covered by the language handler tests.
 - **`router.qnt` is not the full router.** `route` models the percent check, which runs first in all three routers, the exec check, the exact `POST /containers/create` route and the container-lifecycle branch, in that order. It leaves out the API-version strip and the other checks that the routers run before the lifecycle branch, such as the read-only endpoints, auth, and the build and commit denials, as well as `POST /images/create` and the endpoints after the lifecycle branch. For paths that those checks catch, the model's outcome can differ from what an implementation does: `GET /build` is `allowRead` in the model, for example, while the routers deny it as `build is not allowed`. The `images` rows of #49 (`GET /images/exec` allowed, `POST /images/create/extra` denied) are therefore language-only rows, as are `GET /containers/myexec/json` and `DELETE /containers/executor`: the model's words are atoms, so it cannot express a name that merely contains `exec`. Only the properties and the table rows are claims about the code.
-- **Exec and create match whole segments (#49).** Before #49 the routers disagreed: Go matched `exec` only in the name position (`/containers/exec`), so `DELETE /containers/mycontainer/exec` went down the lifecycle branch and was allowed. Rust matched the substring `/exec` anywhere after `/containers/`, so both Go and Rust let `GET /exec/<id>/json` through the GET passthrough; and TypeScript anywhere in the path, so both also denied containers named `exec-runner` or `executor`. Go also accepted `POST /containers/create/extra` as a container create. In the model the exec check runs before the create route, the lifecycle branch and the GET passthrough, so it denies every method, GET included: exec inspect shows the full command line. `reservedExecDeleteDenied` (`DELETE /containers/exec`) is decided by the exec check, as in all three implementations, and now asserts `denyExec`. `exec` stays in the reserved set, but no row, in the model or in the language tests, would catch it being dropped from there.
+- **Exec and create match whole segments (#49).** Before #49 the routers disagreed: Go matched `exec` only in the name position (`/containers/exec`), so `DELETE /containers/mycontainer/exec` went down the lifecycle branch and was allowed. Rust matched the substring `/exec` anywhere after `/containers/`, and TypeScript anywhere in the path, so Rust and TypeScript denied containers named `exec-runner` or `executor`. Neither Go nor Rust checked the `/exec/…` namespace, so both let `GET /exec/<id>/json` through the GET passthrough. Go also accepted `POST /containers/create/extra` as a container create. In the model the exec check runs before the create route, the lifecycle branch and the GET passthrough, so it denies every method, GET included: exec inspect shows the full command line. `reservedExecDeleteDenied` (`DELETE /containers/exec`) is decided by the exec check, as in all three implementations, and now asserts `denyExec`. `exec` stays in the reserved set, but no row, in the model or in the language tests, would catch it being dropped from there.
 - **The #49 properties are not vacuous.** None of them is shown on a separate instance; replacing the rule in `route` makes them fail. With a substring-style rule (a segment that starts with `exec`, modeled as the set `exec`, `exec-runner`), `execPrefixSoundTest` and the three `execPrefixName*Allowed` rows fail. With Go's rule before #49 (`exec` only as the second segment under `containers`), `execSoundTest` and the four `exec*Denied` rows fail. `execSubpathPostDenied` and `execNamespacePostDenied` fail there only because the outcome is the default `deny`, not `denyExec`: the request is still refused, as before #49, but not by the exec check. With Go's prefix match for create, `createExactSoundTest` and `createSubpathDenied` fail. `execNeverAllowed` writes out the exec positions itself instead of calling `isExecPath`, so that a narrower `isExecPath` cannot narrow the property with it.
 - **HEAD is outside the model.** `METHODS` is `GET`, `POST`, `DELETE`. The real lifecycle branches agree on those three methods only. For `HEAD /containers/x`, Go and TypeScript fall through to the GET/HEAD passthrough and allow it. Rust denies it in the lifecycle branch.
 - **Listener fault bias.** `step` crashes an instance on 1 in 10 draws instead of half of all steps, so random runs actually interleave live instances. Every crash stays reachable from every phase, so the reachable state space is unchanged.

From cc9be7655083e1b64586977face70bbf7245d078 Mon Sep 17 00:00:00 2001
From: Adrian Bienkowski <adrian@chainsafe.io>
Date: Thu, 8 Oct 2026 15:11:18 -0400
Subject: [PATCH 8/8] refactor: parenthesise the Go exec check; exact README
 exec row (#49)

---
 README.md                   | 2 +-
 go/internal/proxy/router.go | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 5d8a7d5..3ee179e 100644
--- a/README.md
+++ b/README.md
@@ -208,7 +208,7 @@ docker pull attacker/malware:latest  # denied: image not in allowlist
 | POST | `/containers/create` | Validated by middleware chain |
 | POST | `/containers/{name}/start\|stop\|restart\|kill\|wait\|pause\|unpause` | Allowed on known containers |
 | DELETE | `/containers/{name}` | Allowed on known containers |
-| Any | `/containers/{name}/exec` | **DENIED** |
+| Any | `/containers/…/exec` (an `exec` segment anywhere under `/containers`) | **DENIED** |
 | Any | `/exec/*` | **DENIED** |
 | POST | `/containers/{name}/rename\|update` | **DENIED** |
 | POST | `/images/create` | Validated by registry gate |
diff --git a/go/internal/proxy/router.go b/go/internal/proxy/router.go
index 3d4414a..8ad03b9 100644
--- a/go/internal/proxy/router.go
+++ b/go/internal/proxy/router.go
@@ -196,7 +196,7 @@ func scanDigits(s string, i int) int {
 // isExecPath matches exec on whole segments, so a name like exec-runner is not exec (#49).
 func isExecPath(path string) bool {
 	segs := strings.Split(strings.TrimPrefix(path, "/"), "/")
-	return segs[0] == "exec" || segs[0] == "containers" && slices.Contains(segs[1:], "exec")
+	return segs[0] == "exec" || (segs[0] == "containers" && slices.Contains(segs[1:], "exec"))
 }
 
 // reservedContainerSegments are Docker endpoints that sit where a container