diff --git a/AGENTS.md b/AGENTS.md index 301859c..60b5a47 100644 --- 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: 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`) +- Go: 113 unit tests (main/listener: 24, policy: 10, middleware: 25, proxy: 50, audit: 4) +- Rust: 145 unit tests (main/listener: 23, policy: 15, middleware: 41, proxy: 49, handler: 11, audit: 4, transport: 2) +- TypeScript: 164 unit tests, 1 skipped (flags: 44, listen: 13 incl. 1 skipped concurrency test (#46), middleware: 32, proxy: 36, policy: 10, handler: 15, shutdown: 5, transport: 5, audit: 4) +- Integration, per implementation: 63 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`, `router_pre78` and `router_pre70`) ## 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` (60 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose +- Integration: `make test-integration` (63 test cases) and `make test-integration-sock` (15 socket cases) via Docker Compose ## Contribution Workflow diff --git a/Makefile b/Makefile index ee94473..96b18de 100644 --- a/Makefile +++ b/Makefile @@ -105,6 +105,7 @@ test-spec: $(QUINT) test $(ROUTER_SPEC) --main=router_readonly --match='^readonly.*Test$$' $(QUINT) test $(ROUTER_SPEC) --main=router_pre76 $(QUINT) test $(ROUTER_SPEC) --main=router_pre78 + $(QUINT) test $(ROUTER_SPEC) --main=router_pre70 verify-ts: $(QUINT) run $(SPEC) --max-steps=50 --invariants allInvariants --backend typescript diff --git a/README.md b/README.md index 34f9fbf..6102aa7 100644 --- 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, attach, the read-only passthrough 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, dot 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/) | 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 | +| Go | [go/](go/) | 113 unit + 63 integration + 15 socket | stdlib net/http + yaml.v3 | +| Rust | [rs/](rs/) | 145 unit + 63 integration + 15 socket | tokio, hyper, serde, clap | +| TypeScript | [ts/](ts/) | 164 unit (1 skipped) + 63 integration + 15 socket | Node 22 ESM, built-in http | ### Build All @@ -209,6 +209,7 @@ The chain runs only on container create. `--readonly` is not a gate: the router | Not GET/HEAD | Any (with `--readonly`) | **DENIED** (checked first in the router) | | Any | Path containing `%` | **DENIED** (see below) | | Any | Path containing `//` | **DENIED** | +| Any | Path with a `.` or `..` segment | **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 | @@ -220,12 +221,12 @@ 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 `//`, including `/_ping`, `/version`, `/info`, `/events` | Allowed (read-only) | +| GET/HEAD | Any other path without `%`, `//` or a dot segment, 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. -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. +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. A path with a segment that is exactly `.` or `..` (`/./exec/{id}/json`, `/x/../exec/{id}/json`) is denied the same way, with `dot path segment not allowed`, rather than resolved: the proxy never routes one path and forwards another ([#70](https://github.com/ChainSafe/docker-socket-policy/issues/70)). Names such as `.hidden` or `a.b` are fine, and 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. @@ -448,7 +449,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 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. +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)), dot segments ([#70](https://github.com/ChainSafe/docker-socket-policy/issues/70)), 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 12 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 index d05733e..1a9e8ba 100755 --- a/deploy/test.sh +++ b/deploy/test.sh @@ -510,6 +510,26 @@ check "HEAD /_ping -> 200" "200" "$S" S=$(get_status "$PROXY/events?since=1&until=2") check "GET /events (bounded) -> 200" "200" "$S" +# #70: a . or .. segment is denied for every method, reads included. Before +# #70 the leading . of /./exec/... (or the x of /x/../exec/...) hid the exec +# namespace and the GET passthrough forwarded it; the daemon answered 301 to +# the clean path. --path-as-is stops curl from resolving the dots. +dot_get() { + : >"$BODY" + out=$(curl -s -o "$BODY" -w '%{http_code}' $TIMEOUT --path-as-is --unix-socket "$PROXY_SOCK" \ + "$1" 2>/dev/null || true) + echo "${out:-000}" +} + +S=$(dot_get "$PROXY/./exec/0000000000000000000000000000000000000000000000000000000000000000/json") +check_denied "GET /./exec/*/json -> 403 (dot segment)" "$S" "$BODY" 'dot path segment not allowed' + +S=$(dot_get "$PROXY/x/../exec/0000000000000000000000000000000000000000000000000000000000000000/json") +check_denied "GET /x/../exec/*/json -> 403 (dot segment)" "$S" "$BODY" 'dot path segment not allowed' + +S=$(dot_get "$PROXY/containers/./json") +check_denied "GET /containers/./json -> 403 (dot segment)" "$S" "$BODY" 'dot path segment 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/router.go b/go/internal/proxy/router.go index 8e3a43b..506888e 100644 --- a/go/internal/proxy/router.go +++ b/go/internal/proxy/router.go @@ -57,6 +57,11 @@ func (r *Router) Route(method, path string, body map[string]interface{}) *RouteR return &RouteResult{Action: ActionDeny, DenyMsg: "empty path segment not allowed"} } + // A . or .. segment can hide a denied prefix the same way (#70). + if hasDotSegment(path) { + return &RouteResult{Action: ActionDeny, DenyMsg: "dot path segment not allowed"} + } + path = stripAPIVersion(path) if strings.HasPrefix(path, "/auth") { @@ -210,6 +215,17 @@ func scanDigits(s string, i int) int { return i } +// hasDotSegment reports a segment that is exactly . or ..; names such as +// .hidden or a.b are not dot segments (#70). +func hasDotSegment(path string) bool { + for _, seg := range strings.Split(path, "/") { + if seg == "." || seg == ".." { + return true + } + } + return false +} + // isExecPath matches exec on whole segments, so a name like exec-runner is not exec (#49). func isExecPath(path string) bool { segs := strings.Split(strings.TrimPrefix(path, "/"), "/") diff --git a/go/internal/proxy/router_test.go b/go/internal/proxy/router_test.go index 1bab54a..46bac74 100644 --- a/go/internal/proxy/router_test.go +++ b/go/internal/proxy/router_test.go @@ -860,3 +860,62 @@ allowed_image_prefixes: }) } } + +// TestRouteDotSegments is the cross-language parity guard for #70. +// +// A path with a segment that is exactly . or .. is denied for every method, +// right after the // check and before the API-version strip. Before #70 +// GET /./exec//json had a first segment of ".", so the exec check missed +// it and the GET passthrough forwarded it. Rows mirror the dot* runs in +// spec/router.qnt. +func TestRouteDotSegments(t *testing.T) { + m := newTestManager(t, map[string]string{ + "beacon.yaml": ` +service_name: beacon +allowed_image_prefixes: + - chainsafe/lodestar +`, + }) + r := NewRouter(m) + dot := "dot path segment not allowed" + + tests := []struct { + method string + path string + want Action + wantMsg string + }{ + // dotLeadingExecGetDeniedTest (#70): the leading . hid the exec namespace. + {"GET", "/./exec/abc/json", ActionDeny, dot}, + // dotDotExecGetDeniedTest (#70) + {"GET", "/x/../exec/abc/json", ActionDeny, dot}, + // dotInContainerPathDeniedTest (#70) + {"GET", "/containers/x/./exec", ActionDeny, dot}, + // #70: .. climbing out of the container path. + {"GET", "/containers/x/../../exec/abc/json", ActionDeny, dot}, + // #70: the check runs before the version strip. + {"GET", "/v1.45/./_ping", ActionDeny, dot}, + // #70: every method. + {"DELETE", "/containers/..", ActionDeny, dot}, + {"POST", "/containers/x/./start", ActionDeny, dot}, + // #70: the dot hid the attach deny too. + {"GET", "/containers/./x/attach/ws", ActionDeny, dot}, + // #70 control: names with dots are names. + {"GET", "/containers/.hidden/json", ActionAllow, ""}, + {"GET", "/containers/a.b/json", ActionAllow, ""}, + {"GET", "/containers/.../json", ActionAllow, ""}, + // #70: the // check runs first. + {"GET", "//./_ping", ActionDeny, "empty path segment not allowed"}, + // #70: an encoded dot is denied by the percent check (#53). + {"GET", "/containers/%2e/json", ActionDeny, "percent-encoded path not allowed"}, + } + 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.Errorf("Route(%s, %s) = %v/%q, want %v/%q", + tt.method, tt.path, got.Action, got.DenyMsg, tt.want, tt.wantMsg) + } + }) + } +} diff --git a/rs/src/proxy.rs b/rs/src/proxy.rs index 88ce76b..5a42f19 100644 --- a/rs/src/proxy.rs +++ b/rs/src/proxy.rs @@ -54,6 +54,11 @@ impl Router { return deny("empty path segment not allowed"); } + // A . or .. segment can hide a denied prefix the same way (#70). + if has_dot_segment(path) { + return deny("dot path segment not allowed"); + } + let path = strip_api_version(path); // Denied endpoints @@ -232,6 +237,12 @@ fn strip_api_version(path: &str) -> &str { path } +// A segment that is exactly . or ..; names such as .hidden or a.b are not +// dot segments (#70). +fn has_dot_segment(path: &str) -> bool { + path.split('/').any(|s| s == "." || s == "..") +} + // Exec is matched on whole segments, so a name like exec-runner is not exec (#49). fn is_exec_path(path: &str) -> bool { let mut segs = path.strip_prefix('/').unwrap_or(path).split('/'); @@ -1045,6 +1056,64 @@ mod tests { assert!(mismatches.is_empty(), "mismatches:\n{}", mismatches.join("\n")); } + /// Cross-language parity guard for #70. A path with a segment that is + /// exactly . or .. is denied for every method, right after the // check + /// and before the API-version strip. Before #70 GET /./exec//json + /// had a first segment of ".", so the exec check missed it and the GET + /// passthrough forwarded it. Rows mirror the dot* runs in + /// spec/router.qnt. + #[test] + fn test_route_dot_segments() { + let router = Router::new(make_manager(vec!["alpine"])); + let dot = Some("dot path segment not allowed"); + let cases = [ + // dotLeadingExecGetDeniedTest (#70): the leading . hid the exec namespace. + ("GET", "/./exec/abc/json", Action::Deny, dot), + // dotDotExecGetDeniedTest (#70) + ("GET", "/x/../exec/abc/json", Action::Deny, dot), + // dotInContainerPathDeniedTest (#70) + ("GET", "/containers/x/./exec", Action::Deny, dot), + // #70: .. climbing out of the container path. + ("GET", "/containers/x/../../exec/abc/json", Action::Deny, dot), + // #70: the check runs before the version strip. + ("GET", "/v1.45/./_ping", Action::Deny, dot), + // #70: every method. + ("DELETE", "/containers/..", Action::Deny, dot), + ("POST", "/containers/x/./start", Action::Deny, dot), + // #70: the dot hid the attach deny too. + ("GET", "/containers/./x/attach/ws", Action::Deny, dot), + // #70 control: names with dots are names. + ("GET", "/containers/.hidden/json", Action::Allow, None), + ("GET", "/containers/a.b/json", Action::Allow, None), + ("GET", "/containers/.../json", Action::Allow, None), + // #70: the // check runs first. + ("GET", "//./_ping", Action::Deny, Some("empty path segment not allowed")), + // #70: an encoded dot is denied by the percent check (#53). + ( + "GET", + "/containers/%2e/json", + Action::Deny, + Some("percent-encoded path not allowed"), + ), + ]; + 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 21fe9cc..bbb219f 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 empty interior segment deny, the segment-exact exec deny and `POST /containers/create` route, the segment-exact attach deny, the GET/HEAD-only read passthrough with `/_ping` standing for the read endpoints, 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, #55, #76 and #78), `router_pre48` (Rust's extraction rule before #48), `router_pre53` (Rust and TypeScript before #53, routing on the raw path), `router_pre55` (all three before #55, letting empty interior segments through), `router_readonly` (as `router`, with `--readonly`, #75) `router_pre76` (all three before #76, letting attach through) and `router_pre78` (all three before #78, allowing the read endpoints for every method). 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 dot segment deny, the segment-exact exec deny and `POST /containers/create` route, the segment-exact attach deny, the GET/HEAD-only read passthrough with `/_ping` standing for the read endpoints, 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, #55, #76, #78 and #70), `router_pre48` (Rust's extraction rule before #48), `router_pre53` (Rust and TypeScript before #53, routing on the raw path), `router_pre55` (all three before #55, letting empty interior segments through), `router_readonly` (as `router`, with `--readonly`, #75), `router_pre76` (all three before #76, letting attach through), `router_pre78` (all three before #78, allowing the read endpoints for every method) and `router_pre70` (all three before #70, letting `.` and `..` 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,7 +34,7 @@ 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 seven instances +# Router model: typecheck, run the table tests on all eight instances quint typecheck spec/router.qnt quint test spec/router.qnt --main=router quint test spec/router.qnt --main=router_pre48 @@ -43,6 +43,7 @@ quint test spec/router.qnt --main=router_pre55 quint test spec/router.qnt --main=router_readonly --match='^readonly.*Test$' quint test spec/router.qnt --main=router_pre76 quint test spec/router.qnt --main=router_pre78 +quint test spec/router.qnt --main=router_pre70 # Formal model-checking via Apalache (exhaustive, requires Java) quint verify --max-steps=10 --invariants allInvariants spec/docker_socket_policy.qnt @@ -88,7 +89,7 @@ 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"]`. With `READONLY` set, the read-only check runs before all of these and denies every method other than `GET` and `HEAD`, for every path (#75). The first check in `route` after it 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. With `ALLOW_ANY_METHOD_PING` set, `router_pre78` allows `/_ping` for every method between the second and third checks, as the routers did before #78. 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 denies attach, for every method (#76): when the first segment is `containers` and any later segment is exactly `attach`; `attach-runner` is a name like any other. The fifth 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: +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"]`. With `READONLY` set, the read-only check runs before all of these and denies every method other than `GET` and `HEAD`, for every path (#75). The percent check, first in `route` after it, denies any path with an encoded segment, for every method (#53). The empty-segment check 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. Right after it, any path with a segment that is exactly `.` or `..` is denied, for every method (#70); `.hidden`, `...` and `a.b` are names. With `ALLOW_ANY_METHOD_PING` set, `router_pre78` allows `/_ping` for every method between the dot segment check and the exec check, as the routers did before #78. The exec check 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 attach check denies attach, for every method (#76): when the first segment is `containers` and any later segment is exactly `attach`; `attach-runner` is a name like any other. The create route then sends `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"]`. @@ -98,10 +99,12 @@ A path is a list of raw, still percent-encoded segments with the query string re - `emptyInteriorDenied` holds when every path with an empty segment before the last one is denied. - `emptySegmentsHideNoExec` holds when every path that is an exec path once its empty segments are dropped is denied. - `attachNeverAllowed` holds when every path whose first segment is `containers`, with `attach` at some later segment, is denied. Like `execNeverAllowed`, it writes the positions out instead of calling `isAttachPath`. +- `dotSegmentsDenied` holds when every path with a `.` or `..` segment is denied (#70). +- `dotSegmentsHideNoExec` holds when every path that is an exec or attach path once its dot segments are resolved (`.` dropped; `..` removes the segment before it, if any) is denied. It does not mention `hasDotSegment` or `ALLOW_DOT_SEGMENTS`, so `router_pre70` fails it. - `readPassthroughOnlyForReads` holds when every request routed to the read passthrough (`allowRead`) is a `GET` or a `HEAD` (#78). It does not mention `ALLOW_ANY_METHOD_PING`, so `router_pre78` fails it. - `readonlyAllowsOnlyReads` holds when every request whose method is not `GET` or `HEAD` is denied, for every path. It is the read-only claim and holds only with `READONLY = true`; the router's read-only check, which runs before every other check, denies such requests (#75). -On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames`, `percentSoundTest` asserts `routerSeesWhatDaemonSees`, `execSoundTest` asserts `execNeverAllowed`, `execPrefixSoundTest` asserts `execPrefixNamesRoute`, `createExactSoundTest` asserts `createOnlyExact`, `emptyInteriorSoundTest` asserts `emptyInteriorDenied`, `emptySegmentsHideNoExecTest` asserts `emptySegmentsHideNoExec`, `attachSoundTest` asserts `attachNeverAllowed` and `readPassthroughSoundTest` asserts `readPassthroughOnlyForReads`. +On `router`, `soundTest` asserts `lifecycleOnlyTargetsRealNames`, `percentSoundTest` asserts `routerSeesWhatDaemonSees`, `execSoundTest` asserts `execNeverAllowed`, `execPrefixSoundTest` asserts `execPrefixNamesRoute`, `createExactSoundTest` asserts `createOnlyExact`, `emptyInteriorSoundTest` asserts `emptyInteriorDenied`, `emptySegmentsHideNoExecTest` asserts `emptySegmentsHideNoExec`, `attachSoundTest` asserts `attachNeverAllowed`, `readPassthroughSoundTest` asserts `readPassthroughOnlyForReads` and `dotSoundTest` asserts `dotSegmentsDenied` and `dotSegmentsHideNoExec`. | Row (`run Test`) | Request | Outcome | Instances | |-----|---------|---------|-----------| @@ -164,6 +167,14 @@ Rows for the read endpoints ([#78](https://github.com/ChainSafe/docker-socket-po | `pingGetAllowed` | `GET /_ping` | allow (read) | all | | `pingHeadAllowed` | `HEAD /_ping` | allow (read) | all | +Rows for dot segments ([#70](https://github.com/ChainSafe/docker-socket-policy/issues/70)), all on `router`. The model has at most three segments, so the paths are shortened. The implementations deny these with `dot path segment not allowed`: + +| Row (`run Test`) | Request | Outcome | +|-----|---------|---------| +| `dotLeadingExecGetDenied` | `GET /./exec/abc` | deny | +| `dotDotExecGetDenied` | `GET /mycontainer/../exec` | deny | +| `dotInContainerPathDenied` | `GET /containers/mycontainer/.` | deny | + Rows for `--readonly` ([#75](https://github.com/ChainSafe/docker-socket-policy/issues/75)), all on `router_readonly`, which also runs `readonlySoundTest` (asserts `readonlyAllowsOnlyReads`). The implementations deny these with `read-only mode: requests are not allowed`: | Row (`run Test`) | Request | Outcome | @@ -176,7 +187,7 @@ Rows for `--readonly` ([#75](https://github.com/ChainSafe/docker-socket-policy/i The rows marked "all" above run on every `READONLY = false` instance; `router_readonly` runs only its own `readonly*` tests (`--match='^readonly.*Test$'`), since with the flag on the shared write rows are denied. -Each implementation's router tests use the same row names in comments (added with the #48, #53, #49, #55, #76 and #78 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. `router_pre76` runs `pre76UnsoundTest`, which asserts that `attachNeverAllowed` fails and that `GET /containers/mycontainer/attach` is allowed through the passthrough ([#76](https://github.com/ChainSafe/docker-socket-policy/issues/76)). `router_pre78` runs `pre78UnsoundTest`, which asserts that `readPassthroughOnlyForReads` fails and that `POST /_ping` and `DELETE /_ping` are allowed as reads ([#78](https://github.com/ChainSafe/docker-socket-policy/issues/78)). +Each implementation's router tests use the same row names in comments (added with the #48, #53, #49, #55, #76, #78 and #70 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. `router_pre76` runs `pre76UnsoundTest`, which asserts that `attachNeverAllowed` fails and that `GET /containers/mycontainer/attach` is allowed through the passthrough ([#76](https://github.com/ChainSafe/docker-socket-policy/issues/76)). `router_pre78` runs `pre78UnsoundTest`, which asserts that `readPassthroughOnlyForReads` fails and that `POST /_ping` and `DELETE /_ping` are allowed as reads ([#78](https://github.com/ChainSafe/docker-socket-policy/issues/78)). `router_pre70` runs `pre70UnsoundTest`, which asserts that `dotSegmentsDenied` and `dotSegmentsHideNoExec` fail and that `GET /./exec/abc` is allowed through the passthrough ([#70](https://github.com/ChainSafe/docker-socket-policy/issues/70)). ### Modeling Notes @@ -193,11 +204,12 @@ Two invariants are structurally tautological within the Quint model — they can - **The query string is outside the model.** Paths are segment lists with the query string already removed, so the model says nothing about `%` in the query. The implementations never inspect the query string for this rule; encoded queries such as `?filters=%7B…%7D` are routine and must still be forwarded. That is pinned by the language handler tests and the integration tests, not by the model. - **GET is covered.** The percent check runs before the GET passthrough, and `routerSeesWhatDaemonSees` ranges over `GET` as well as `POST` and `DELETE`. On `router_pre53` the passthrough lets `GET /containers/%2F` through, and the property fails for it too. - **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 `routerSeesWhatDaemonSees` cannot express Go's risk: decoding that differs from the daemon's, such as encoded version segments ([#57](https://github.com/ChainSafe/docker-socket-policy/issues/57)). Go's change is covered by the language handler tests. -- **`router.qnt` is not the full router.** `route` models the read-only check, which runs first in all three routers, the percent check, the empty interior segment check, the exec check, the attach 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 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. +- **`router.qnt` is not the full router.** `route` models the read-only check, which runs first in all three routers, the percent check, the empty interior segment check, the dot segment check, the exec check, the attach 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 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 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. +- **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`. 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. +- **Dot segments are denied, not normalised (#70).** Before #70, `GET /./exec//json` and `GET /x/../exec//json` had a first segment of `.` or `x`, so the exec check did not match and the GET passthrough forwarded them; attach and any other path-based deny could be hidden the same way. The daemon answers such paths with a `301` to the clean path, so nothing leaked, but the router had allowed an exec path. The routers now deny any segment that is exactly `.` or `..`, for every method, right after the `//` check. Normalising the path and routing the result was rejected: the proxy would then route one path and forward another, or have to rewrite it. `dotSegmentsDenied` states the rule and on `router` is close to a tautology, since `route` tests `hasDotSegment` directly. `dotSegmentsHideNoExec` states the security claim: a path that is an exec or attach path once its dot segments are resolved is denied for every method. Both fail on `router_pre70`, and setting `router`'s `ALLOW_DOT_SEGMENTS` to `true` makes `dotSoundTest` and the three `dot*Denied` rows fail. An encoded dot (`%2e`) is already denied by the percent check (#53). The implementations check the path without its query, so `GET /containers/json?filters=a/./b` is still forwarded; that is pinned by the TypeScript router test. - **`--readonly` is a router rule (#75).** Before #75 the flag reached only the middleware chain, and the handler runs the chain only on the create route, so lifecycle `POST`s, `DELETE /containers/{name}` and `POST /images/create` were forwarded in read-only mode. That was handler wiring, not routing, so there is no `pre75` instance: the `READONLY = false` instances are the behaviour without the flag, which before the fix was also the behaviour with it for every route but create. `readonlyAllowsOnlyReads` does not mention `READONLY`, so it is not vacuous: setting `router_readonly`'s `READONLY` to `false` makes `readonlySoundTest` and the three `readonly*Denied` rows fail. `METHODS` has no `PUT`; the implementations' tests cover it. - **Attach is a router rule; the upgrade refusal is not modelled (#76).** Before #76, `GET /containers/{name}/attach/ws` with `Upgrade: websocket` fell through to the GET passthrough, and Go relayed the daemon's `101`, giving the caller the container's stdin. The router now denies `attach` as a whole segment after `containers`, for every method, right after the exec check. As with `/containers/exec/…`, a container literally named `attach` is denied too (`attachNamedContainerDenied`). `attachNeverAllowed` fails on `router_pre76`, and setting `router`'s `ALLOW_ATTACH` to `true` makes `attachSoundTest` and three of the four `attach*` rows fail; `attachPostDenied` is a pin, since the lifecycle branch already denies `POST` when the last segment is not an action. The handler also refuses every request with an `Upgrade` header, or a `Connection` header listing `upgrade`, with `protocol upgrade not allowed`, before routing. That check is on headers, which the model does not have, so like the query string it is pinned by the language handler tests and the integration tests, not by the model. - **The read endpoints admit only `GET` and `HEAD`; the `CONNECT` refusal is not modelled (#78).** Before #78 an early clause in all three routers allowed `/_ping`, `/version`, `/info` and any path starting with `/events` for every method, so `POST /_ping` and `DELETE /version` reached the daemon, and `/eventsxyz` matched too. The clause is gone: `GET` and `HEAD` on those paths reach the read passthrough as before, and every other method falls through to the default deny. `readPassthroughOnlyForReads` fails on `router_pre78`, and setting `router`'s `ALLOW_ANY_METHOD_PING` to `true` makes `readPassthroughSoundTest`, `pingPostDenied` and `pingDeleteDenied` fail. The handlers also refuse every `CONNECT` request with `CONNECT is not allowed` before routing, ahead of the upgrade check; `METHODS` has no `CONNECT`, so that is pinned by the language handler tests and the integration tests, not by the model. diff --git a/spec/router.qnt b/spec/router.qnt index 536482c..d02874e 100644 --- a/spec/router.qnt +++ b/spec/router.qnt @@ -5,8 +5,9 @@ // path deny that runs first in the router (#53), the empty interior segment // deny that follows it (#55), the segment-exact exec deny and // POST /containers/create route (#49), and the segment-exact attach deny -// (#76), and that the read passthrough admits only GET and HEAD, with -// `/_ping` standing for the read endpoints (#78). Mirrors +// (#76), that the read passthrough admits only GET and HEAD, with +// `/_ping` standing for the read endpoints (#78), and the dot segment deny +// that follows the empty interior segment deny (#70). 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 @@ -57,6 +58,12 @@ // other read, and every other method is denied by default. `/_ping` stands // for all four. // +// ALLOW_DOT_SEGMENTS = true models all three before #70, which let a `.` +// or `..` segment through. false models all three after the fix: a path +// with a segment that is exactly `.` or `..` is denied, for every method, +// right after the empty interior segment check. `.hidden`, `...` and `a.b` +// are names like any other. +// // 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 @@ -70,6 +77,7 @@ module router_model { const READONLY: bool const ALLOW_ATTACH: bool const ALLOW_ANY_METHOD_PING: bool + const ALLOW_DOT_SEGMENTS: bool // ─── Daemon decoding ──────────────────────────────────────────────── @@ -144,20 +152,24 @@ module router_model { pure def hasEmptyInterior(segs: List[str]): bool = segs.indices().exists(i => i < segs.length() - 1 and segs[i] == "") + // A segment that is exactly `.` or `..` (#70). + pure def hasDotSegment(segs: List[str]): bool = + segs.indices().exists(i => segs[i] == "." or segs[i] == "..") + pure def isDenied(outcome: str): bool = outcome == "deny" or outcome == "denyExec" // The read-only check (#75) comes first, then the percent check (#53), - // then the empty interior segment check (#55). Before #78 the read - // endpoints were allowed next, for every method. The exec check (#49) - // and the attach check (#76) follow, before - // the create route, the lifecycle branch and the GET passthrough, so it + // then the empty interior segment check (#55), then the dot segment check + // (#70). Before #78 the read endpoints were allowed next, for every method. + // The exec check (#49) and the attach check (#76) follow, 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 (READONLY and not(method == "GET" or method == "HEAD")) "deny" else if (not(ALLOW_PERCENT) and hasEncodedSeg(segs)) "deny" else if (not(ALLOW_EMPTY_INTERIOR) and hasEmptyInterior(segs)) "deny" + else if (not(ALLOW_DOT_SEGMENTS) and hasDotSegment(segs)) "deny" else if (ALLOW_ANY_METHOD_PING and segs == ["_ping"]) "allowRead" else if (isExecPath(segs)) "denyExec" else if (not(ALLOW_ATTACH) and isAttachPath(segs)) "deny" @@ -178,7 +190,7 @@ module router_model { pure val WORDS = Set( "containers", "", "json", "create", "exec", "mycontainer", "beacon", "start", "stop", "%2F", "%2f", "%6A%73%6F%6E", "beacon%2Fstart", - "exec-runner", "abc", "extra", "attach", "ws", "_ping", + "exec-runner", "abc", "extra", "attach", "ws", "_ping", ".", "..", ) pure val METHODS = Set("GET", "HEAD", "POST", "DELETE") @@ -258,6 +270,32 @@ module router_model { isExecPath(segs.select(s => s != "")) implies isDenied(route(m, segs)) )) + // A path with a `.` or `..` segment is denied for every method (#70). + // Ranges over GET too. + pure val dotSegmentsDenied: bool = + METHODS.forall(m => PATHS.forall(segs => + hasDotSegment(segs) implies isDenied(route(m, segs)) + )) + + // The path a client that resolves dot segments reads, as the daemon's + // redirect to the clean path does: `.` is dropped, and `..` removes the + // segment before it, if any, and is dropped. + pure def resolveDots(segs: List[str]): List[str] = + segs.foldl([], (acc, s) => + if (s == ".") acc + else if (s == "..") (if (acc.length() == 0) acc else acc.slice(0, acc.length() - 1)) + else acc.append(s)) + + // The security claim behind dotSegmentsDenied: a path that is an exec or + // attach path once its dot segments are resolved is denied for every + // method (#70). It does not mention hasDotSegment or ALLOW_DOT_SEGMENTS, + // so that router_pre70 fails it. + pure val dotSegmentsHideNoExec: bool = + METHODS.forall(m => PATHS.forall(segs => + (isExecPath(resolveDots(segs)) or isAttachPath(resolveDots(segs))) + implies isDenied(route(m, segs)) + )) + // Every request that is not GET or HEAD is denied, for every path (#75). // The read-only claim: it holds only on `router_readonly`. It does not // mention READONLY, so that the instance with the flag off fails it @@ -278,12 +316,12 @@ module router_model { // ─── Tests: one run per table row ─────────────────────────────────── // // Rows whose outcome depends on none of ALLOW_EMPTY_NAME, ALLOW_PERCENT, - // ALLOW_EMPTY_INTERIOR, ALLOW_ATTACH and ALLOW_ANY_METHOD_PING run on - // every READONLY = false instance. The rows + // ALLOW_EMPTY_INTERIOR, ALLOW_ATTACH, ALLOW_ANY_METHOD_PING and + // ALLOW_DOT_SEGMENTS run on every READONLY = false instance. The rows // that do and the // property tests (soundTest, percentSoundTest, execSoundTest, // execPrefixSoundTest, createExactSoundTest, emptyInteriorSoundTest, - // attachSoundTest, readPassthroughSoundTest) live + // attachSoundTest, readPassthroughSoundTest, dotSoundTest) live // in `router`. `router_readonly` runs only its own `readonly*` tests // (`--match`): with READONLY = true the write rows here are denied. @@ -348,12 +386,12 @@ module router_model { // ─── Instances ────────────────────────────────────────────────────────── -// Go, TypeScript, and Rust after #48, #53, #49, #55, #76 and #78: an empty -// segment is not a name, a percent-encoded path or one with an empty -// interior segment is denied, attach is denied, and the read endpoints are -// read-only. +// Go, TypeScript, and Rust after #48, #53, #49, #55, #76, #78 and #70: an +// empty segment is not a name, a percent-encoded path or one with an empty +// interior segment or a dot segment is denied, attach is denied, and the +// read endpoints are read-only. module router { - import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false, ALLOW_DOT_SEGMENTS = false).* run emptyNameDeleteDeniedTest = assert(route("DELETE", ["containers", ""]) == "deny") @@ -447,6 +485,24 @@ module router { run readPassthroughSoundTest = assert(readPassthroughOnlyForReads) + + // Dot segments (#70). `GET /./exec/abc/json`: the leading `.` hid the + // exec namespace from the exec check. + + run dotLeadingExecGetDeniedTest = + assert(route("GET", [".", "exec", "abc"]) == "deny") + + run dotDotExecGetDeniedTest = + assert(route("GET", ["mycontainer", "..", "exec"]) == "deny") + + run dotInContainerPathDeniedTest = + assert(route("GET", ["containers", "mycontainer", "."]) == "deny") + + run dotSoundTest = + assert(and { + dotSegmentsDenied, + dotSegmentsHideNoExec, + }) } // Rust before #48: `/containers/` and `/containers//start` reach @@ -455,7 +511,7 @@ module router { // 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, ALLOW_EMPTY_INTERIOR = true, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false).* + import router_model(ALLOW_EMPTY_NAME = true, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = true, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false, ALLOW_DOT_SEGMENTS = false).* run pre48UnsoundTest = assert(and { @@ -469,7 +525,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, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = true, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false, ALLOW_DOT_SEGMENTS = false).* run pre53UnsoundTest = assert(and { @@ -485,7 +541,7 @@ module router_pre53 { // 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, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = true, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false, ALLOW_DOT_SEGMENTS = false).* run pre55UnsoundTest = assert(and { @@ -499,7 +555,7 @@ module router_pre55 { // `--match='^readonly.*Test$'`; the shared write rows in router_model assume the // flag is off. module router_readonly { - import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = true, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = true, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false, ALLOW_DOT_SEGMENTS = false).* run readonlySoundTest = assert(readonlyAllowsOnlyReads) @@ -525,7 +581,7 @@ module router_readonly { // and Go relayed the 101, giving the caller the container's stdin. Other // flags as `router`. module router_pre76 { - import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = true, ALLOW_ANY_METHOD_PING = false).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = true, ALLOW_ANY_METHOD_PING = false, ALLOW_DOT_SEGMENTS = false).* run pre76UnsoundTest = assert(and { @@ -538,7 +594,7 @@ module router_pre76 { // `/info` and `/events…` for every method, so `POST /_ping` and // `DELETE /version` reached the daemon. Other flags as `router`. module router_pre78 { - import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = true).* + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = true, ALLOW_DOT_SEGMENTS = false).* run pre78UnsoundTest = assert(and { @@ -547,3 +603,21 @@ module router_pre78 { route("DELETE", ["_ping"]) == "allowRead", }) } + +// All three before #70: a `.` or `..` segment went through. In +// `GET /./exec/abc/json` the first segment is `.`, 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. +// Other flags as `router`. +module router_pre70 { + import router_model(ALLOW_EMPTY_NAME = false, ALLOW_PERCENT = false, ALLOW_EMPTY_INTERIOR = false, READONLY = false, ALLOW_ATTACH = false, ALLOW_ANY_METHOD_PING = false, ALLOW_DOT_SEGMENTS = true).* + + run pre70UnsoundTest = + assert(and { + not(dotSegmentsDenied), + not(dotSegmentsHideNoExec), + route("GET", [".", "exec", "abc"]) == "allowRead", + // The attach half of dotSegmentsHideNoExec, witnessed on its own. + route("GET", [".", "containers", "attach"]) == "allowRead", + }) +} diff --git a/ts/src/proxy.test.ts b/ts/src/proxy.test.ts index 6901e0f..860653a 100644 --- a/ts/src/proxy.test.ts +++ b/ts/src/proxy.test.ts @@ -592,4 +592,50 @@ describe("Router", () => { } assert.deepEqual(mismatches, []); }); + + // Cross-language parity guard for #70. A path with a segment that is + // exactly . or .. is denied for every method, right after the // check and + // before the API-version strip. Before #70 GET /./exec//json had a + // first segment of ".", so the exec check missed it and the GET passthrough + // forwarded it. Rows mirror the dot* runs in spec/router.qnt. + it("denies dot path segments", () => { + const dot = "dot path segment not allowed"; + const cases: [string, string, Action, string | undefined][] = [ + // dotLeadingExecGetDeniedTest (#70): the leading . hid the exec namespace. + ["GET", "/./exec/abc/json", Action.Deny, dot], + // dotDotExecGetDeniedTest (#70) + ["GET", "/x/../exec/abc/json", Action.Deny, dot], + // dotInContainerPathDeniedTest (#70) + ["GET", "/containers/x/./exec", Action.Deny, dot], + // #70: .. climbing out of the container path. + ["GET", "/containers/x/../../exec/abc/json", Action.Deny, dot], + // #70: the check runs before the version strip. + ["GET", "/v1.45/./_ping", Action.Deny, dot], + // #70: every method. + ["DELETE", "/containers/..", Action.Deny, dot], + ["POST", "/containers/x/./start", Action.Deny, dot], + // #70: the dot hid the attach deny too. + ["GET", "/containers/./x/attach/ws", Action.Deny, dot], + // #70 control: names with dots are names. + ["GET", "/containers/.hidden/json", Action.Allow, undefined], + ["GET", "/containers/a.b/json", Action.Allow, undefined], + ["GET", "/containers/.../json", Action.Allow, undefined], + // #70: the // check runs first. + ["GET", "//./_ping", Action.Deny, "empty path segment not allowed"], + // #70: an encoded dot is denied by the percent check (#53). + ["GET", "/containers/%2e/json", Action.Deny, "percent-encoded path not allowed"], + // #70, TS-only: the TS router receives the raw target; the query is not inspected. + ["GET", "/containers/json?filters=a/./b", Action.Allow, undefined], + ]; + 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 63b6885..92a2c0a 100644 --- a/ts/src/proxy.ts +++ b/ts/src/proxy.ts @@ -39,6 +39,8 @@ export class Router { 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" }; + // A . or .. segment can hide a denied prefix the same way (#70). + if (hasDotSegment(cleanPath)) return { action: Action.Deny, denyMsg: "dot path segment not allowed" }; path = stripAPIVersion(cleanPath); // Denied endpoints @@ -135,6 +137,12 @@ function stripAPIVersion(path: string): string { return match ? path.slice(match[0].length - 1) : path; } +// A segment that is exactly . or ..; names such as .hidden or a.b are not +// dot segments (#70). +function hasDotSegment(path: string): boolean { + return path.split("/").some((s) => s === "." || s === ".."); +} + // Exec is matched on whole segments, so a name like exec-runner is not exec (#49). function isExecPath(path: string): boolean { const [first, ...rest] = path.replace(/^\//, "").split("/");