fix(rs): an empty path segment is not a container name

AGENTS.md

@@ -19,7 +19,7 @@ deploy/ — Docker Compose + integration tests
 - `make build-rs` / `make test-rs` / `make lint-rs` — Rust only
 - `make build-ts` / `make test-ts` / `make lint-ts` — TypeScript only
 - `make verify` — Quint spec simulation (request handling + listener)
-- `make test-spec` — Quint `run` tests for `spec/listener.qnt`
+- `make test-spec` — Quint `run` tests for `spec/listener.qnt` and `spec/router.qnt`
 - `make test-integration` — Docker Compose integration tests
 - `make test-integration-sock` — listening-socket integration tests (`IMPL=rs|ts` for the others)
 
@@ -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: 99 unit tests (main/listener: 23, policy: 10, middleware: 29, proxy: 33, audit: 4)
-- Rust: 137 unit tests (main/listener: 23, policy: 15, middleware: 50, proxy: 39, handler: 4, audit: 4, transport: 2)
-- TypeScript: 155 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 41, proxy: 27, policy: 10, handler: 6, shutdown: 5, transport: 5, audit: 4)
-- Integration, per implementation: 30 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
+- Go: 101 unit tests (main/listener: 23, policy: 10, middleware: 29, proxy: 35, audit: 4)
+- Rust: 139 unit tests (main/listener: 23, policy: 15, middleware: 50, proxy: 41, handler: 4, audit: 4, transport: 2)
+- TypeScript: 156 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 41, proxy: 28, policy: 10, handler: 6, shutdown: 5, transport: 5, audit: 4)
+- Integration, per implementation: 32 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`)
 
 ## 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` (30 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
+- Integration: `make test-integration` (32 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
 
 ## Contribution Workflow
 

Makefile

@@ -4,6 +4,7 @@ VERSION ?= $(shell git describe --tags --always --dirty 2>/dev/null || echo dev)
 QUINT ?= $(shell command -v quint 2>/dev/null || echo node $$HOME/.hermes/node/lib/node_modules/@informalsystems/quint/dist/src/cli.js)
 SPEC ?= spec/docker_socket_policy.qnt
 LISTENER_SPEC ?= spec/listener.qnt
+ROUTER_SPEC := spec/router.qnt
 BACKEND ?=
 
 .PHONY: build clean test lint verify typecheck test-spec validate ci-verify release-verify
@@ -67,6 +68,7 @@ clean:
 typecheck:
 	$(QUINT) typecheck $(SPEC)
 	$(QUINT) typecheck $(LISTENER_SPEC)
+	$(QUINT) typecheck $(ROUTER_SPEC)
 
 verify:
 	if [ -n "$(BACKEND)" ]; then \
@@ -80,6 +82,8 @@ verify:
 test-spec:
 	$(QUINT) test $(LISTENER_SPEC) --main=listener_locked
 	$(QUINT) test $(LISTENER_SPEC) --main=listener_unlocked
+	$(QUINT) test $(ROUTER_SPEC) --main=router
+	$(QUINT) test $(ROUTER_SPEC) --main=router_pre48
 
 verify-ts:
 	$(QUINT) run $(SPEC) --max-steps=50 --invariants allInvariants --backend typescript

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/) | 74 unit + 26 integration | stdlib net/http + yaml.v3 |
-| Rust | [rs/](rs/) | 112 unit | tokio, hyper, serde, clap |
-| TypeScript | [ts/](ts/) | 108 unit | Node 22 ESM, built-in http |
+| Go | [go/](go/) | 101 unit + 32 integration | stdlib net/http + yaml.v3 |
+| Rust | [rs/](rs/) | 139 unit | tokio, hyper, serde, clap |
+| TypeScript | [ts/](ts/) | 156 unit (1 skipped) | Node 22 ESM, built-in http |
 
 ### Build All
 
@@ -363,15 +363,15 @@ group to `SupplementaryGroups=`. Otherwise startup fails with the
 
 ## Formal Verification
 
-This project includes a [Quint](https://quint-lang.org/) formal specification that models the security invariants as a state machine. Random-simulation verification runs 10,000 sampled traces of up to 100 steps each, checking all 9 invariants on every state transition. A second module, `spec/listener.qnt`, models listening-socket startup (group selection, existing-path checks, the single-instance lock) with 6 more invariants.
+This project includes a [Quint](https://quint-lang.org/) formal specification that models the security invariants as a state machine. Random-simulation verification runs 10,000 sampled traces of up to 100 steps each, checking all 9 invariants on every state transition. A second module, `spec/listener.qnt`, models listening-socket startup (group selection, existing-path checks, the single-instance lock) with 6 more invariants. A third module, `spec/router.qnt`, models container-name extraction and the router's container-lifecycle routing branch only, not the full routing table ([#24](https://github.com/ChainSafe/docker-socket-policy/issues/24), [#48](https://github.com/ChainSafe/docker-socket-policy/issues/48)).
 
 The CI pipeline runs verification on every push and PR. A violation blocks the build.
 
 ```bash
 make typecheck            # Quint type-check (proves type safety)
 make verify               # Random-simulation verification (default evaluator)
 make verify BACKEND=rust  # Same, using the faster Rust backend
-make test-spec            # Quint `run` tests for listener.qnt (one per design-table row)
+make test-spec            # Quint `run` tests for listener.qnt and router.qnt (one per table row)
 make validate             # All checks: typecheck + verify + go vet + go test
 ```
 

deploy/test.sh

@@ -315,6 +315,16 @@ check "DELETE /containers/create -> 403 (reserved, not a container)" "403" "$S"
 S=$(get_status "$PROXY/containers/json")
 check "GET /containers/json -> 200 (still the list endpoint)" "200" "$S"
 
+# Empty name segment (#48). /containers/ and /containers//start carry no
+# container name. Treating "" as a name sent the request down the lifecycle
+# path, where an unknown container is allowed through, so Rust forwarded these
+# while Go and TypeScript denied them.
+S=$(delete_status "$PROXY/containers/")
+check "DELETE /containers/ -> 403 (empty name, not a container)" "403" "$S"
+
+S=$(post_empty "$PROXY/containers//start")
+check "POST /containers//start -> 403 (empty name, not a container)" "403" "$S"
+
 # ─── Summary ──────────────────────────────────────────
 
 echo ""

go/internal/proxy/router_test.go

@@ -320,14 +320,20 @@ allowed_image_prefixes:
 		want   Action
 	}{
 		// Reserved: must not be mistaken for a container to remove.
+		// reservedJsonDeleteDeniedTest
 		{"DELETE", "/containers/json", ActionDeny},
+		// reservedCreateDeleteDeniedTest
 		{"DELETE", "/containers/create", ActionDeny},
+		// reservedExecDeleteDeniedTest: denied by the exec check, before the lifecycle branch.
+		{"DELETE", "/containers/exec", ActionDeny},
 		// Listing and inspecting stay allowed via the GET/HEAD passthrough.
 		{"GET", "/containers/json", ActionAllow},
 		// A real container name is still routed as a container.
+		// realNameDeleteAllowedTest
 		{"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},
 	}
 	for _, tt := range tests {
@@ -355,3 +361,50 @@ func TestExtractContainerNameSkipsReservedSegments(t *testing.T) {
 		t.Errorf("extractContainerName(/containers/mycontainer/json) = %q, want \"mycontainer\"", got)
 	}
 }
+
+// TestRouteEmptyContainerName is the cross-language parity guard for #48.
+//
+// An empty segment in the name position (/containers/, /containers//start) is
+// not a container name. Treating it as one routes the request down the
+// lifecycle path, where an unknown container is allowed through — Rust did
+// exactly that. Rows mirror the emptyName* runs in spec/router.qnt.
+func TestRouteEmptyContainerName(t *testing.T) {
+	m := newTestManager(t, map[string]string{
+		"beacon.yaml": `
+service_name: beacon
+allowed_image_prefixes:
+  - chainsafe/lodestar
+`,
+	})
+	r := NewRouter(m)
+
+	tests := []struct {
+		method string
+		path   string
+		want   Action
+	}{
+		// emptyNameDeleteDeniedTest
+		{"DELETE", "/containers/", ActionDeny},
+		// emptyNameStartDeniedTest
+		{"POST", "/containers//start", ActionDeny},
+		// emptyNameGetAllowedTest
+		{"GET", "/containers/", ActionAllow},
+	}
+	for _, tt := range tests {
+		t.Run(tt.method+" "+tt.path, func(t *testing.T) {
+			got := r.Route(tt.method, tt.path, nil)
+			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)
+			}
+		})
+	}
+}
+
+func TestExtractContainerNameSkipsEmptySegment(t *testing.T) {
+	for _, path := range []string{"/containers/", "/containers//start"} {
+		if got := extractContainerName(path); got != "" {
+			t.Errorf("extractContainerName(%s) = %q, want \"\"", path, got)
+		}
+	}
+}

rs/src/proxy.rs

@@ -209,7 +209,8 @@ fn strip_api_version(path: &str) -> &str {
 fn extract_container_name(path: &str) -> Option<&str> {
     let path = path.strip_prefix('/').unwrap_or(path);
     let parts: Vec<&str> = path.split('/').collect();
-    if parts.len() >= 2 && parts[0] == "containers" && parts[1] != "create" && parts[1] != "json" && parts[1] != "exec" {
+    // An empty segment is not a name, mirroring Go/TS (#48).
+    if parts.len() >= 2 && parts[0] == "containers" && !parts[1].is_empty() && parts[1] != "create" && parts[1] != "json" && parts[1] != "exec" {
         Some(parts[1])
     } else {
         None
@@ -449,14 +450,20 @@ mod tests {
         let router = Router::new(make_manager(vec!["alpine"]));
         let cases = [
             // 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),
             // Listing stays allowed, via the GET/HEAD passthrough.
             ("GET", "/containers/json", Action::Allow),
             // A real container name is still routed as a container.
+            // realNameDeleteAllowedTest
             ("DELETE", "/containers/mycontainer", Action::Allow),
             ("GET", "/containers/mycontainer", Action::Allow),
             // Reserved words are only reserved in the name position.
+            // reservedInSubpathAllowedTest
             ("GET", "/containers/mycontainer/json", Action::Allow),
         ];
         for (method, path, want) in cases {
@@ -478,6 +485,35 @@ mod tests {
         );
     }
 
+    /// Cross-language parity guard for #48. An empty segment in the name
+    /// position (/containers/, /containers//start) is not a container name.
+    /// Treating it as one routes the request down the lifecycle path, where an
+    /// unknown container is allowed through. Rows mirror the emptyName* runs
+    /// in spec/router.qnt.
+    #[test]
+    fn test_route_empty_container_name() {
+        let router = Router::new(make_manager(vec!["alpine"]));
+        let cases = [
+            // emptyNameDeleteDeniedTest
+            ("DELETE", "/containers/", Action::Deny),
+            // emptyNameStartDeniedTest
+            ("POST", "/containers//start", Action::Deny),
+            // emptyNameGetAllowedTest
+            ("GET", "/containers/", Action::Allow),
+        ];
+        for (method, path, want) in cases {
+            let got = router.route(method, path, None);
+            assert_eq!(got.action, want, "route({} {})", method, path);
+        }
+    }
+
+    #[test]
+    fn test_extract_container_name_skips_empty_segment() {
+        for path in ["/containers/", "/containers//start"] {
+            assert_eq!(extract_container_name(path), None, "{} has no container name", path);
+        }
+    }
+
     #[test]
     fn test_route_image_pull() {
         let router = Router::new(make_manager(vec!["alpine"]));

spec/README.md

@@ -9,6 +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` | Container-name extraction and the container-lifecycle branch of the router only, not the full router. One `run` test per table row. Instances `router` (the extraction rule of Go, TypeScript, and Rust after #48) and `router_pre48` (Rust's rule before #48) |
 
 ## How to Run
 
@@ -33,6 +34,11 @@ quint run spec/listener.qnt --main=listener_locked --max-steps=30 --invariant al
 quint test spec/listener.qnt --main=listener_locked
 quint test spec/listener.qnt --main=listener_unlocked
 
+# Router model: typecheck, run the table tests on both instances
+quint typecheck spec/router.qnt
+quint test spec/router.qnt --main=router
+quint test spec/router.qnt --main=router_pre48
+
 # Formal model-checking via Apalache (exhaustive, requires Java)
 quint verify --max-steps=10 --invariants allInvariants spec/docker_socket_policy.qnt
 ```
@@ -75,6 +81,23 @@ quint verify --max-steps=10 --invariants allInvariants spec/docker_socket_policy
 quint run spec/listener.qnt --main=listener_unlocked --max-steps=30 --invariant noLiveTakeover   # violation expected
 ```
 
+### Router path parsing (`router.qnt`)
+
+A path is a list of segments, so `/containers/` is `["containers", ""]` and `/containers//start` is `["containers", "", "start"]`. The second segment is a container name unless it is empty or one of `create`, `json`, `exec`. `lifecycleOnlyTargetsRealNames` checks every method in `GET`, `POST`, `DELETE` against every path of 1 to 3 segments. It holds when each lifecycle allow (`allowKnown` or `allowUnknown`) targets a non-empty, non-reserved name. `soundTest` asserts it on `router`.
+
+| Row (`run <row>Test`) | Request | Outcome | Instances |
+|-----|---------|---------|-----------|
+| `emptyNameDeleteDenied` | `DELETE /containers/` | deny | `router` |
+| `emptyNameStartDenied` | `POST /containers//start` | deny | `router` |
+| `emptyNameGetAllowed` | `GET /containers/` | allow (passthrough) | both |
+| `reservedJsonDeleteDenied` | `DELETE /containers/json` | deny | both |
+| `reservedCreateDeleteDenied` | `DELETE /containers/create` | deny | both |
+| `reservedExecDeleteDenied` | `DELETE /containers/exec` | deny | both |
+| `realNameDeleteAllowed` | `DELETE /containers/mycontainer` | allow (unknown container) | both |
+| `reservedInSubpathAllowed` | `GET /containers/mycontainer/json` | allow | both |
+
+Each implementation's router tests use the same row names in comments (added with the #48 fix). `router_pre48` runs `pre48UnsoundTest`, which asserts that the property fails and that both `emptyName*Denied` requests are allowed as an unknown container ([#48](https://github.com/ChainSafe/docker-socket-policy/issues/48)).
+
 ### Modeling Notes
 
 Two invariants are structurally tautological within the Quint model — they can't be falsified by any action sequence the simulator generates, so they don't get real coverage from `quint run`/`quint verify`:
@@ -83,6 +106,13 @@ Two invariants are structurally tautological within the Quint model — they can
 - **`routingTableComplete`** — checks that `endpointsTable` (a fixed constant) contains a fixed list of literals declared in the same file. It documents the intended routing table but doesn't cross-check it against any of the three Router implementations; that comparison has to be done manually (or via `quint-analyzer`) against `go/internal/proxy/router.go`, `rs/src/proxy.rs`, and `ts/src/proxy.ts`.
 
 - **`listener.qnt` checks the design, not the code.** Nothing in the model is derived from the Go, Rust or TypeScript sources. Conformance rests on each implementation's unit and integration tests, which carry the same names as the Quint `run`s (`groupDefaultPresent`, `pathStaleReplaced`, …) so every design-table row can be traced across all four. `raceWithoutLockTest` (in `listener_unlocked`) is the formal record of the TypeScript gap: Node has no `flock`, so two TypeScript instances starting together can orphan one another's socket ([#46](https://github.com/ChainSafe/docker-socket-policy/issues/46)).
+- **`lifecycleOnlyTargetsRealNames` is close to a tautology.** `route` only allows by name when `hasContainerName` holds, and `hasContainerName` is nearly the property itself. It is not vacuous: on `router_pre48`, where an empty segment counts as a name, the property fails, and `pre48UnsoundTest` asserts that. Most of the evidence comes from the table rows, whose names the language router tests reuse (added with the #48 fix).
+- **`router.qnt` is not the full router.** `route` models only the container-lifecycle branch. It leaves out the checks that the routers run before that branch, 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 property 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.
+- **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.
 
 ### Attack Scenarios Prevented by Invariants
@@ -167,6 +197,6 @@ Quint formal verification runs in CI via `.github/workflows/ci.yml` (quint job),
 - run: quint run --max-steps=100 --invariants allInvariants --backend typescript spec/docker_socket_policy.qnt
 ```
 
-In practice the job calls `make typecheck`, `make test-spec` and `make verify BACKEND=typescript`, which also cover `listener.qnt`.
+In practice the job calls `make typecheck`, `make test-spec` and `make verify BACKEND=typescript`, which also cover `listener.qnt` and `router.qnt`.
 
 Releases are handled by `.github/workflows/release.yml`, which auto-bumps the patch version on push to `main`, creates a draft release, builds Docker images, generates SPDX + CycloneDX SBOMs with syft, and signs them with Cosign.