From 43fc44c3aa5e8edb5f08e9cb31eff311f3f5389c Mon Sep 17 00:00:00 2001 From: Adrian Bienkowski Date: Tue, 25 Aug 2026 21:23:59 -0400 Subject: [PATCH] spec: fix alwaysHostNetwork invariant to be relational, not hardcoded MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The invariant literally checked c.networkMode == "host", but all three implementations copy whatever network_mode the matched policy configures into the container's HostConfig — they don't hardcode "host" the way ContainerConfigMutator hardcodes privileged=false. The real security property is: the untrusted create-request body cannot override the operator's policy-configured network mode. Changed the invariant to check networkMode against the matched policy's configured value (same relational pattern as volumesInWhitelist/flagsInAllowlist), rather than a hardcoded literal. Behavior is unchanged under simulation (beacon.yaml still configures network_mode: host), but the invariant now models the actual guarantee instead of an incidental property of the one existing policy file. Also documents in spec/README.md that proxyLives and routingTableComplete are structurally tautological in the model (can't be falsified by any action sequence) and notes what actually provides real coverage for each. Verified: quint typecheck passes; quint run --invariants allInvariants reports no violation (1615 traces/sec, 100-step traces). Part of #5 --- spec/README.md | 9 ++++++++- spec/docker_socket_policy.qnt | 11 ++++++++++- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/spec/README.md b/spec/README.md index 80838fc..13e93ab 100644 --- a/spec/README.md +++ b/spec/README.md @@ -36,7 +36,7 @@ quint verify --max-steps=10 --invariants allInvariants spec/docker_socket_policy | Invariant | What It Checks | Guard / Mutator | |-----------|---------------|-----------------| | `noPrivilegedAccess` | No created container has `privileged=true` | ContainerConfigMutator sets `privileged=false` | -| `alwaysHostNetwork` | All containers use `network_mode: host` | ContainerConfigMutator enforces `networkMode=host` | +| `alwaysHostNetwork` | Every container's network mode matches its policy's configured value (caller cannot override) | ContainerConfigMutator enforces `networkMode` from policy | | `imagesAlwaysAllowed` | All images match an `allowed_image_prefix` | RegistryGate via `nondet` policy match | | `validImagesOnly` | No container has invalid image ref (`InvalidTag`, `InvalidDigest`) | `createContainer` guard rejects invalid variants | | `envOnlyFromFile` | No inline env vars when policy sets `env_file` | EnvFileGate → `envAllowed()` | @@ -50,6 +50,13 @@ quint verify --max-steps=10 --invariants allInvariants spec/docker_socket_policy | `flagsInAllowlist` | All CLI flags pass allowlist + denylist | CmdGate → `flagAllowed()` | | `routingTableComplete` | Every endpoint in the routing table has an explicit action | Explicit `endpointsTable.contains()` check | +### Modeling Notes + +Two invariants are structurally tautological within the Quint model — they can't be falsified by any action sequence the simulator generates, so they don't get real coverage from `quint run`/`quint verify`: + +- **`proxyLives`** — `proxyRunning` is set once in `init` and every action preserves it (`proxyRunning' = proxyRunning`); nothing in the model ever sets it `false`. The real guarantee ("a panic/error on one request doesn't crash the whole proxy") is enforced by language-specific mechanisms outside the model: Go's stdlib `net/http.Server` recovers per-request panics, Rust's `tokio::spawn` isolates panics per connection task, and TypeScript's request handler wraps `handle()` in a `.catch()`. These are exercised by each implementation's own test suite, not by the Quint simulation. +- **`routingTableComplete`** — checks that `endpointsTable` (a fixed constant) contains a fixed list of literals declared in the same file. It documents the intended routing table but doesn't cross-check it against any of the three Router implementations; that comparison has to be done manually (or via `quint-analyzer`) against `go/internal/proxy/router.go`, `rs/src/proxy.rs`, and `ts/src/proxy.ts`. + ### Attack Scenarios Prevented by Invariants | Scenario | Attacker Action | Prevented By | diff --git a/spec/docker_socket_policy.qnt b/spec/docker_socket_policy.qnt index 36852af..b31e1ee 100644 --- a/spec/docker_socket_policy.qnt +++ b/spec/docker_socket_policy.qnt @@ -381,7 +381,16 @@ module docker_socket_policy { val noPrivilegedAccess = containers.forall(c => not(c.privileged)) - val alwaysHostNetwork = containers.forall(c => c.networkMode == "host") + // Every container's network mode is exactly what its matched policy + // configures — the caller cannot override it via the create request. + // (Not a hardcoded "host" check: the security property is that the + // policy YAML controls networkMode, not the untrusted request body.) + val alwaysHostNetwork = containers.forall(c => + policies.exists(p => + p.serviceName == c.serviceName + and c.networkMode == p.containerConfig.networkMode + ) + ) val imagesAlwaysAllowed = containers.forall(c => if (c.imageRef.kind == "valid")