abienkowski · Oct 12, 2026 · Oct 12, 2026 · Oct 12, 2026 · Oct 12, 2026
diff --git a/AGENTS.md b/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: 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`)
+- 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`)
 
 ## 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` (50 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
+- Integration: `make test-integration` (53 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose
 
 ## Contribution Workflow
 

diff --git a/Makefile b/Makefile
@@ -103,6 +103,7 @@ test-spec:
 	$(QUINT) test $(ROUTER_SPEC) --main=router_pre53
 	$(QUINT) test $(ROUTER_SPEC) --main=router_pre55
 	$(QUINT) test $(ROUTER_SPEC) --main=router_readonly --match='^readonly.*Test$$'
+	$(QUINT) test $(ROUTER_SPEC) --main=router_pre76
 
 verify-ts:
 	$(QUINT) run $(SPEC) --max-steps=50 --invariants allInvariants --backend typescript

diff --git a/README.md b/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 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 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 + 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 |
+| 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 |
 
 ### Build All
 
@@ -198,20 +198,22 @@ docker pull attacker/malware:latest  # denied: image not in allowlist
 | 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)).
+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)). Attach is denied by the router for every method, so a websocket attach (`GET /containers/{name}/attach/ws`) cannot reach a container's stdin, with or without `--readonly` ([#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 | 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) |
 | Any | Path containing `//` | **DENIED** |
 | POST | `/containers/create` | Validated by middleware chain |
 | POST | `/containers/{name}/start\|stop\|restart\|kill\|wait\|pause\|unpause` | Allowed on known containers |
 | DELETE | `/containers/{name}` | Allowed on known containers |
 | Any | `/containers/…/exec` (an `exec` segment anywhere under `/containers`) | **DENIED** |
 | Any | `/exec/*` | **DENIED** |
+| Any | `/containers/{name}/attach…` (an `attach` segment anywhere under `/containers`) | **DENIED** |
 | POST | `/containers/{name}/rename\|update` | **DENIED** |
 | POST | `/images/create` | Validated by registry gate |
 | POST | `/auth` | **DENIED** |
@@ -224,6 +226,8 @@ Any request whose path contains a percent-encoded byte (`%`) is denied with 403
 
 Exec is matched on whole path segments, so containers named like `exec-runner` work normally, and exec inspect (`GET /exec/{id}/json`) is denied too. A path with an empty segment (`//`, as in `//exec/{id}/json`) is denied for every method, so an empty segment cannot hide the exec namespace; a single trailing slash is fine, and `//` in the query string is not inspected. Absolute-form request targets (`GET http://host/…`) never reach exec: Go and Rust route them on the parsed path, so exec is denied and other paths are routed as usual, while the TypeScript proxy sees the raw target and denies every absolute-form request (its `//` after the scheme is an empty segment). The Docker CLI never sends absolute form.
 
+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.
+
 ## Configuration
 
 ### CLI Flags
@@ -441,7 +445,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)) 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.
+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.
 
 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
@@ -3,8 +3,9 @@
 # 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 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).
+# 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).
 
 set -e
 
@@ -448,6 +449,30 @@ 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'
 
+# #76: attach is denied by the router for every method, and any protocol
+# upgrade is refused by the handler before routing. Before #76 a websocket
+# attach went through the GET passthrough and Go relayed the daemon's 101,
+# handing the caller the container's stdin. The target is this test
+# container (its hostname is its short ID), so on a proxy without the fix the
+# daemon answers 101, not 404. curl does not speak websocket over http://, so
+# it reports the status and waits for the body until --max-time.
+upgrade_get() {
+  : >"$BODY"
+  out=$(curl -s -o "$BODY" -w '%{http_code}' $TIMEOUT --unix-socket "$PROXY_SOCK" \
+    -H 'Upgrade: websocket' -H 'Connection: Upgrade' -H 'Sec-WebSocket-Version: 13' \
+    -H 'Sec-WebSocket-Key: dGhlIHNhbXBsZSBub25jZQ==' "$1" 2>/dev/null || true)
+  echo "${out:-000}"
+}
+
+S=$(upgrade_get "$PROXY/containers/$(hostname)/attach/ws?stdin=1&stream=1")
+check_denied "GET /containers/*/attach/ws with Upgrade: websocket -> 403 (upgrade refused)" "$S" "$BODY" 'protocol upgrade not allowed'
+
+S=$(get_status "$PROXY/containers/no-such-container/attach/ws")
+check_denied "GET /containers/*/attach/ws -> 403 (attach denied)" "$S" "$BODY" 'attach is not allowed'
+
+S=$(upgrade_get "$PROXY/_ping")
+check_denied "GET /_ping with Upgrade: websocket -> 403 (upgrade refused)" "$S" "$BODY" 'protocol upgrade not allowed'
+
 # ─── Read-only mode (#75) ────────────────────────────────
 
 # The same config behind --readonly. Every request whose method is not GET or

