Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
1 change: 1 addition & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
15 changes: 8 additions & 7 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 |
Expand All @@ -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.

Expand Down Expand Up @@ -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.

Expand Down
20 changes: 20 additions & 0 deletions deploy/test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 16 additions & 0 deletions go/internal/proxy/router.go
Original file line number Diff line number Diff line change
Expand Up @@ -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") {
Expand Down Expand Up @@ -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, "/"), "/")
Expand Down
59 changes: 59 additions & 0 deletions go/internal/proxy/router_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -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/<id>/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)
}
})
}
}
Loading
Loading