From 0e104b94eba4cf698d449e7cef20928ea1097979 Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Sun, 11 Oct 2026 02:50:42 -0400 Subject: [PATCH 1/3] refactor: remove the unreachable ExecGate; the router denies exec (#55) --- go/internal/middleware/chain.go | 1 - go/internal/middleware/chain_test.go | 22 ------------ go/internal/middleware/exec.go | 18 ---------- rs/src/middleware.rs | 53 ---------------------------- ts/src/middleware.test.ts | 22 ------------ ts/src/middleware.ts | 7 ---- 6 files changed, 123 deletions(-) delete mode 100644 go/internal/middleware/exec.go diff --git a/go/internal/middleware/chain.go b/go/internal/middleware/chain.go index 51f2426..5ae4b01 100644 --- a/go/internal/middleware/chain.go +++ b/go/internal/middleware/chain.go @@ -32,7 +32,6 @@ func NewChain(readonly bool) *Chain { if readonly { c.gates = append(c.gates, &ReadonlyGate{}) } - c.gates = append(c.gates, &ExecGate{}) c.gates = append(c.gates, &RegistryGate{}) c.gates = append(c.gates, &MountSourceGate{}) c.gates = append(c.gates, &EnvFileGate{}) diff --git a/go/internal/middleware/chain_test.go b/go/internal/middleware/chain_test.go index ddd3b93..8843112 100644 --- a/go/internal/middleware/chain_test.go +++ b/go/internal/middleware/chain_test.go @@ -64,17 +64,6 @@ func testPolicy(overrides map[string]interface{}) *policy.Policy { return p } -func TestExecGate_DeniesExec(t *testing.T) { - c := NewChain(false) - r := testRequest("POST", "/containers/test/exec") - body := map[string]interface{}{} - p := testPolicy(nil) - result := c.Execute(r, p, body) - if result.Allowed { - t.Fatal("expected exec to be denied") - } -} - func TestChain_ReadonlyDeniesWrites(t *testing.T) { for _, method := range []string{"POST", "PUT", "DELETE", "PATCH"} { c := NewChain(true) @@ -104,17 +93,6 @@ func TestChain_ReadonlyAllowsReads(t *testing.T) { } } -func TestExecGate_AllowsNonExec(t *testing.T) { - c := NewChain(false) - r := testRequest("POST", "/containers/create") - body := map[string]interface{}{"Image": "chainsafe/lodestar:next"} - p := testPolicy(nil) - result := c.Execute(r, p, body) - if !result.Allowed { - t.Fatalf("expected allow, got: %s", result.Reason) - } -} - func TestRegistryGate_ValidImage(t *testing.T) { c := NewChain(false) r := testRequest("POST", "/containers/create") diff --git a/go/internal/middleware/exec.go b/go/internal/middleware/exec.go deleted file mode 100644 index f0b20a3..0000000 --- a/go/internal/middleware/exec.go +++ /dev/null @@ -1,18 +0,0 @@ -package middleware - -import ( - "fmt" - "net/http" - "strings" - - "github.com/ChainSafe/docker-socket-policy/go/internal/policy" -) - -type ExecGate struct{} - -func (g *ExecGate) Check(r *http.Request, p *policy.Policy, body map[string]interface{}) error { - if strings.Contains(r.URL.Path, "/exec") && r.Method == "POST" { - return fmt.Errorf("exec is not allowed: docker exec provides a shell escape vector") - } - return nil -} diff --git a/rs/src/middleware.rs b/rs/src/middleware.rs index 4d3dcbb..097633c 100644 --- a/rs/src/middleware.rs +++ b/rs/src/middleware.rs @@ -37,7 +37,6 @@ impl Chain { if readonly { gates.push(Box::new(ReadonlyGate)); } - gates.push(Box::new(ExecGate)); gates.push(Box::new(RegistryGate)); gates.push(Box::new(MountSourceGate)); gates.push(Box::new(EnvFileGate)); @@ -86,22 +85,6 @@ fn charset_check(s: &str) -> bool { .all(|c| matches!(c, 'A'..='Z' | 'a'..='z' | '0'..='9' | '.' | '_' | '=' | ':' | '/' | ',' | '-')) } -pub struct ExecGate; -impl Gate for ExecGate { - fn check( - &self, - _method: &str, - path: &str, - _policy: &Policy, - _body: &HashMap, - ) -> std::result::Result<(), String> { - if path.contains("/exec") { - return Err("exec is not allowed: docker exec provides a shell escape vector".into()); - } - Ok(()) - } -} - pub struct ReadonlyGate; impl Gate for ReadonlyGate { fn check( @@ -389,32 +372,6 @@ fn body_from_json(json: serde_json::Value) -> HashMap mod tests { use super::*; - #[test] - fn test_exec_gate_allows_normal_create() { - let gate = ExecGate; - let policy = make_policy("test", vec!["alpine"]); - let body = body_from_json(serde_json::json!({"Image": "alpine"})); - assert!(gate.check("POST", "/containers/create", &policy, &body).is_ok()); - } - - #[test] - fn test_exec_gate_denies_exec_path() { - let gate = ExecGate; - let policy = make_policy("test", vec!["alpine"]); - let body = HashMap::new(); - assert!(gate.check("POST", "/containers/test/exec", &policy, &body).is_err()); - } - - #[test] - fn test_exec_gate_denies_exec_endpoint() { - let gate = ExecGate; - let policy = make_policy("test", vec!["alpine"]); - let body = HashMap::new(); - let result = gate.check("POST", "/exec/abc123/start", &policy, &body); - assert!(result.is_err()); - assert!(result.unwrap_err().contains("exec")); - } - #[test] fn test_readonly_gate_allows_get() { let gate = ReadonlyGate; @@ -711,16 +668,6 @@ mod tests { assert_eq!(result.reason, "container create allowed"); } - #[test] - fn test_chain_execute_denies_exec_via_gate() { - let chain = Chain::new(false); - let policy = make_policy("test", vec!["alpine"]); - let body = HashMap::new(); - let result = chain.execute("POST", "/containers/test/exec", &policy, &body); - assert!(!result.allowed); - assert!(result.reason.contains("exec")); - } - #[test] fn test_chain_execute_denies_unknown_image_via_registry_gate() { let chain = Chain::new(false); diff --git a/ts/src/middleware.test.ts b/ts/src/middleware.test.ts index 67b7f54..59d18d6 100644 --- a/ts/src/middleware.test.ts +++ b/ts/src/middleware.test.ts @@ -2,7 +2,6 @@ import { describe, it } from "node:test"; import assert from "node:assert/strict"; import { Chain, - ExecGate, ReadonlyGate, RegistryGate, MountSourceGate, @@ -20,20 +19,6 @@ function makePolicy(overrides: Partial = {}): Policy { }; } -describe("ExecGate", () => { - const gate = new ExecGate(); - - it("denies paths containing /exec", () => { - const result = gate.check("POST", "/containers/foo/exec", makePolicy(), {}); - assert.notEqual(result, null); - assert.ok(result?.includes("shell escape")); - }); - - it("allows non-exec paths", () => { - assert.equal(gate.check("POST", "/containers/create", makePolicy(), {}), null); - }); -}); - describe("ReadonlyGate", () => { const gate = new ReadonlyGate(); @@ -303,13 +288,6 @@ describe("Chain", () => { assert.ok(result.modifiedBody); }); - it("denies exec request", () => { - const chain = new Chain(false); - const result = chain.execute("POST", "/containers/foo/exec", makePolicy(), {}); - assert.equal(result.allowed, false); - assert.ok(result.reason.includes("exec")); - }); - it("denies readonly mode write request", () => { const chain = new Chain(true); const result = chain.execute("POST", "/containers/create", makePolicy(), { Image: "nginx:latest" }); diff --git a/ts/src/middleware.ts b/ts/src/middleware.ts index 0d24718..dde83b8 100644 --- a/ts/src/middleware.ts +++ b/ts/src/middleware.ts @@ -19,7 +19,6 @@ export class Chain { if (readonly) { this.gates.push(new ReadonlyGate()); } - this.gates.push(new ExecGate()); this.gates.push(new RegistryGate()); this.gates.push(new MountSourceGate()); this.gates.push(new EnvFileGate()); @@ -49,12 +48,6 @@ export class Chain { const SAFE_CHARSET = /^[A-Za-z0-9._=:/,\-]{1,256}$/; -export class ExecGate implements Gate { - check(_method: string, path: string, _policy: Policy, _body: Record): string | null { - return path.includes("/exec") ? "exec is not allowed: docker exec provides a shell escape vector" : null; - } -} - export class ReadonlyGate implements Gate { check(method: string, _path: string, _policy: Policy, _body: Record): string | null { return ["POST", "PUT", "DELETE", "PATCH"].includes(method) From 7649d406d1fa479f8f0178a0fc1e41681a1a02ec Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Sun, 11 Oct 2026 02:52:16 -0400 Subject: [PATCH 2/3] docs: refresh counts, invariants and gate list (#55) --- AGENTS.md | 12 ++++++------ CONTRIBUTING.md | 2 +- README.md | 13 ++++++------- deploy/test.sh | 2 +- spec/README.md | 3 ++- spec/docker_socket_policy.qnt | 6 ++++-- spec/listener-design.md | 3 ++- 7 files changed, 22 insertions(+), 19 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index c9add1b..56c28a6 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -27,7 +27,7 @@ deploy/ — Docker Compose + integration tests ## Architecture (same across all 3 languages) - `policy/` — Policy types + Manager (loads YAML from config dir) -- `middleware/` — Gate trait + Chain: ExecGate, ReadonlyGate, RegistryGate, MountSourceGate, EnvFileGate, CmdGate, ContainerConfigMutator +- `middleware/` — Gate trait + Chain: ReadonlyGate, RegistryGate, MountSourceGate, EnvFileGate, CmdGate, ContainerConfigMutator - `proxy/` — Router (default-deny), Handler (orchestrates chain), Transport (forwards to Docker socket) - `audit/` — JSON-structured logging @@ -39,17 +39,17 @@ deploy/ — Docker Compose + integration tests - Zero external deps where possible (Go: yaml.v3, Rust: tokio/hyper/serde/clap, TS: yaml) ## Test Coverage -- 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) +- Go: 108 unit tests (main/listener: 24, policy: 10, middleware: 27, proxy: 43, audit: 4) +- Rust: 143 unit tests (main/listener: 23, policy: 15, middleware: 46, proxy: 45, handler: 8, audit: 4, transport: 2) +- TypeScript: 161 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 38, proxy: 32, policy: 10, handler: 10, shutdown: 5, transport: 5, audit: 4) +- Integration, per implementation: 45 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`, `router_pre55`) ## 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` (43 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose +- Integration: `make test-integration` (45 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose ## Contribution Workflow diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8fc499a..9961454 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -34,7 +34,7 @@ To bypass a hook once, pass `--no-verify` to `git commit` or `git push`. CI runs All three languages implement the same architecture: - `policy/` — Policy types + Manager (loads YAML) -- `middleware/` — Gate trait + Chain (6 gates + 1 mutator) +- `middleware/` — Gate trait + Chain (5 gates + 1 mutator: ReadonlyGate, RegistryGate, MountSourceGate, EnvFileGate, CmdGate, ContainerConfigMutator; exec is denied by the router) - `proxy/` — Router (default-deny) + Handler + Transport Changes should be applied to **all three implementations** unless they are language-specific (e.g., CLI flag parsing). diff --git a/README.md b/README.md index 55c9e51..34ce5f2 100644 --- a/README.md +++ b/README.md @@ -10,9 +10,9 @@ A validating Docker API proxy that enforces **per-service container policies** t Key features: - **Policy-driven**: Per-service YAML policies, selected by image name, control images, volumes, flags, and env vars. The listening socket is the trust boundary: every caller of a socket can use every policy behind it (see [Trust model](#trust-model)) -- **Middleware pipeline**: 6 validation gates + 1 config mutator chain +- **Middleware pipeline**: 5 validation gates + 1 config mutator chain - **Default-deny router**: Only explicitly allowed endpoints pass through -- **Formally verified**: [Quint](https://quint-lang.org/) specification with 9 security invariants +- **Formally verified**: [Quint](https://quint-lang.org/) specification: 9 request-handling invariants, 6 listener invariants, and router properties for percent-encoded paths, empty segments, exec and the container lifecycle - **Audit logging**: JSON-structured logs for all requests and decisions - **Three implementations**: [Go](go/), [Rust](rs/), [TypeScript](ts/) — equal peer languages - **Minimal dependencies**: Zero external deps for Go, crate-based for Rust, npm for TypeScript @@ -100,9 +100,9 @@ All three implementations expose the same API surface, share the same [Quint spe | Language | Directory | Tests | Stack | |----------|-----------|-------|-------| -| 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 | +| Go | [go/](go/) | 108 unit + 45 integration + 15 socket | stdlib net/http + yaml.v3 | +| Rust | [rs/](rs/) | 143 unit + 45 integration + 15 socket | tokio, hyper, serde, clap | +| TypeScript | [ts/](ts/) | 161 unit (1 skipped) + 45 integration + 15 socket | Node 22 ESM, built-in http | ### Build All @@ -193,7 +193,6 @@ docker pull attacker/malware:latest # denied: image not in allowlist | Middleware | Type | What it checks | |------------|------|----------------| | ContainerConfigMutator | Mutator | Forces `network_mode`, `user`, `security_options`, `restart_policy` from policy | -| ExecGate | Gate | Denies `POST /containers/*/exec` and `POST /exec/*/start` | | ReadonlyGate | Gate | Denies all `POST`, `PUT`, `DELETE`, `PATCH` (optional `--readonly` flag) | | RegistryGate | Gate | Validates image ref against `allowed_image_prefixes` | | MountSourceGate | Gate | Validates volume binds against whitelist | @@ -440,7 +439,7 @@ not at the socket. ## 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 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)). +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 the router's denies for percent-encoded paths ([#53](https://github.com/ChainSafe/docker-socket-policy/issues/53)), empty interior segments ([#55](https://github.com/ChainSafe/docker-socket-policy/issues/55)) and exec ([#49](https://github.com/ChainSafe/docker-socket-policy/issues/49)), the `POST /containers/create` route, container-name extraction and the 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)). Its 7 properties are checked exhaustively over every method and every path of 1 to 3 segments; exec is denied by the router, not by a middleware gate. The CI pipeline runs verification on every push and PR. A violation blocks the build. diff --git a/deploy/test.sh b/deploy/test.sh index 9b4d0de..4ecd2e7 100755 --- a/deploy/test.sh +++ b/deploy/test.sh @@ -3,7 +3,7 @@ # Sends HTTP requests directly to the proxy's Docker API and checks status codes, # and the deny message on every expected proxy 403. # The proxy's ReadonlyGate, RegistryGate, MountSourceGate, EnvFileGate, -# CmdGate, ExecGate, and ContainerConfigMutator are all exercised. +# CmdGate, and ContainerConfigMutator are all exercised; exec is denied by the router. set -e diff --git a/spec/README.md b/spec/README.md index 23a21b2..ceb617f 100644 --- a/spec/README.md +++ b/spec/README.md @@ -93,8 +93,9 @@ A path is a list of raw, still percent-encoded segments with the query string re - `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`. - `emptyInteriorDenied` holds when every path with an empty segment before the last one is denied. +- `emptySegmentsHideNoExec` holds when every path that is an exec path once its empty segments are dropped is denied. -On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames`, `percentSoundTest` asserts `routerSeesWhatDaemonSees`, `execSoundTest` asserts `execNeverAllowed`, `execPrefixSoundTest` asserts `execPrefixNamesRoute`, `createExactSoundTest` asserts `createOnlyExact` `emptyInteriorSoundTest` asserts `emptyInteriorDenied` and `emptySegmentsHideNoExecTest` asserts `emptySegmentsHideNoExec`. +On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames`, `percentSoundTest` asserts `routerSeesWhatDaemonSees`, `execSoundTest` asserts `execNeverAllowed`, `execPrefixSoundTest` asserts `execPrefixNamesRoute`, `createExactSoundTest` asserts `createOnlyExact`, `emptyInteriorSoundTest` asserts `emptyInteriorDenied` and `emptySegmentsHideNoExecTest` asserts `emptySegmentsHideNoExec`. | Row (`run Test`) | Request | Outcome | Instances | |-----|---------|---------|-----------| diff --git a/spec/docker_socket_policy.qnt b/spec/docker_socket_policy.qnt index b31e1ee..88244af 100644 --- a/spec/docker_socket_policy.qnt +++ b/spec/docker_socket_policy.qnt @@ -178,7 +178,8 @@ module docker_socket_policy { { method: "POST", path: "/auth", kind: "deny" }, { method: "POST", path: "/build", kind: "deny" }, { method: "POST", path: "/commit", kind: "deny" }, - { method: "POST", path: "/containers/:name/exec", kind: "deny" }, + { method: "*", path: "/containers/:name/exec", kind: "deny" }, + { method: "*", path: "/exec/*", kind: "deny" }, { method: "POST", path: "/containers/:name/rename",kind: "deny" }, { method: "POST", path: "/containers/:name/update",kind: "deny" }, { method: "POST", path: "/containers/:name/attach",kind: "deny" }, @@ -450,7 +451,8 @@ module docker_socket_policy { endpointsTable.contains({ method: "POST", path: "/auth", kind: "deny" }), endpointsTable.contains({ method: "POST", path: "/build", kind: "deny" }), endpointsTable.contains({ method: "POST", path: "/commit", kind: "deny" }), - endpointsTable.contains({ method: "POST", path: "/containers/:name/exec", kind: "deny" }), + endpointsTable.contains({ method: "*", path: "/containers/:name/exec", kind: "deny" }), + endpointsTable.contains({ method: "*", path: "/exec/*", kind: "deny" }), endpointsTable.contains({ method: "POST", path: "/containers/:name/rename",kind: "deny" }), endpointsTable.contains({ method: "POST", path: "/containers/:name/update",kind: "deny" }), endpointsTable.contains({ method: "POST", path: "/containers/:name/attach",kind: "deny" }), diff --git a/spec/listener-design.md b/spec/listener-design.md index 06fad74..ff98adb 100644 --- a/spec/listener-design.md +++ b/spec/listener-design.md @@ -246,7 +246,8 @@ Unit, in all three languages, same cases: - `fd://3` rejected as a non-path value. - `--listen-socket-mode` rejected as unknown. - Group table: default missing → own gid + warning; explicit missing → error; - `""` → own gid, no warning; explicit numeric → that gid. + `""` → own gid, no warning; explicit numeric → that gid (digits only, + `0-4294967294`; larger exits 2). - Existing path: stale socket replaced at `0660`; live socket refused and left in place (same inode, first listener still answers); non-socket refused. From 62667071cc8a892443950834210d92a410813401 Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Sun, 11 Oct 2026 02:55:34 -0400 Subject: [PATCH 3/3] docs: state the router model scope and the --readonly gap precisely (#55) --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 34ce5f2..0b668a5 100644 --- a/README.md +++ b/README.md @@ -193,7 +193,7 @@ docker pull attacker/malware:latest # denied: image not in allowlist | Middleware | Type | What it checks | |------------|------|----------------| | ContainerConfigMutator | Mutator | Forces `network_mode`, `user`, `security_options`, `restart_policy` from policy | -| ReadonlyGate | Gate | Denies all `POST`, `PUT`, `DELETE`, `PATCH` (optional `--readonly` flag) | +| ReadonlyGate | Gate | Denies `POST`, `PUT`, `DELETE`, `PATCH` (optional `--readonly` flag). Like every gate it runs only on container create, so lifecycle actions and `DELETE` are not blocked yet ([#75](https://github.com/ChainSafe/docker-socket-policy/issues/75)) | | RegistryGate | Gate | Validates image ref against `allowed_image_prefixes` | | MountSourceGate | Gate | Validates volume binds against whitelist | | EnvFileGate | Gate | Strips `Env` field from create body; env must come from locked `env_file` | @@ -439,7 +439,7 @@ not at the socket. ## 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 the router's denies for percent-encoded paths ([#53](https://github.com/ChainSafe/docker-socket-policy/issues/53)), empty interior segments ([#55](https://github.com/ChainSafe/docker-socket-policy/issues/55)) and exec ([#49](https://github.com/ChainSafe/docker-socket-policy/issues/49)), the `POST /containers/create` route, container-name extraction and the 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)). Its 7 properties are checked exhaustively over every method and every path of 1 to 3 segments; exec is denied by the router, not by a middleware gate. +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 the router's denies for percent-encoded paths ([#53](https://github.com/ChainSafe/docker-socket-policy/issues/53)), empty interior segments ([#55](https://github.com/ChainSafe/docker-socket-policy/issues/55)) and exec ([#49](https://github.com/ChainSafe/docker-socket-policy/issues/49)), the `POST /containers/create` route, container-name extraction and the 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)). Its 7 properties are checked exhaustively over the methods `GET`, `HEAD`, `POST`, `DELETE` and every path of 1 to 3 segments over the model's word set; exec is denied by the router, not by a middleware gate. The CI pipeline runs verification on every push and PR. A violation blocks the build.