diff --git a/go/internal/proxy/handler.go b/go/internal/proxy/handler.go
@@ -6,6 +6,7 @@ import (
 	"io"
 	"log/slog"
 	"net/http"
+	"strings"
 
 	"github.com/ChainSafe/docker-socket-policy/go/internal/audit"
 	"github.com/ChainSafe/docker-socket-policy/go/internal/middleware"
@@ -32,6 +33,16 @@ func NewHandler(router *Router, chain *middleware.Chain, auditLog *audit.Logger,
 }
 
 func (h *Handler) ServeHTTP(w http.ResponseWriter, r *http.Request) {
+	// 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) {
+		const msg = "protocol upgrade not allowed"
+		slog.Warn("denied", "method", r.Method, "path", r.URL.EscapedPath(), "reason", msg)
+		h.auditLog.Deny(r.Method, r.RequestURI, msg, map[string]interface{}{"method": r.Method, "path": r.URL.EscapedPath()})
+		http.Error(w, msg, http.StatusForbidden)
+		return
+	}
+
 	body, err := io.ReadAll(r.Body)
 	if err != nil {
 		slog.Warn("failed to read request body", "error", err)
@@ -96,3 +107,19 @@ func (h *Handler) ServeHTTP(w http.ResponseWriter, r *http.Request) {
 
 	h.transport.ServeHTTP(w, r)
 }
+
+// isUpgradeRequest reports an Upgrade header, or a Connection header that
+// lists the upgrade token.
+func isUpgradeRequest(h http.Header) bool {
+	if _, ok := h["Upgrade"]; ok {
+		return true
+	}
+	for _, v := range h.Values("Connection") {
+		for _, tok := range strings.Split(v, ",") {
+			if strings.EqualFold(strings.TrimSpace(tok), "upgrade") {
+				return true
+			}
+		}
+	}
+	return false
+}
diff --git a/go/internal/proxy/handler_test.go b/go/internal/proxy/handler_test.go
@@ -377,3 +377,79 @@ container_config:
 		t.Fatalf("ContentLength %d does not match body size %d", rec.lastRequest.ContentLength, len(forwardedBody))
 	}
 }
+
+// #76: any protocol upgrade is refused before the body is read and before
+// routing, so the transport never sees it. Before #76 a websocket attach went
+// through the GET passthrough and Go relayed the daemon's 101.
+func TestHandlerRefusesProtocolUpgrade(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 = "protocol upgrade not allowed"
+
+	tests := []struct {
+		name    string
+		target  string
+		headers map[string]string
+	}{
+		{"websocket", "/containers/json", map[string]string{"Upgrade": "websocket", "Connection": "Upgrade"}},
+		{"connection token only", "/_ping", map[string]string{"Connection": "keep-alive, Upgrade"}},
+		{"upgrade header only", "/_ping", map[string]string{"Upgrade": "h2c"}},
+	}
+	var mismatches []string
+	for _, tt := range tests {
+		rec := &recorderTransport{}
+		h := NewHandler(NewRouter(policyManager), middleware.NewChain(), auditLog, rec)
+		req := httptest.NewRequest("GET", 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")
+		}
+	}
+
+	rec := &recorderTransport{}
+	h := NewHandler(NewRouter(policyManager), middleware.NewChain(), auditLog, rec)
+	w := httptest.NewRecorder()
+	h.ServeHTTP(w, httptest.NewRequest("GET", "/containers/json", nil))
+	if w.Code != http.StatusOK || rec.lastRequest == nil {
+		mismatches = append(mismatches, "plain GET /containers/json: not forwarded")
+	}
+
+	data, err := os.ReadFile(logPath)
+	if err != nil {
+		t.Fatalf("reading audit log: %v", err)
+	}
+	lines := strings.Split(strings.TrimSpace(string(data)), "\n")
+	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[0]), &entry); err != nil {
+		t.Fatalf("audit line 0: %v", err)
+	}
+	if entry.Method != "GET" || entry.URI != "/containers/json" || entry.Decision != "DENY" || entry.Reason != refused {
+		mismatches = append(mismatches, "audit entry: "+lines[0])
+	}
+
+	if len(mismatches) > 0 {
+		t.Fatalf("protocol upgrade mismatches:\n%s", strings.Join(mismatches, "\n"))
+	}
+}
diff --git a/go/internal/proxy/router.go b/go/internal/proxy/router.go
@@ -71,6 +71,10 @@ func (r *Router) Route(method, path string, body map[string]interface{}) *RouteR
 		return &RouteResult{Action: ActionDeny, DenyMsg: "exec is not allowed"}
 	}
 
+	if isAttachPath(path) {
+		return &RouteResult{Action: ActionDeny, DenyMsg: "attach is not allowed"}
+	}
+
 	if strings.HasPrefix(path, "/build") {
 		return &RouteResult{Action: ActionDeny, DenyMsg: "build is not allowed"}
 	}
@@ -216,6 +220,13 @@ func isExecPath(path string) bool {
 	return segs[0] == "exec" || (segs[0] == "containers" && slices.Contains(segs[1:], "exec"))
 }
 
+// isAttachPath matches attach on whole segments after /containers, so a name
+// like attach-runner is not attach (#76).
+func isAttachPath(path string) bool {
+	segs := strings.Split(strings.TrimPrefix(path, "/"), "/")
+	return segs[0] == "containers" && slices.Contains(segs[1:], "attach")
+}
+
 // reservedContainerSegments are Docker endpoints that sit where a container
 // name would: /containers/json lists, /containers/create creates. Treating one
 // as a container name routes the request down the lifecycle path, where an