fix: allow only GET and HEAD on the read endpoints and refuse CONNECT (#78)

AGENTS.md

@@ -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: 110 unit tests (main/listener: 24, policy: 10, middleware: 25, proxy: 47, audit: 4)
-- Rust: 142 unit tests (main/listener: 23, policy: 15, middleware: 41, proxy: 47, handler: 10, audit: 4, transport: 2)
-- TypeScript: 160 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 32, proxy: 34, policy: 10, handler: 13, shutdown: 5, transport: 5, audit: 4)
-- Integration, per implementation: 53 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`, `router_readonly`, whose `readonly*` tests run with `--match`, and `router_pre76`)
+- Go: 112 unit tests (main/listener: 24, policy: 10, middleware: 25, proxy: 49, audit: 4)
+- Rust: 144 unit tests (main/listener: 23, policy: 15, middleware: 41, proxy: 48, handler: 11, audit: 4, transport: 2)
+- TypeScript: 163 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 32, proxy: 35, policy: 10, handler: 15, shutdown: 5, transport: 5, audit: 4)
+- Integration, per implementation: 60 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`, `router_readonly`, whose `readonly*` tests run with `--match`, `router_pre76` and `router_pre78`)
 
 ## 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` (53 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
+- Integration: `make test-integration` (60 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
 
 ## Contribution Workflow
 

Makefile

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

README.md

@@ -12,7 +12,7 @@ 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**: 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 `--readonly`, percent-encoded paths, empty segments, exec, attach 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, attach, the read-only passthrough 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/) | 110 unit + 53 integration + 15 socket | stdlib net/http + yaml.v3 |
-| Rust | [rs/](rs/) | 142 unit + 53 integration + 15 socket | tokio, hyper, serde, clap |
-| TypeScript | [ts/](ts/) | 160 unit (1 skipped) + 53 integration + 15 socket | Node 22 ESM, built-in http |
+| Go | [go/](go/) | 112 unit + 60 integration + 15 socket | stdlib net/http + yaml.v3 |
+| Rust | [rs/](rs/) | 144 unit + 60 integration + 15 socket | tokio, hyper, serde, clap |
+| TypeScript | [ts/](ts/) | 163 unit (1 skipped) + 60 integration + 15 socket | Node 22 ESM, built-in http |
 
 ### Build All
 
@@ -204,6 +204,7 @@ The chain runs only on container create. `--readonly` is not a gate: the router
 
 | HTTP Method | Path | Action |
 |-------------|------|--------|
+| CONNECT | Any target | **DENIED** (checked first, before routing) |
 | Any | Request with an `Upgrade` header, or `Connection: upgrade` | **DENIED** (checked before routing) |
 | Not GET/HEAD | Any (with `--readonly`) | **DENIED** (checked first in the router) |
 | Any | Path containing `%` | **DENIED** (see below) |
@@ -219,7 +220,7 @@ The chain runs only on container create. `--readonly` is not a gate: the router
 | POST | `/auth` | **DENIED** |
 | POST | `/build` | **DENIED** |
 | POST | `/commit` | **DENIED** |
-| GET/HEAD | Any other path without `%` or `//` | Allowed (read-only) |
+| GET/HEAD | Any other path without `%` or `//`, including `/_ping`, `/version`, `/info`, `/events` | Allowed (read-only) |
 | Other | Other | **DENIED** |
 
 Any request whose path contains a percent-encoded byte (`%`) is denied with 403 for every method, GET and HEAD included, because the daemon decodes the path before routing. The query string is not inspected, so filters such as `docker ps --filter …` still work. The Go implementation also denies paths that contain raw characters it must re-encode, such as non-ASCII bytes or `{`; the Docker CLI never sends these. A consequence is that networks whose names need percent-encoding (for example a space or `%`) cannot be inspected by name through the proxy; inspecting them by ID still works, and other network operations are denied regardless.
