fix: enforce --readonly in the router for every write (#75)

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: ReadonlyGate, RegistryGate, MountSourceGate, EnvFileGate, CmdGate, ContainerConfigMutator
+- `middleware/` — Gate trait + Chain: RegistryGate, MountSourceGate, EnvFileGate, CmdGate, ContainerConfigMutator (`--readonly` and exec are denied by the router)
 - `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: 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`)
+- Go: 108 unit tests (main/listener: 24, policy: 10, middleware: 25, proxy: 45, audit: 4)
+- Rust: 140 unit tests (main/listener: 23, policy: 15, middleware: 41, proxy: 46, handler: 9, audit: 4, transport: 2)
+- TypeScript: 157 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 32, proxy: 33, policy: 10, handler: 11, shutdown: 5, transport: 5, audit: 4)
+- Integration, per implementation: 50 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`, and `router_readonly`, whose `readonly*` tests run with `--match`)
 
 ## 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` (45 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
+- Integration: `make test-integration` (50 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 (5 gates + 1 mutator: ReadonlyGate, RegistryGate, MountSourceGate, EnvFileGate, CmdGate, ContainerConfigMutator; exec is denied by the router)
+- `middleware/` — Gate trait + Chain (4 gates + 1 mutator: RegistryGate, MountSourceGate, EnvFileGate, CmdGate, ContainerConfigMutator; `--readonly` and exec are 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).

Makefile

@@ -102,6 +102,7 @@ test-spec:
 	$(QUINT) test $(ROUTER_SPEC) --main=router_pre48
 	$(QUINT) test $(ROUTER_SPEC) --main=router_pre53
 	$(QUINT) test $(ROUTER_SPEC) --main=router_pre55
+	$(QUINT) test $(ROUTER_SPEC) --main=router_readonly --match='^readonly.*Test$$'
 
 verify-ts:
 	$(QUINT) run $(SPEC) --max-steps=50 --invariants allInvariants --backend typescript

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**: 5 validation gates + 1 config mutator chain
+- **Middleware pipeline**: 4 validation gates + 1 config mutator chain
 - **Default-deny router**: Only explicitly allowed endpoints pass through
-- **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
+- **Formally verified**: [Quint](https://quint-lang.org/) specification: 9 request-handling invariants, 6 listener invariants, and router properties for `--readonly`, 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 + 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 |
+| Go | [go/](go/) | 108 unit + 50 integration + 15 socket | stdlib net/http + yaml.v3 |
+| Rust | [rs/](rs/) | 140 unit + 50 integration + 15 socket | tokio, hyper, serde, clap |
+| TypeScript | [ts/](ts/) | 157 unit (1 skipped) + 50 integration + 15 socket | Node 22 ESM, built-in http |
 
 ### Build All
 
@@ -193,16 +193,18 @@ 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 `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` |
 | CmdGate | Gate | Validates each CLI flag in `Cmd` array against allowlist + denylist |
 
+The chain runs only on container create. `--readonly` is not a gate: the router denies every request that is not `GET` or `HEAD`, on every path, before any other check ([#75](https://github.com/ChainSafe/docker-socket-policy/issues/75)). A websocket attach (`GET /containers/{name}/attach/ws` with `Upgrade`) is a `GET` and is not denied yet; the Go proxy lets it write to a container's stdin ([#76](https://github.com/ChainSafe/docker-socket-policy/issues/76)).
+
 ## Endpoint Access
 
 | HTTP Method | Path | Action |
 |-------------|------|--------|
+| Not GET/HEAD | Any (with `--readonly`) | **DENIED** (checked first) |
 | Any | Path containing `%` | **DENIED** (see below) |
 | Any | Path containing `//` | **DENIED** |
 | POST | `/containers/create` | Validated by middleware chain |
@@ -232,7 +234,7 @@ Exec is matched on whole path segments, so containers named like `exec-runner` w
 | `--docker-host` | `/var/run/docker.sock` | Docker daemon socket path (Unix socket only) |
 | `--config-dir` | `/etc/docker-socket-policy/services` | Policy config directory |
 | `--log-file` | `/var/log/docker-socket-policy.log` | Audit log path |
-| `--readonly` | `false` | Enable read-only mode |
+| `--readonly` | `false` | Enable read-only mode: the router denies every request that is not `GET` or `HEAD` |
 | `--listen-socket-group` | `docker-socket-policy` | Group owning the socket (default `docker-socket-policy`; `""` = the proxy's own group) |
 
 > **Unix socket security boundary**: the proxy listens on a Unix socket only,
@@ -439,7 +441,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 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.
+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 writes under `--readonly` ([#75](https://github.com/ChainSafe/docker-socket-policy/issues/75)), 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 8 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/docker-compose.yml

@@ -16,14 +16,33 @@ services:
       - --config-dir=/etc/docker-socket-policy/services
       - --log-file=/tmp/docker-socket-policy.log
 
+  # The same proxy with --readonly (#75), on its own socket in the shared volume.
+  proxy-readonly:
+    build:
+      context: ../${IMPL:-go}
+      dockerfile: Dockerfile
+    user: "0:0"
+    volumes:
+      - /var/run/docker.sock:/var/run/docker.sock
+      - ./config:/etc/docker-socket-policy/services:ro
+      - proxy-sock:/sock
+    command:
+      - --docker-host=/var/run/docker.sock
+      - --listen-socket=/sock/readonly.sock
+      - --config-dir=/etc/docker-socket-policy/services
+      - --log-file=/tmp/docker-socket-policy-readonly.log
+      - --readonly
+
   test:
     build:
       context: .
       dockerfile: Dockerfile.test
     depends_on:
       - proxy
+      - proxy-readonly
     environment:
       PROXY_SOCK: /sock/proxy.sock
+      PROXY_RO_SOCK: /sock/readonly.sock
       # Hostname the proxy would have been reachable on when it still had a
       # TCP listener, so the suite can assert that it no longer is.
       PROXY_HOST: proxy

deploy/test.sh

@@ -2,8 +2,9 @@
 # Integration tests for docker-socket-policy.
 # 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, and ContainerConfigMutator are all exercised; exec is denied by the router.
+# The proxy's RegistryGate, MountSourceGate, EnvFileGate, CmdGate, and
+# ContainerConfigMutator are all exercised; exec is denied by the router, and so
+# is every write on a second proxy run with --readonly (#75).
 
 set -e
 
@@ -29,24 +30,31 @@ fi
 # instead of failing it — and the readiness counter below would never advance.
 TIMEOUT="--max-time 10 --connect-timeout 2"
 
-# Wait for the proxy to create and serve its socket.
-echo "Waiting for proxy at ${PROXY_SOCK}..."
-i=0
-while [ $i -lt 30 ]; do
-  if curl -sf $TIMEOUT --unix-socket "$PROXY_SOCK" "$PROXY/_ping" >/dev/null 2>&1; then
-    echo "Proxy ready."
-    break
+# The --readonly proxy (#75) serves the same config on its own socket.
+PROXY_RO_SOCK="${PROXY_RO_SOCK:-/sock/readonly.sock}"
+
+# Wait for a proxy to create and serve its socket.
+wait_for_sock() {
+  echo "Waiting for proxy at $1..."
+  i=0
+  while [ $i -lt 30 ]; do
+    if curl -sf $TIMEOUT --unix-socket "$1" "$PROXY/_ping" >/dev/null 2>&1; then
+      echo "Proxy ready."
+      break
+    fi
+    printf "."
+    sleep 1
+    i=$((i + 1))
+  done
+  if [ $i -eq 30 ]; then
+    echo ""
+    echo "ERROR: Proxy at $1 failed to respond within 30s"
+    exit 1
   fi
-  printf "."
-  sleep 1
-  i=$((i + 1))
-done
-if [ $i -eq 30 ]; then
   echo ""
-  echo "ERROR: Proxy failed to respond within 30s"
-  exit 1
-fi
-echo ""
+}
+wait_for_sock "$PROXY_SOCK"
+wait_for_sock "$PROXY_RO_SOCK"
 
 # Helpers: report the HTTP status code of a request sent over the Unix socket.
 # curl exits non-zero when it cannot connect at all, which under `set -e` would
@@ -440,6 +448,34 @@ S="${S:-000}"
 check_denied "GET http://docker/exec/*/json -> 403 (absolute-form target)" "$S" "$BODY" \
   'exec is not allowed' 'empty path segment not allowed'
 
+# ─── Read-only mode (#75) ────────────────────────────────
+
+# The same config behind --readonly. Every request whose method is not GET or
+# HEAD is denied by the router. Before #75 the flag only reached the gate
+# chain, which runs on create alone, so these reached the daemon (a 404 for
+# the unknown container below, i.e. a leak, not a proxy 403).
+echo ""
+echo "--- Read-only mode ---"
+
+# The request helpers read PROXY_SOCK, so this switches every check below to
+# the read-only proxy. Keep this section last.
+PROXY_SOCK="$PROXY_RO_SOCK"
+
+S=$(get_status "$PROXY/_ping")
+check "GET /_ping -> 200 (read-only)" "200" "$S"
+
+S=$(post_empty "$PROXY/containers/no-such-container/stop")
+check_denied "POST /containers/*/stop -> 403 (read-only)" "$S" "$BODY" 'read-only mode: POST requests are not allowed'
+
+S=$(delete_status "$PROXY/containers/no-such-container")
+check_denied "DELETE /containers/* -> 403 (read-only)" "$S" "$BODY" 'read-only mode: DELETE requests are not allowed'
+
+S=$(post_json '{"Image":"chainsafe/lodestar:beacon","Cmd":["--rcConfig","/data/config.yml"]}' "$PROXY/containers/create")
+check_denied "POST /containers/create with allowed image -> 403 (read-only)" "$S" "$BODY" 'read-only mode: POST requests are not allowed'
+
+S=$(post_empty "$PROXY/images/create?fromImage=chainsafe/lodestar&tag=beacon")
+check_denied "POST /images/create?fromImage=chainsafe/lodestar -> 403 (read-only)" "$S" "$BODY" 'read-only mode: POST requests are not allowed'
+
 # ─── Summary ──────────────────────────────────────────
 
 echo ""

go/internal/middleware/chain.go

@@ -26,12 +26,9 @@ type Chain struct {
 	mutators []Mutator
 }
 
-func NewChain(readonly bool) *Chain {
+func NewChain() *Chain {
 	c := &Chain{}
 
-	if readonly {
-		c.gates = append(c.gates, &ReadonlyGate{})
-	}
 	c.gates = append(c.gates, &RegistryGate{})
 	c.gates = append(c.gates, &MountSourceGate{})
 	c.gates = append(c.gates, &EnvFileGate{})