diff --git a/AGENTS.md b/AGENTS.md index a7e4063..c9add1b 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -43,7 +43,7 @@ deploy/ — Docker Compose + integration tests - 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) -- 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`) +- 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 ./...` diff --git a/Makefile b/Makefile index 254b830..d6862fb 100644 --- a/Makefile +++ b/Makefile @@ -101,6 +101,7 @@ test-spec: $(QUINT) test $(ROUTER_SPEC) --main=router $(QUINT) test $(ROUTER_SPEC) --main=router_pre48 $(QUINT) test $(ROUTER_SPEC) --main=router_pre53 + $(QUINT) test $(ROUTER_SPEC) --main=router_pre55 verify-ts: $(QUINT) run $(SPEC) --max-steps=50 --invariants allInvariants --backend typescript diff --git a/README.md b/README.md index a761c94..55c9e51 100644 --- a/README.md +++ b/README.md @@ -205,6 +205,7 @@ docker pull attacker/malware:latest # denied: image not in allowlist | HTTP Method | Path | Action | |-------------|------|--------| | 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 | @@ -215,12 +216,12 @@ docker pull attacker/malware:latest # denied: image not in allowlist | POST | `/auth` | **DENIED** | | POST | `/build` | **DENIED** | | POST | `/commit` | **DENIED** | -| GET/HEAD | Any other path without `%` | Allowed (read-only) | +| GET/HEAD | Any other path without `%` or `//` | 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. -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. +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. ## Configuration diff --git a/deploy/test.sh b/deploy/test.sh index f0e9e9a..a5e3eae 100755 --- a/deploy/test.sh +++ b/deploy/test.sh @@ -386,6 +386,24 @@ check "POST /containers/exec-nosuch/start -> 404 (daemon answered, not proxy 403 S=$(get_status "$PROXY/exec/0000000000000000000000000000000000000000000000000000000000000000/json") check "GET /exec/*/json -> 403 (exec inspect denied)" "403" "$S" +# #55: an empty interior segment is denied for every method. Before #55 the +# empty first segment of //exec/... hid the exec namespace and the GET +# passthrough forwarded it. --path-as-is stops curl from collapsing the //. +S=$(curl -s -o /dev/null -w '%{http_code}' $TIMEOUT --path-as-is --unix-socket "$PROXY_SOCK" \ + "$PROXY//exec/0000000000000000000000000000000000000000000000000000000000000000/json" 2>/dev/null || true) +S="${S:-000}" +check "GET //exec/*/json -> 403 (empty segment)" "403" "$S" + +# #55: an absolute-form request target. Before #55 the TypeScript router saw +# the raw target, whose first segment is "http:", and forwarded exec inspect; +# the daemon answered 404 for this unknown ID (200 with the command line for a +# real one). Go and Rust route on the parsed path. +S=$(curl -s -o /dev/null -w '%{http_code}' $TIMEOUT --unix-socket "$PROXY_SOCK" \ + --request-target "http://docker/exec/0000000000000000000000000000000000000000000000000000000000000000/json" \ + "$PROXY/" 2>/dev/null || true) +S="${S:-000}" +check "GET http://docker/exec/*/json -> 403 (absolute-form target)" "403" "$S" + # ─── Summary ────────────────────────────────────────── echo "" diff --git a/go/internal/proxy/router.go b/go/internal/proxy/router.go index 41ee75a..24b6f15 100644 --- a/go/internal/proxy/router.go +++ b/go/internal/proxy/router.go @@ -40,6 +40,11 @@ func (r *Router) Route(method, path string, body map[string]interface{}) *RouteR return &RouteResult{Action: ActionDeny, DenyMsg: "percent-encoded path not allowed"} } + // An empty interior segment can hide a denied prefix such as /exec (#55). + if strings.Contains(path, "//") { + return &RouteResult{Action: ActionDeny, DenyMsg: "empty path segment not allowed"} + } + path = stripAPIVersion(path) if path == "/_ping" || path == "/version" || path == "/info" || strings.HasPrefix(path, "/events") { diff --git a/go/internal/proxy/router_test.go b/go/internal/proxy/router_test.go index c819e37..39f4cd7 100644 --- a/go/internal/proxy/router_test.go +++ b/go/internal/proxy/router_test.go @@ -508,8 +508,7 @@ allowed_image_prefixes: {"POST", "/containers/%2F/start", ActionDeny}, // percentGetDeniedTest (#53) {"GET", "/containers/%2F", ActionDeny}, - // #53, language-only: HEAD is outside the model's METHODS, but the rule - // covers every method. + // #53, language-only: the rule covers every method, HEAD included. {"HEAD", "/containers/%2F", ActionDeny}, // #53: the check runs on the versioned path too. {"DELETE", "/v1.45/containers/foo%25", ActionDeny}, @@ -608,6 +607,70 @@ allowed_image_prefixes: } } +// TestRouteEmptySegmentsAndHead is the cross-language parity guard for #55. +// +// A path with an empty interior segment (// anywhere in the path) is denied +// for every method, after the percent check and before the API-version strip; +// a single trailing slash is not interior. HEAD on a named container is routed +// like GET. Rows mirror the emptyLeadingExecGetDenied, emptyInteriorGetDenied +// and headNamedContainerAllowed runs in spec/router.qnt. +func TestRouteEmptySegmentsAndHead(t *testing.T) { + m := newTestManager(t, map[string]string{ + "beacon.yaml": ` +service_name: beacon +allowed_image_prefixes: + - chainsafe/lodestar +`, + }) + r := NewRouter(m) + empty := "empty path segment not allowed" + percent := "percent-encoded path not allowed" + exec := "exec is not allowed" + + tests := []struct { + method string + path string + want Action + wantMsg string + }{ + // emptyLeadingExecGetDeniedTest (#55): the leading empty segment hid the exec namespace. + {"GET", "//exec/abc/json", ActionDeny, empty}, + // #55: the empty segment after the version prefix hides the exec namespace too. + {"GET", "/v1.45//exec/abc/json", ActionDeny, empty}, + // #55: the check runs before the version strip. + {"GET", "//v1.45/exec/abc/json", ActionDeny, empty}, + // emptyInteriorGetDeniedTest (#55) + {"GET", "/containers//json", ActionDeny, empty}, + // #55: emptyNameStartDeniedTest (#48) is now decided by the empty segment check. + {"POST", "/containers//start", ActionDeny, empty}, + // #55: an empty name followed by a trailing slash. + {"DELETE", "/containers//", ActionDeny, empty}, + // #55: the read-only endpoints are not exempt. + {"GET", "//_ping", ActionDeny, empty}, + // #55: the percent check runs first. + {"GET", "//containers/%2F", ActionDeny, percent}, + // #55 control: a single trailing slash is not an empty interior segment. + {"GET", "/containers/", ActionAllow, ""}, + // #55 control: the root path. + {"GET", "/", ActionAllow, ""}, + // headNamedContainerAllowedTest (#55) + {"HEAD", "/containers/mycontainer", ActionAllow, ""}, + // #55: HEAD on a container subpath. + {"HEAD", "/containers/mycontainer/json", ActionAllow, ""}, + // #55: the exec check still denies HEAD. + {"HEAD", "/containers/mycontainer/exec", ActionDeny, exec}, + } + for _, tt := range tests { + t.Run(tt.method+" "+tt.path, func(t *testing.T) { + got := r.Route(tt.method, tt.path, nil) + if got.Action != tt.want || got.DenyMsg != tt.wantMsg { + t.Fatalf("Route(%s, %s) = %v/%q, want %v/%q", + tt.method, tt.path, got.Action, got.DenyMsg, tt.want, tt.wantMsg) + } + }) + } +} + func TestExtractContainerNameSkipsEmptySegment(t *testing.T) { for _, path := range []string{"/containers/", "/containers//start"} { if got := extractContainerName(path); got != "" { diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs index 0c1563e..24dbc6c 100644 --- a/rs/src/proxy.rs +++ b/rs/src/proxy.rs @@ -34,6 +34,11 @@ impl Router { return deny("percent-encoded path not allowed"); } + // An empty interior segment can hide a denied prefix such as /exec (#55). + if path.contains("//") { + return deny("empty path segment not allowed"); + } + let path = strip_api_version(path); // Read-only endpoints @@ -81,7 +86,7 @@ impl Router { _ if path.ends_with("/rename") && method == "POST" => deny("rename is not allowed"), _ if path.ends_with("/update") && method == "POST" => deny("update is not allowed"), _ if method == "DELETE" => self.route_by_name(name), - _ if method == "GET" => allow(), + _ if method == "GET" || method == "HEAD" => allow(), _ => deny(&format!("endpoint {} {} is not allowed", method, path)), }; } @@ -618,8 +623,7 @@ mod tests { ("POST", "/containers/%2F/start", Action::Deny), // percentGetDeniedTest (#53) ("GET", "/containers/%2F", Action::Deny), - // #53, language-only: HEAD is outside the model's METHODS, but the rule - // covers every method. + // #53, language-only: the rule covers every method, HEAD included. ("HEAD", "/containers/%2F", Action::Deny), // #53: the check runs on the versioned path too. ("DELETE", "/v1.45/containers/foo%25", Action::Deny), @@ -712,6 +716,64 @@ mod tests { } } + /// Cross-language parity guard for #55. A path with an empty interior + /// segment (// anywhere in the path) is denied for every method, after the + /// percent check and before the API-version strip; a single trailing slash + /// is not interior. HEAD on a named container is routed like GET. Rows + /// mirror the emptyLeadingExecGetDenied, emptyInteriorGetDenied and + /// headNamedContainerAllowed runs in spec/router.qnt. + #[test] + fn test_route_empty_segments_and_head() { + let router = Router::new(make_manager(vec!["alpine"])); + let empty = Some("empty path segment not allowed"); + let percent = Some("percent-encoded path not allowed"); + let exec = Some("exec is not allowed"); + let cases = [ + // emptyLeadingExecGetDeniedTest (#55): the leading empty segment hid the exec namespace. + ("GET", "//exec/abc/json", Action::Deny, empty), + // #55: the empty segment after the version prefix hides the exec namespace too. + ("GET", "/v1.45//exec/abc/json", Action::Deny, empty), + // #55: the check runs before the version strip. + ("GET", "//v1.45/exec/abc/json", Action::Deny, empty), + // emptyInteriorGetDeniedTest (#55) + ("GET", "/containers//json", Action::Deny, empty), + // #55: emptyNameStartDeniedTest (#48) is now decided by the empty segment check. + ("POST", "/containers//start", Action::Deny, empty), + // #55: an empty name followed by a trailing slash. + ("DELETE", "/containers//", Action::Deny, empty), + // #55: the read-only endpoints are not exempt. + ("GET", "//_ping", Action::Deny, empty), + // #55: the percent check runs first. + ("GET", "//containers/%2F", Action::Deny, percent), + // #55 control: a single trailing slash is not an empty interior segment. + ("GET", "/containers/", Action::Allow, None), + // #55 control: the root path. + ("GET", "/", Action::Allow, None), + // headNamedContainerAllowedTest (#55) + ("HEAD", "/containers/mycontainer", Action::Allow, None), + // #55: HEAD on a container subpath. + ("HEAD", "/containers/mycontainer/json", Action::Allow, None), + // #55: the exec check still denies HEAD. + ("HEAD", "/containers/mycontainer/exec", Action::Deny, exec), + ]; + let mut mismatches = Vec::new(); + for (method, path, want, want_msg) in cases { + let got = router.route(method, path, None); + if got.action != want || got.deny_msg.as_deref() != want_msg { + mismatches.push(format!( + "{} {}: got {:?}/{}, want {:?}/{}", + method, + path, + got.action, + got.deny_msg.as_deref().unwrap_or("-"), + want, + want_msg.unwrap_or("-") + )); + } + } + assert!(mismatches.is_empty(), "mismatches:\n{}", mismatches.join("\n")); + } + #[test] fn test_extract_container_name_skips_empty_segment() { for path in ["/containers/", "/containers//start"] { diff --git a/spec/README.md b/spec/README.md index d18a2c1..23a21b2 100644 --- a/spec/README.md +++ b/spec/README.md @@ -9,7 +9,7 @@ This directory contains a [Quint](https://quint-lang.org/) formal specification | `docker_socket_policy.qnt` | Request-handling spec: policy types, state machine, endpoint routing table, 9 invariants (6 P0 / 3 P1), 6 attack scenario simulations | | `listener.qnt` | Listening-socket startup: flag/group selection, existing-path checks, single-instance lock, 6 invariants, one `run` test per design-table row. Instances `listener_locked` (Go, Rust) and `listener_unlocked` (TypeScript) | | `listener-design.md` | Design of the listening socket (dockerd parity) that `listener.qnt` models | -| `router.qnt` | The percent-encoded path deny, the segment-exact exec deny and `POST /containers/create` route, container-name extraction and the container-lifecycle branch of the router only, not the full router. The daemon's percent-decoding as a fixed table. One `run` test per table row. Instances `router` (Go, TypeScript, and Rust after #48, #53 and #49), `router_pre48` (Rust's extraction rule before #48) and `router_pre53` (Rust and TypeScript before #53, routing on the raw path). Every instance includes the #49 exec and create rule, so the pre instances isolate one earlier rule each rather than being full snapshots | +| `router.qnt` | The percent-encoded path deny, the empty interior segment deny, the segment-exact exec deny and `POST /containers/create` route, container-name extraction and the container-lifecycle branch of the router only, not the full router. The daemon's percent-decoding as a fixed table. One `run` test per table row. Instances `router` (Go, TypeScript, and Rust after #48, #53, #49 and #55), `router_pre48` (Rust's extraction rule before #48), `router_pre53` (Rust and TypeScript before #53, routing on the raw path) and `router_pre55` (all three before #55, letting empty interior segments through). Every instance includes the #49 exec and create rule, so the pre instances isolate one earlier rule each rather than being full snapshots | ## How to Run @@ -34,11 +34,12 @@ quint run spec/listener.qnt --main=listener_locked --max-steps=30 --invariant al quint test spec/listener.qnt --main=listener_locked quint test spec/listener.qnt --main=listener_unlocked -# Router model: typecheck, run the table tests on all three instances +# Router model: typecheck, run the table tests on all four instances quint typecheck spec/router.qnt quint test spec/router.qnt --main=router quint test spec/router.qnt --main=router_pre48 quint test spec/router.qnt --main=router_pre53 +quint test spec/router.qnt --main=router_pre55 # Formal model-checking via Apalache (exhaustive, requires Java) quint verify --max-steps=10 --invariants allInvariants spec/docker_socket_policy.qnt @@ -84,15 +85,16 @@ quint run spec/listener.qnt --main=listener_unlocked --max-steps=30 --invariant ### Router path parsing (`router.qnt`) -A path is a list of raw, still percent-encoded segments with the query string removed, so `/containers/` is `["containers", ""]`, `/containers//start` is `["containers", "", "start"]` and `/containers/%2F` is `["containers", "%2F"]`. The first check in `route` denies any path with an encoded segment, for every method (#53). The second denies exec, for every method, as `denyExec` (#49): when the first segment is `exec` (the `/exec//…` namespace), or when the first segment is `containers` and any later segment is exactly `exec`. A segment that only starts with or contains `exec`, such as `exec-runner`, is not matched. The third routes `POST` with exactly the segments `["containers", "create"]` to `routeCreate`; a longer path falls through. After these, the second segment is a container name unless it is empty or one of `create`, `json`, `exec`. Every property checks every method in `GET`, `POST`, `DELETE` against every path of 1 to 3 segments: +A path is a list of raw, still percent-encoded segments with the query string removed, so `/containers/` is `["containers", ""]`, `/containers//start` is `["containers", "", "start"]` and `/containers/%2F` is `["containers", "%2F"]`. The first check in `route` denies any path with an encoded segment, for every method (#53). The second denies any path with an empty segment before the last one, i.e. `//` in the path, for every method (#55); a single trailing slash, as in `/containers/`, is not interior. The third denies exec, for every method, as `denyExec` (#49): when the first segment is `exec` (the `/exec//…` namespace), or when the first segment is `containers` and any later segment is exactly `exec`. A segment that only starts with or contains `exec`, such as `exec-runner`, is not matched. The fourth routes `POST` with exactly the segments `["containers", "create"]` to `routeCreate`; a longer path falls through. After these, the second segment is a container name unless it is empty or one of `create`, `json`, `exec`. `HEAD` is routed like `GET` (#55). Every property checks every method in `GET`, `HEAD`, `POST`, `DELETE` against every path of 1 to 3 segments: - `lifecycleOnlyTargetsRealNames` holds when each lifecycle allow (`allowKnown` or `allowUnknown`) targets a non-empty, non-reserved name. - `routerSeesWhatDaemonSees` holds when every request the router does not deny reads the same to the daemon: decoding leaves its path unchanged. The daemon's decoding is the table `DAEMON_DECODING`: `%2F` and `%2f` decode to `["", ""]` (a `/` splits the segment), `%6A%73%6F%6E` to `["json"]`, and `beacon%2Fstart` to `["beacon", "start"]`. - `execNeverAllowed` holds when every path with `exec` in an exec position is denied. The exec positions are written out in the property, not taken from `route`'s `isExecPath`. - `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. -On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames`, `percentSoundTest` asserts `routerSeesWhatDaemonSees`, `execSoundTest` asserts `execNeverAllowed`, `execPrefixSoundTest` asserts `execPrefixNamesRoute` and `createExactSoundTest` asserts `createOnlyExact`. +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 | |-----|---------|---------|-----------| @@ -129,7 +131,15 @@ Rows for segment-exact exec and create matching ([#49](https://github.com/ChainS | `execNamespacePostDenied` | `POST /exec/abc/start` | deny (exec) | | `createSubpathDenied` | `POST /containers/create/extra` | deny (default, not the create route) | -Each implementation's router tests use the same row names in comments (added with the #48, #53 and #49 fixes). `router_pre48` runs `pre48UnsoundTest`, which asserts that `lifecycleOnlyTargetsRealNames` fails and that both `emptyName*Denied` requests are allowed as an unknown container ([#48](https://github.com/ChainSafe/docker-socket-policy/issues/48)). `router_pre53` runs `pre53UnsoundTest`, which asserts that `routerSeesWhatDaemonSees` fails, that `DELETE /containers/%2F` and `POST /containers/%2F/start` are allowed as an unknown container, and that `GET /containers/%2F` is allowed through the passthrough. +Rows for empty interior segments and HEAD ([#55](https://github.com/ChainSafe/docker-socket-policy/issues/55)): + +| Row (`run Test`) | Request | Outcome | Instances | +|-----|---------|---------|-----------| +| `emptyLeadingExecGetDenied` | `GET //exec/abc` | deny | `router` | +| `emptyInteriorGetDenied` | `GET /containers//json` | deny | `router` | +| `headNamedContainerAllowed` | `HEAD /containers/mycontainer` | allow (read) | all | + +Each implementation's router tests use the same row names in comments (added with the #48, #53, #49 and #55 fixes). `router_pre48` runs `pre48UnsoundTest`, which asserts that `lifecycleOnlyTargetsRealNames` fails and that both `emptyName*Denied` requests are allowed as an unknown container ([#48](https://github.com/ChainSafe/docker-socket-policy/issues/48)). `router_pre53` runs `pre53UnsoundTest`, which asserts that `routerSeesWhatDaemonSees` fails, that `DELETE /containers/%2F` and `POST /containers/%2F/start` are allowed as an unknown container, and that `GET /containers/%2F` is allowed through the passthrough. `router_pre55` runs `pre55UnsoundTest`, which asserts that `emptyInteriorDenied` fails and that `GET //exec/abc` is allowed through the passthrough: its first segment is empty, not `exec`, so the exec check misses it. ### Modeling Notes @@ -149,7 +159,8 @@ Two invariants are structurally tautological within the Quint model — they can - **`router.qnt` is not the full router.** `route` models the percent check, which runs first in all three routers, the exec check, the exact `POST /containers/create` route and the container-lifecycle branch, in that order. It leaves out the API-version strip and the other checks that the routers run before the lifecycle branch, such as the read-only endpoints, auth, and the build and commit denials, as well as `POST /images/create` and the endpoints after the lifecycle branch. For paths that those checks catch, the model's outcome can differ from what an implementation does: `GET /build` is `allowRead` in the model, for example, while the routers deny it as `build is not allowed`. The `images` rows of #49 (`GET /images/exec` allowed, `POST /images/create/extra` denied) are therefore language-only rows, as are `GET /containers/myexec/json` and `DELETE /containers/executor`: the model's words are atoms, so it cannot express a name that merely contains `exec`. Only the properties and the table rows are claims about the code. - **Exec and create match whole segments (#49).** Before #49 the routers disagreed: Go matched `exec` only in the name position (`/containers/exec`), so `DELETE /containers/mycontainer/exec` went down the lifecycle branch and was allowed. Rust matched the substring `/exec` anywhere after `/containers/`, and TypeScript anywhere in the path, so Rust and TypeScript denied containers named `exec-runner` or `executor`. Neither Go nor Rust checked the `/exec/…` namespace, so both let `GET /exec//json` through the GET passthrough. Go also accepted `POST /containers/create/extra` as a container create. In the model the exec check runs before the create route, the lifecycle branch and the GET passthrough, so it denies every method, GET included: exec inspect shows the full command line. `reservedExecDeleteDenied` (`DELETE /containers/exec`) is decided by the exec check, as in all three implementations, and now asserts `denyExec`. `exec` stays in the reserved set, but no row, in the model or in the language tests, would catch it being dropped from there. - **The #49 properties are not vacuous.** None of them is shown on a separate instance; replacing the rule in `route` makes them fail. With a substring-style rule (a segment that starts with `exec`, modeled as the set `exec`, `exec-runner`), `execPrefixSoundTest` and the three `execPrefixName*Allowed` rows fail. With Go's rule before #49 (`exec` only as the second segment under `containers`), `execSoundTest` and the four `exec*Denied` rows fail. `execSubpathPostDenied` and `execNamespacePostDenied` fail there only because the outcome is the default `deny`, not `denyExec`: the request is still refused, as before #49, but not by the exec check. With Go's prefix match for create, `createExactSoundTest` and `createSubpathDenied` fail. `execNeverAllowed` writes out the exec positions itself instead of calling `isExecPath`, so that a narrower `isExecPath` cannot narrow the property with it. -- **HEAD is outside the model.** `METHODS` is `GET`, `POST`, `DELETE`. The real lifecycle branches agree on those three methods only. For `HEAD /containers/x`, Go and TypeScript fall through to the GET/HEAD passthrough and allow it. Rust denies it in the lifecycle branch. +- **HEAD is routed like GET (#55).** `METHODS` is `GET`, `HEAD`, `POST`, `DELETE`. Before #55 the lifecycle branches disagreed on `HEAD /containers/x`: Go and TypeScript fell through to the GET/HEAD passthrough and allowed it, while Rust denied it. All three now allow it like `GET`, and the model's lifecycle branch allows `GET` and `HEAD` alike. +- **Empty interior segments are denied (#55).** Before #55, `GET //exec//json` (and `/v1.45//exec/…`) had an empty first segment, so the exec check did not match and the GET passthrough forwarded it. A live daemon answers such paths with a `301` to the clean path, so nothing leaked, but the router had allowed an exec path. `emptyInteriorDenied` states the rule, and on `router` it is close to a tautology, because `route` tests `hasEmptyInterior` directly. `emptySegmentsHideNoExec` states the security claim: a path that is an exec path once its empty segments are dropped, as the daemon's redirect does, is denied for every method. Both fail on `router_pre55`, and setting `router`'s `ALLOW_EMPTY_INTERIOR` to `true` makes `emptyInteriorSoundTest`, `emptySegmentsHideNoExecTest`, `emptyLeadingExecGetDenied` and `emptyInteriorGetDenied` fail. `router_pre48` keeps the rule off: with it on, `POST /containers//start` is denied before it reaches the name branch, and the instance could no longer show the #48 extraction bug. For the same reason, on `router` the empty-segment check now decides `emptyNameStartDenied`; the #48 extraction stays covered there by `emptyNameDeleteDenied` (a trailing slash) and on `router_pre48`. Dot segments (`/./exec/…`, `/x/../exec/…`) are not modelled and not denied yet (#70); the daemon redirects them to the clean path as it does for `//`. The implementations check for `//` in the path without its query, so `GET /containers/json?filters=a//b` is still forwarded; that is pinned by the TypeScript router test, since Go and Rust route on the path alone. - **Listener fault bias.** `step` crashes an instance on 1 in 10 draws instead of half of all steps, so random runs actually interleave live instances. Every crash stays reachable from every phase, so the reachable state space is unchanged. ### Attack Scenarios Prevented by Invariants diff --git a/spec/router.qnt b/spec/router.qnt index 35a6c67..9bd6f65 100644 --- a/spec/router.qnt +++ b/spec/router.qnt @@ -2,16 +2,16 @@ // // How the router extracts a container name from a request path, how the // container-lifecycle branch routes on it (#48), the percent-encoded -// path deny that runs first in the router (#53), and the segment-exact exec -// deny and POST /containers/create route (#49). Mirrors +// path deny that runs first in the router (#53), the empty interior segment +// deny that follows it (#55), and the segment-exact exec deny and +// POST /containers/create route (#49). Mirrors // `extract_container_name` and the lifecycle branch of `Router::route` in // rs/src/proxy.rs. This is not the full router: the API-version strip and // the other checks that run between the percent check and the lifecycle // branch (build, commit, the read-only endpoints, auth) are left out, as is // POST /images/create. Go (`extractContainerName`) and -// TypeScript (`extractContainerName`) have the same lifecycle branch for -// GET, POST and DELETE. HEAD differs: Go and TypeScript allow it through -// the passthrough, Rust denies it. HEAD is outside METHODS. +// TypeScript (`extractContainerName`) have the same lifecycle branch. +// HEAD is routed like GET in all three (#55). // // A path is a list of raw (still percent-encoded) segments, with the query // string removed: `DELETE /containers/` is ["containers", ""], @@ -31,6 +31,11 @@ // on the raw path and let encoded segments through. false models all three // after the fix: any `%` in the path is denied, for every method. // +// ALLOW_EMPTY_INTERIOR = true models all three before #55, which let an +// empty segment before the last one through. false models all three after +// the fix: a path with `//` in it is denied, for every method. A single +// trailing slash, as in `/containers/`, is not interior. +// // No instance models Go before #53. Go decoded before routing, which is // route(m, decodePath(segs)); with this table that agrees with the daemon // by construction, so the property cannot express Go's risk: decoding that @@ -40,6 +45,7 @@ module router_model { const ALLOW_EMPTY_NAME: bool const ALLOW_PERCENT: bool + const ALLOW_EMPTY_INTERIOR: bool // ─── Daemon decoding ──────────────────────────────────────────────── @@ -102,15 +108,22 @@ module router_model { segs[0] == "containers" and segs.indices().exists(i => i >= 1 and segs[i] == "exec"), } + // An empty segment before the last one, i.e. `//` in the path. A trailing + // empty segment (`/containers/`) is not interior. + pure def hasEmptyInterior(segs: List[str]): bool = + segs.indices().exists(i => i < segs.length() - 1 and segs[i] == "") + pure def isDenied(outcome: str): bool = outcome == "deny" or outcome == "denyExec" - // The percent check (#53) comes first. The exec check (#49) follows, before + // The percent check (#53) comes first, then the empty interior segment + // check (#55). The exec check (#49) follows, before // the create route, the lifecycle branch and the GET passthrough, so it // denies every method. POST /containers/create matches only the exact // segments; a longer path falls through. pure def route(method: str, segs: List[str]): str = if (not(ALLOW_PERCENT) and hasEncodedSeg(segs)) "deny" + else if (not(ALLOW_EMPTY_INTERIOR) and hasEmptyInterior(segs)) "deny" else if (isExecPath(segs)) "denyExec" else if (method == "POST" and segs == ["containers", "create"]) "routeCreate" else if (hasContainerName(segs)) { @@ -118,7 +131,7 @@ module router_model { if (method == "POST" and BY_NAME_ACTIONS.contains(lastSeg(segs))) routeByName(name) else if (method == "POST" and DENIED_ACTIONS.contains(lastSeg(segs))) "deny" else if (method == "DELETE") routeByName(name) - else if (method == "GET") "allowRead" + else if (method == "GET" or method == "HEAD") "allowRead" else "deny" } else if (method == "GET" or method == "HEAD") "allowRead" @@ -131,7 +144,7 @@ module router_model { "%2F", "%2f", "%6A%73%6F%6E", "beacon%2Fstart", "exec-runner", "abc", "extra", ) - pure val METHODS = Set("GET", "POST", "DELETE") + pure val METHODS = Set("GET", "HEAD", "POST", "DELETE") pure val PATHS: Set[List[str]] = WORDS.map(a => [a]) @@ -184,12 +197,28 @@ module router_model { (route(m, segs) == "routeCreate") iff (m == "POST" and segs == ["containers", "create"]) )) + // A path with an empty segment before the last one is denied for every + // method (#55). Ranges over GET too. + pure val emptyInteriorDenied: bool = + METHODS.forall(m => PATHS.forall(segs => + hasEmptyInterior(segs) implies isDenied(route(m, segs)) + )) + + // The security claim behind emptyInteriorDenied: a path that is an exec + // path once its empty segments are dropped, as the daemon's redirect to + // the clean path does, is denied for every method (#55). + pure val emptySegmentsHideNoExec: bool = + METHODS.forall(m => PATHS.forall(segs => + isExecPath(segs.select(s => s != "")) implies isDenied(route(m, segs)) + )) + // ─── Tests: one run per table row ─────────────────────────────────── // - // Rows whose outcome depends on neither ALLOW_EMPTY_NAME nor - // ALLOW_PERCENT run on every instance. The rows that do and the property - // tests (soundTest, percentSoundTest, execSoundTest, execPrefixSoundTest, - // createExactSoundTest) live in `router`. + // Rows whose outcome depends on none of ALLOW_EMPTY_NAME, ALLOW_PERCENT + // and ALLOW_EMPTY_INTERIOR run on every instance. The rows that do and the + // property tests (soundTest, percentSoundTest, execSoundTest, + // execPrefixSoundTest, createExactSoundTest, emptyInteriorSoundTest) live + // in `router`. run emptyNameGetAllowedTest = assert(route("GET", ["containers", ""]) == "allowRead") @@ -235,14 +264,20 @@ module router_model { run createSubpathDeniedTest = assert(route("POST", ["containers", "create", "extra"]) == "deny") + + // HEAD is routed like GET (#55). + + run headNamedContainerAllowedTest = + assert(route("HEAD", ["containers", "mycontainer"]) == "allowRead") } // ─── Instances ────────────────────────────────────────────────────────── -// Go, TypeScript, and Rust after #48, #53 and #49: an empty segment is not a -// name, and a percent-encoded path is denied. +// Go, TypeScript, and Rust after #48, #53, #49 and #55: an empty segment is +// not a name, and a percent-encoded path or one with an empty interior +// segment is denied. module router { - import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false).* run emptyNameDeleteDeniedTest = assert(route("DELETE", ["containers", ""]) == "deny") @@ -286,13 +321,30 @@ module router { run createExactSoundTest = assert(createOnlyExact) + + // Empty interior segments (#55). `GET //exec/abc/json`: the leading empty + // segment hid the exec namespace from the exec check. + + run emptyLeadingExecGetDeniedTest = + assert(route("GET", ["", "exec", "abc"]) == "deny") + + run emptyInteriorGetDeniedTest = + assert(route("GET", ["containers", "", "json"]) == "deny") + + run emptyInteriorSoundTest = + assert(emptyInteriorDenied) + + run emptySegmentsHideNoExecTest = + assert(emptySegmentsHideNoExec) } // Rust before #48: `/containers/` and `/containers//start` reach // route_by_name("") and are allowed as an unknown container. The percent -// check is on, so that this instance isolates #48. +// check is on, so that this instance isolates #48. The empty interior check +// is off: with it on, `/containers//start` would be denied before it reached +// the name branch, and the instance could not show #48. module router_pre48 { - import router_model(ALLOW_EMPTY_NAME = true, ALLOW_PERCENT = false).* + import router_model(ALLOW_EMPTY_NAME = true, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = true).* run pre48UnsoundTest = assert(and { @@ -306,7 +358,7 @@ module router_pre48 { // encoded name such as `%2F` counted as an unknown container and the // request was forwarded. The daemon decodes it and reads a different path. module router_pre53 { - import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = true).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = true, ALLOW_EMPTY_INTERIOR = false).* run pre53UnsoundTest = assert(and { @@ -316,3 +368,18 @@ module router_pre53 { route("GET", ["containers", "%2F"]) == "allowRead", }) } + +// All three before #55: an empty interior segment went through. In +// `GET //exec/abc/json` the first segment is empty, not `exec`, so the exec +// check missed it and the GET passthrough forwarded it. The daemon answers +// with a 301 to the clean path, so nothing leaked, but the router allowed it. +module router_pre55 { + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = true).* + + run pre55UnsoundTest = + assert(and { + not(emptyInteriorDenied), + not(emptySegmentsHideNoExec), + route("GET", ["", "exec", "abc"]) == "allowRead", + }) +} diff --git a/ts/src/proxy.test.ts b/ts/src/proxy.test.ts index 2bec613..c11c7c5 100644 --- a/ts/src/proxy.test.ts +++ b/ts/src/proxy.test.ts @@ -291,8 +291,7 @@ describe("Router", () => { ["POST", "/containers/%2F/start", Action.Deny], // percentGetDeniedTest (#53) ["GET", "/containers/%2F", Action.Deny], - // #53, language-only: HEAD is outside the model's METHODS, but the rule - // covers every method. + // #53, language-only: the rule covers every method, HEAD included. ["HEAD", "/containers/%2F", Action.Deny], // #53: the check runs on the versioned path too. ["DELETE", "/v1.45/containers/foo%25", Action.Deny], @@ -370,4 +369,61 @@ describe("Router", () => { } } }); + + // Cross-language parity guard for #55. A path with an empty interior segment + // (// anywhere in the path) is denied for every method, after the percent + // check and before the API-version strip; a single trailing slash is not + // interior. HEAD on a named container is routed like GET. Rows mirror the + // emptyLeadingExecGetDenied, emptyInteriorGetDenied and + // headNamedContainerAllowed runs in spec/router.qnt. + it("denies empty interior segments and routes HEAD like GET", () => { + const empty = "empty path segment not allowed"; + const percent = "percent-encoded path not allowed"; + const exec = "exec is not allowed"; + const cases: [string, string, Action, string | undefined][] = [ + // emptyLeadingExecGetDeniedTest (#55): the leading empty segment hid the exec namespace. + ["GET", "//exec/abc/json", Action.Deny, empty], + // #55: the empty segment after the version prefix hides the exec namespace too. + ["GET", "/v1.45//exec/abc/json", Action.Deny, empty], + // #55: the check runs before the version strip. + ["GET", "//v1.45/exec/abc/json", Action.Deny, empty], + // emptyInteriorGetDeniedTest (#55) + ["GET", "/containers//json", Action.Deny, empty], + // #55: emptyNameStartDeniedTest (#48) is now decided by the empty segment check. + ["POST", "/containers//start", Action.Deny, empty], + // #55: an empty name followed by a trailing slash. + ["DELETE", "/containers//", Action.Deny, empty], + // #55: the read-only endpoints are not exempt. + ["GET", "//_ping", Action.Deny, empty], + // #55: the percent check runs first. + ["GET", "//containers/%2F", Action.Deny, percent], + // #55 control: a single trailing slash is not an empty interior segment. + ["GET", "/containers/", Action.Allow, undefined], + // #55 control: the root path. + ["GET", "/", Action.Allow, undefined], + // headNamedContainerAllowedTest (#55) + ["HEAD", "/containers/mycontainer", Action.Allow, undefined], + // #55: HEAD on a container subpath. + ["HEAD", "/containers/mycontainer/json", Action.Allow, undefined], + // #55: the exec check still denies HEAD. + ["HEAD", "/containers/mycontainer/exec", Action.Deny, exec], + // #55, TS-only: only the TS router receives the query string (Go and Rust + // route URL.EscapedPath() / uri.path()). A // in the query is not checked. + ["GET", "/containers/json?filters=a//b", Action.Allow, undefined], + // #55, TS-only: the TS router receives the raw request target, so an + // absolute-form target reaches it as-is. Its "//" after the scheme denies + // it; before #55 the first segment "http:" hid exec inspect (v0.3.1-v0.3.3). + ["GET", "http://docker/exec/abc/json", Action.Deny, empty], + ]; + const mismatches: string[] = []; + for (const [method, path, want, wantMsg] of cases) { + const r = router.route(method, path); + if (r.action !== want || r.denyMsg !== wantMsg) { + mismatches.push( + `${method} ${path}: got ${Action[r.action]}/${r.denyMsg ?? "-"}, want ${Action[want]}/${wantMsg ?? "-"}`, + ); + } + } + assert.deepEqual(mismatches, []); + }); }); diff --git a/ts/src/proxy.ts b/ts/src/proxy.ts index d249eb4..95f48a4 100644 --- a/ts/src/proxy.ts +++ b/ts/src/proxy.ts @@ -25,6 +25,8 @@ export class Router { const cleanPath = qmIdx !== -1 ? path.slice(0, qmIdx) : path; // The daemon decodes the path before routing, so deny any escape (#53). if (cleanPath.includes("%")) return { action: Action.Deny, denyMsg: "percent-encoded path not allowed" }; + // An empty interior segment can hide a denied prefix such as /exec (#55). + if (cleanPath.includes("//")) return { action: Action.Deny, denyMsg: "empty path segment not allowed" }; path = stripAPIVersion(cleanPath); // Read-only endpoints