@@ -228,6 +229,8 @@ Exec is matched on whole path segments, so containers named like `exec-runner` w
 
 Attach is matched the same way: an `attach` segment under `/containers` is denied for every method, so `attach-runner` is an ordinary name, while a container literally named `attach` cannot be reached by name. Protocol upgrades are refused outright: any request with an `Upgrade` header, or a `Connection` header that lists `upgrade`, gets 403 `protocol upgrade not allowed` before it is routed, whatever its path ([#76](https://github.com/ChainSafe/docker-socket-policy/issues/76)). Forwarding one would hand the caller a raw stream to the daemon. Every Docker endpoint that upgrades (attach, exec start, the build session) is denied anyway; the refusal keeps any path the router allows from becoming one.
 
+`/_ping`, `/version`, `/info` and `/events` are ordinary reads: `GET` and `HEAD` pass, and every other method is denied with `endpoint <METHOD> <path> is not allowed`, `OPTIONS` (a CORS preflight) included ([#78](https://github.com/ChainSafe/docker-socket-policy/issues/78)). `CONNECT` is refused with 403 `CONNECT is not allowed` before anything else, whatever its target or headers; the TypeScript proxy answers it on the raw socket, since Node never hands `CONNECT` to the request handler.
+
 ## Configuration
 
 ### CLI Flags
@@ -445,7 +448,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 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)), exec ([#49](https://github.com/ChainSafe/docker-socket-policy/issues/49)) and attach ([#76](https://github.com/ChainSafe/docker-socket-policy/issues/76)), 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 9 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)), exec ([#49](https://github.com/ChainSafe/docker-socket-policy/issues/49)) and attach ([#76](https://github.com/ChainSafe/docker-socket-policy/issues/76)), the GET/HEAD-only read passthrough ([#78](https://github.com/ChainSafe/docker-socket-policy/issues/78)), 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 10 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

@@ -4,8 +4,9 @@
 # and the deny message on every expected proxy 403.
 # The proxy's RegistryGate, MountSourceGate, EnvFileGate, CmdGate, and
 # ContainerConfigMutator are all exercised; exec and attach are denied by the
-# router, protocol upgrades by the handler (#76), and every write on a second
-# proxy run with --readonly (#75).
+# router, protocol upgrades by the handler (#76), non-read methods on the read
+# endpoints by the router and CONNECT by the handler (#78), and every write on a
+# second proxy run with --readonly (#75).
 
 set -e
 
@@ -166,7 +167,7 @@ case "$rc" in
     ;;
 esac
 
-# ─── Read-only endpoints (always allowed) ───────────────────────
+# ─── Read-only endpoints (GET and HEAD allowed, #78) ────────────
 
 echo "--- Read-only endpoints ---"
 
@@ -473,6 +474,42 @@ check_denied "GET /containers/*/attach/ws -> 403 (attach denied)" "$S" "$BODY" '
 S=$(upgrade_get "$PROXY/_ping")
 check_denied "GET /_ping with Upgrade: websocket -> 403 (upgrade refused)" "$S" "$BODY" 'protocol upgrade not allowed'
 
+# #78: the read endpoints admit only GET and HEAD. Before #78 an early router
+# clause allowed /_ping, /version, /info and /events… for every method, so the
+# daemon answered POST /_ping. CONNECT is refused by the handler before
+# routing; before #78 the TypeScript proxy dropped it with no response.
+# method_status METHOD URL [CURL_ARGS...]
+method_status() {
+  : >"$BODY"
+  m="$1"
+  u="$2"
+  shift 2
+  out=$(curl -s -o "$BODY" -w '%{http_code}' $TIMEOUT --unix-socket "$PROXY_SOCK" \
+    -X "$m" "$@" "$u" 2>/dev/null || true)
+  echo "${out:-000}"
+}
+
+S=$(method_status POST "$PROXY/_ping")
+check_denied "POST /_ping -> 403 (read endpoint, GET/HEAD only)" "$S" "$BODY" 'endpoint POST /_ping is not allowed'
+
+S=$(method_status DELETE "$PROXY/version")
+check_denied "DELETE /version -> 403 (read endpoint, GET/HEAD only)" "$S" "$BODY" 'endpoint DELETE /version is not allowed'
+
+S=$(method_status OPTIONS "$PROXY/_ping")
+check_denied "OPTIONS /_ping -> 403 (CORS preflight denied)" "$S" "$BODY" 'endpoint OPTIONS /_ping is not allowed'
+
+S=$(method_status CONNECT "$PROXY/_ping")
+check_denied "CONNECT /_ping -> 403 (CONNECT refused)" "$S" "$BODY" 'CONNECT is not allowed'
+
+S=$(method_status CONNECT "$PROXY/" --request-target localhost:80)
+check_denied "CONNECT localhost:80 -> 403 (CONNECT refused, authority form)" "$S" "$BODY" 'CONNECT is not allowed'
+
+S=$(method_status HEAD "$PROXY/_ping" -I)
+check "HEAD /_ping -> 200" "200" "$S"
+
+S=$(get_status "$PROXY/events?since=1&until=2")
+check "GET /events (bounded) -> 200" "200" "$S"
+
 # ─── Read-only mode (#75) ────────────────────────────────
 
 # The same config behind --readonly. Every request whose method is not GET or

go/internal/proxy/handler.go

@@ -33,6 +33,16 @@ func NewHandler(router *Router, chain *middleware.Chain, auditLog *audit.Logger,
 }
 
 func (h *Handler) ServeHTTP(w http.ResponseWriter, r *http.Request) {
+	// Refuse CONNECT before anything else, whatever its target or headers: it
+	// asks for a tunnel, which the proxy never provides (#78).
+	if r.Method == http.MethodConnect {
+		const msg = "CONNECT is not allowed"
+		slog.Warn("denied", "method", r.Method, "path", r.RequestURI, "reason", msg)
+		h.auditLog.Deny(r.Method, r.RequestURI, msg, map[string]interface{}{"method": r.Method, "path": r.RequestURI})
+		http.Error(w, msg, http.StatusForbidden)
+		return
+	}
+
 	// Refuse protocol upgrades before anything else: the reverse proxy would
 	// relay a 101 and hand the caller a raw stream to the daemon (#76).
 	if isUpgradeRequest(r.Header) {

go/internal/proxy/handler_test.go

@@ -453,3 +453,78 @@ func TestHandlerRefusesProtocolUpgrade(t *testing.T) {
 		t.Fatalf("protocol upgrade mismatches:\n%s", strings.Join(mismatches, "\n"))
 	}
 }
+
+// #78: CONNECT is refused before the upgrade check and before routing, so the
+// transport never sees it, in origin form and in authority form. Before #78
+// CONNECT /_ping matched the early read-endpoint allow and was forwarded.
+func TestHandlerRefusesConnect(t *testing.T) {
+	dir := t.TempDir()
+	os.WriteFile(filepath.Join(dir, "default.yaml"), []byte("service_name: default\nallowed_image_prefixes:\n  - scratch\n"), 0644)
+	policyManager, err := policy.NewManager(dir)
+	if err != nil {
+		t.Fatalf("NewManager failed: %v", err)
+	}
+	logPath := filepath.Join(t.TempDir(), "audit.log")
+	auditLog, err := audit.NewLogger(logPath)
+	if err != nil {
+		t.Fatalf("NewLogger failed: %v", err)
+	}
+	defer auditLog.Close()
+	const refused = "CONNECT is not allowed"
+
+	tests := []struct {
+		name    string
+		target  string
+		headers map[string]string
+	}{
+		{"origin form", "/_ping", nil},
+		{"authority form", "localhost:80", nil},
+		{"with Upgrade", "/_ping", map[string]string{"Upgrade": "websocket", "Connection": "Upgrade"}},
+	}
+	var mismatches []string
+	for _, tt := range tests {
+		rec := &recorderTransport{}
+		h := NewHandler(NewRouter(policyManager), middleware.NewChain(), auditLog, rec)
+		req := httptest.NewRequest("CONNECT", tt.target, nil)
+		for k, v := range tt.headers {
+			req.Header.Set(k, v)
+		}
+		w := httptest.NewRecorder()
+		h.ServeHTTP(w, req)
+		if got := strings.TrimSpace(w.Body.String()); w.Code != http.StatusForbidden || got != refused {
+			mismatches = append(mismatches, tt.name+": "+http.StatusText(w.Code)+" "+got)
+		}
+		if rec.lastRequest != nil {
+			mismatches = append(mismatches, tt.name+": forwarded")
+		}
+	}
+
+	data, err := os.ReadFile(logPath)
+	if err != nil {
+		t.Fatalf("reading audit log: %v", err)
+	}
+	lines := strings.Split(strings.TrimSpace(string(data)), "\n")
+	wantURIs := []string{"/_ping", "localhost:80", "/_ping"}
+	for i, wantURI := range wantURIs {
+		if i >= len(lines) {
+			mismatches = append(mismatches, "audit entry missing for "+wantURI)
+			continue
+		}
+		var entry struct {
+			Method   string `json:"method"`
+			URI      string `json:"uri"`
+			Decision string `json:"decision"`
+			Reason   string `json:"reason"`
+		}
+		if err := json.Unmarshal([]byte(lines[i]), &entry); err != nil {
+			t.Fatalf("audit line %d: %v", i, err)
+		}
+		if entry.Method != "CONNECT" || entry.URI != wantURI || entry.Decision != "DENY" || entry.Reason != refused {
+			mismatches = append(mismatches, "audit entry: "+lines[i])
+		}
+	}
+
+	if len(mismatches) > 0 {
+		t.Fatalf("CONNECT mismatches:\n%s", strings.Join(mismatches, "\n"))
+	}
+}

go/internal/proxy/router.go

@@ -59,10 +59,6 @@ func (r *Router) Route(method, path string, body map[string]interface{}) *RouteR
 
 	path = stripAPIVersion(path)
 
-	if path == "/_ping" || path == "/version" || path == "/info" || strings.HasPrefix(path, "/events") {
-		return &RouteResult{Action: ActionAllow}
-	}
-
 	if strings.HasPrefix(path, "/auth") {
 		return &RouteResult{Action: ActionDeny, DenyMsg: "auth endpoint is not allowed"}
 	}