refactor: remove the unreachable ExecGate; refresh docs and counts (#55)

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
 

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).

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,8 +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 |
-| ExecGate | Gate | Denies `POST /containers/*/exec` and `POST /exec/*/start` |
-| 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` |
@@ -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 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.
 

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
 

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{})

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")

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<String, serde_json::Value>,
-    ) -> 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<String, serde_json::Value>
 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);

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 <row>Test`) | Request | Outcome | Instances |
 |-----|---------|---------|-----------|

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" }),

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.

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> = {}): 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" });

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, unknown>): 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, unknown>): string | null {
     return ["POST", "PUT", "DELETE", "PATCH"].includes(method)