From 62e8e96c7ddf3c9efde931e7065b862f41e9d8d1 Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 06:52:55 -0400 Subject: [PATCH 1/9] spec: model container-name extraction in the router (#48) --- Makefile | 4 ++ spec/README.md | 26 +++++++++- spec/router.qnt | 129 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 158 insertions(+), 1 deletion(-) create mode 100644 spec/router.qnt diff --git a/Makefile b/Makefile index 69f2c88..109e3ce 100644 --- a/Makefile +++ b/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 diff --git a/spec/README.md b/spec/README.md index 94163f9..141d16a 100644 --- a/spec/README.md +++ b/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` | Router path parsing: container-name extraction and the container-lifecycle branch, one `run` test per table row. Instances `router` (Go, TypeScript, Rust after #48) and `router_pre48` (Rust 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 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 | + +The Go, Rust and TypeScript router tests carry the same row names in comments. `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,7 @@ 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, because the language tests share their names. `router.qnt` models only the lifecycle branch. The earlier exec, build and commit denials and `POST /containers/create` are left out, so it says nothing about paths that those checks catch first. - **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 +191,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. diff --git a/spec/router.qnt b/spec/router.qnt new file mode 100644 index 0000000..99b05fe --- /dev/null +++ b/spec/router.qnt @@ -0,0 +1,129 @@ +// ─── Module: router_model ─────────────────────────────────────────────── +// +// How the router extracts a container name from a request path, and how +// the container-lifecycle branch routes on it (#48). Mirrors +// `extract_container_name` and the lifecycle branch of `Router::route` in +// rs/src/proxy.rs; Go (`extractContainerName`) and TypeScript +// (`extractContainerName`) share the lifecycle branch. +// +// A path is a list of segments: `DELETE /containers/` is +// ["containers", ""], `POST /containers//start` is ["containers", "", "start"]. +// +// ALLOW_EMPTY_NAME = true models Rust before #48, where an empty second +// segment counted as a container name. false models Go, TypeScript, and +// Rust after the fix. + +module router_model { + const ALLOW_EMPTY_NAME: bool + + pure val RESERVED = Set("create", "json", "exec") + pure val KNOWN_SERVICES = Set("beacon") + + pure val BY_NAME_ACTIONS = Set("start", "stop", "restart", "kill", "wait", "pause", "unpause") + pure val DENIED_ACTIONS = Set("rename", "update") + + // Kept apart from containerNameOf so that, under ALLOW_EMPTY_NAME, "the + // name is empty" and "there is no name" stay distinct. + pure def hasContainerName(segs: List[str]): bool = + if (segs.length() < 2) false + else and { + segs[0] == "containers", + not(RESERVED.contains(segs[1])), + segs[1] != "" or ALLOW_EMPTY_NAME, + } + + pure def containerNameOf(segs: List[str]): str = + if (hasContainerName(segs)) segs[1] else "" + + pure def lastSeg(segs: List[str]): str = + if (segs.length() == 0) "" else segs[segs.length() - 1] + + pure def routeByName(name: str): str = + if (KNOWN_SERVICES.contains(name)) "allowKnown" else "allowUnknown" + + pure def route(method: str, segs: List[str]): str = + if (hasContainerName(segs)) { + val name = containerNameOf(segs) + if (method == "POST" and BY_NAME_ACTIONS.contains(lastSeg(segs))) routeByName(name) + else if (method == "POST" and DENIED_ACTIONS.contains(lastSeg(segs))) "deny" + else if (method == "DELETE") routeByName(name) + else if (method == "GET") "allowRead" + else "deny" + } + else if (method == "GET" or method == "HEAD") "allowRead" + else "deny" + + // ─── Path universe ────────────────────────────────────────────────── + + pure val WORDS = Set("containers", "", "json", "create", "exec", "mycontainer", "beacon", "start") + pure val METHODS = Set("GET", "POST", "DELETE") + + pure val PATHS: Set[List[str]] = + WORDS.map(a => [a]) + .union(tuples(WORDS, WORDS).map(t => [t._1, t._2])) + .union(tuples(WORDS, WORDS, WORDS).map(t => [t._1, t._2, t._3])) + + // ─── Property ─────────────────────────────────────────────────────── + + // A lifecycle allow only ever targets a real, non-reserved name. + pure val lifecycleOnlyTargetsRealNames: bool = + METHODS.forall(m => PATHS.forall(segs => + Set("allowKnown", "allowUnknown").contains(route(m, segs)) implies and { + segs.length() >= 2, + segs[1] != "", + not(RESERVED.contains(segs[1])), + } + )) + + // ─── Tests: one run per table row ─────────────────────────────────── + // + // Rows whose outcome does not depend on ALLOW_EMPTY_NAME run on both + // instances. The two rows that do, and soundTest, live in `router`. + + run emptyNameGetAllowedTest = + assert(route("GET", ["containers", ""]) == "allowRead") + + run reservedJsonDeleteDeniedTest = + assert(route("DELETE", ["containers", "json"]) == "deny") + + run reservedCreateDeleteDeniedTest = + assert(route("DELETE", ["containers", "create"]) == "deny") + + run reservedExecDeleteDeniedTest = + assert(route("DELETE", ["containers", "exec"]) == "deny") + + run realNameDeleteAllowedTest = + assert(route("DELETE", ["containers", "mycontainer"]) == "allowUnknown") + + run reservedInSubpathAllowedTest = + assert(route("GET", ["containers", "mycontainer", "json"]) == "allowRead") +} + +// ─── Instances ────────────────────────────────────────────────────────── + +// Go, TypeScript, and Rust after #48: an empty segment is not a name. +module router { + import router_model(ALLOW_EMPTY_NAME = false).* + + run emptyNameDeleteDeniedTest = + assert(route("DELETE", ["containers", ""]) == "deny") + + run emptyNameStartDeniedTest = + assert(route("POST", ["containers", "", "start"]) == "deny") + + run soundTest = + assert(lifecycleOnlyTargetsRealNames) +} + +// Rust before #48: `/containers/` and `/containers//start` reach +// route_by_name("") and are allowed as an unknown container. +module router_pre48 { + import router_model(ALLOW_EMPTY_NAME = true).* + + run pre48UnsoundTest = + assert(and { + not(lifecycleOnlyTargetsRealNames), + route("DELETE", ["containers", ""]) == "allowUnknown", + route("POST", ["containers", "", "start"]) == "allowUnknown", + }) +} From e8990113e99a84b1dffebda0944772bec602f05b Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 06:58:00 -0400 Subject: [PATCH 2/9] spec: clarify router model scope (#48) --- spec/README.md | 12 +++++++++--- spec/router.qnt | 11 ++++++++--- 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/spec/README.md b/spec/README.md index 141d16a..9853933 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` | Router path parsing: container-name extraction and the container-lifecycle branch, one `run` test per table row. Instances `router` (Go, TypeScript, Rust after #48) and `router_pre48` (Rust before #48) | +| `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 @@ -96,7 +96,7 @@ A path is a list of segments, so `/containers/` is `["containers", ""]` and `/co | `realNameDeleteAllowed` | `DELETE /containers/mycontainer` | allow (unknown container) | both | | `reservedInSubpathAllowed` | `GET /containers/mycontainer/json` | allow | both | -The Go, Rust and TypeScript router tests carry the same row names in comments. `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)). +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 @@ -106,7 +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, because the language tests share their names. `router.qnt` models only the lifecycle branch. The earlier exec, build and commit denials and `POST /containers/create` are left out, so it says nothing about paths that those checks catch first. +- **`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 can return a different outcome from the implementations: + - `DELETE /containers/mycontainer/exec` is `allowUnknown` in the model, but the exec check in all three implementations denies it. + - `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 diff --git a/spec/router.qnt b/spec/router.qnt index 99b05fe..9a5da86 100644 --- a/spec/router.qnt +++ b/spec/router.qnt @@ -3,8 +3,12 @@ // How the router extracts a container name from a request path, and how // the container-lifecycle branch routes on it (#48). Mirrors // `extract_container_name` and the lifecycle branch of `Router::route` in -// rs/src/proxy.rs; Go (`extractContainerName`) and TypeScript -// (`extractContainerName`) share the lifecycle branch. +// rs/src/proxy.rs. This is not the full router: checks that run before the +// lifecycle branch (exec, build, commit, POST /containers/create) are left +// out. 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. // // A path is a list of segments: `DELETE /containers/` is // ["containers", ""], `POST /containers//start` is ["containers", "", "start"]. @@ -101,7 +105,8 @@ module router_model { // ─── Instances ────────────────────────────────────────────────────────── -// Go, TypeScript, and Rust after #48: an empty segment is not a name. +// The extraction rule of Go, TypeScript, and Rust after #48: an empty +// segment is not a name. module router { import router_model(ALLOW_EMPTY_NAME = false).* From 642abd28b8cfbcd7016a63f9ef1c59d0074adf3e Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 07:48:39 -0400 Subject: [PATCH 3/9] test: pin empty container-name routing (#48) --- deploy/test.sh | 10 +++++++ go/internal/proxy/router_test.go | 47 ++++++++++++++++++++++++++++++++ rs/src/proxy.rs | 29 ++++++++++++++++++++ ts/src/proxy.test.ts | 19 +++++++++++++ 4 files changed, 105 insertions(+) diff --git a/deploy/test.sh b/deploy/test.sh index 4061645..7f6d5cd 100755 --- a/deploy/test.sh +++ b/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 "" diff --git a/go/internal/proxy/router_test.go b/go/internal/proxy/router_test.go index b791863..645c5c7 100644 --- a/go/internal/proxy/router_test.go +++ b/go/internal/proxy/router_test.go @@ -355,3 +355,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) + } + } +} diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs index b304db2..e9b190d 100644 --- a/rs/src/proxy.rs +++ b/rs/src/proxy.rs @@ -478,6 +478,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"])); diff --git a/ts/src/proxy.test.ts b/ts/src/proxy.test.ts index 6f58eb2..0d01756 100644 --- a/ts/src/proxy.test.ts +++ b/ts/src/proxy.test.ts @@ -199,4 +199,23 @@ describe("Router", () => { assert.equal(r.action, want, `route(${method} ${path})`); } }); + + // 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. + it("does not treat an empty path segment as a container name", () => { + const cases: [string, string, Action][] = [ + // emptyNameDeleteDeniedTest + ["DELETE", "/containers/", Action.Deny], + // emptyNameStartDeniedTest + ["POST", "/containers//start", Action.Deny], + // emptyNameGetAllowedTest + ["GET", "/containers/", Action.Allow], + ]; + for (const [method, path, want] of cases) { + const r = router.route(method, path); + assert.equal(r.action, want, `route(${method} ${path})`); + } + }); }); From 6645835a3e9b7c927e72466690eb9a114642b2bb Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 08:01:33 -0400 Subject: [PATCH 4/9] fix(rs): an empty path segment is not a container name (#48) --- rs/src/proxy.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs index e9b190d..10ebcf3 100644 --- a/rs/src/proxy.rs +++ b/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 From d798577277097ec31dcaa82f145c3b585437e60b Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 08:01:39 -0400 Subject: [PATCH 5/9] docs: update test coverage counts (#48) --- AGENTS.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 1b358e7..4343cef 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: 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) +- 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 ## 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 From 715dbdfa02a75cd69e354510a49192163798ad95 Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 08:03:46 -0400 Subject: [PATCH 6/9] docs: mention router.qnt and refresh README test counts (#48) --- AGENTS.md | 4 ++-- README.md | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 4343cef..90b83e9 100644 --- a/AGENTS.md +++ b/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) @@ -41,7 +41,7 @@ deploy/ — Docker Compose + integration tests - 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 +- 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 ./...` diff --git a/README.md b/README.md index 3c2ee0f..c9e91cb 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/) | 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,7 +363,7 @@ 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 only container-name extraction in the router's container-lifecycle branch, 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. @@ -371,7 +371,7 @@ The CI pipeline runs verification on every push and PR. A violation blocks the b 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 ``` From 1813c409d8108cf2c7e75a75887ba6ef5898805d Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 10:54:43 -0400 Subject: [PATCH 7/9] test: carry Quint row names on the reserved-segment cases (#48) --- go/internal/proxy/router_test.go | 6 ++++++ rs/src/proxy.rs | 6 ++++++ ts/src/proxy.test.ts | 6 ++++++ 3 files changed, 18 insertions(+) diff --git a/go/internal/proxy/router_test.go b/go/internal/proxy/router_test.go index 645c5c7..7b45541 100644 --- a/go/internal/proxy/router_test.go +++ b/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 { diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs index 10ebcf3..a357dd3 100644 --- a/rs/src/proxy.rs +++ b/rs/src/proxy.rs @@ -450,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 { diff --git a/ts/src/proxy.test.ts b/ts/src/proxy.test.ts index 0d01756..016ff40 100644 --- a/ts/src/proxy.test.ts +++ b/ts/src/proxy.test.ts @@ -184,14 +184,20 @@ describe("Router", () => { it("does not treat reserved path segments as container names", () => { const cases: [string, string, Action][] = [ // 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 (const [method, path, want] of cases) { From bf90ecab57142a26adfa1d0afa42615577ef009d Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Mon, 5 Oct 2026 10:54:50 -0400 Subject: [PATCH 8/9] docs: describe router.qnt scope accurately (#48) --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c9e91cb..d98a4dd 100644 --- a/README.md +++ b/README.md @@ -363,7 +363,7 @@ 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. A third module, `spec/router.qnt`, models only container-name extraction in the router's container-lifecycle branch, 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)). +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. From 68a445ec8776d88f91b0afbce7091d64996154a2 Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Wed, 7 Oct 2026 09:50:42 -0400 Subject: [PATCH 9/9] docs: Go's exec check covers only the name position (#48) --- spec/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/README.md b/spec/README.md index 9853933..ee76589 100644 --- a/spec/README.md +++ b/spec/README.md @@ -107,8 +107,8 @@ Two invariants are structurally tautological within the Quint model — they can - **`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 can return a different outcome from the implementations: - - `DELETE /containers/mycontainer/exec` is `allowUnknown` in the model, but the exec check in all three implementations denies it. +- **`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.