Skip to content

spec: fix alwaysHostNetwork invariant to be relational, not hardcoded #23

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
abienkowski merged 1 commit into from
Aug 26, 2026
Merged

spec: fix alwaysHostNetwork invariant to be relational, not hardcoded #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
9 changes: 8 additions & 1 deletion spec/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()` |
Expand All @@ -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 |
Expand Down
11 changes: 10 additions & 1 deletion spec/docker_socket_policy.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down