Repository navigation
Quint spec review: verify invariants map to implementation behavior #5
Description
Problem
The Quint formal specification (spec/docker_socket_policy.qnt) is the source of truth for security invariants, but it has not been formally reviewed against the actual guard/mutator behavior in the Go, Rust, and TypeScript implementations.
Solution
Perform a formal review of each invariant and confirm it maps to real code paths in all three implementations:
| Invariant | Go | Rust | TypeScript |
|---|---|---|---|
noPrivilegedAccess (privileged=false enforced) |
ContainerConfigMutator | ? | ? |
alwaysHostNetwork (network_mode=host) |
ContainerConfigMutator | ? | ? |
imagesAlwaysAllowed (allowed_image_prefix) |
RegistryGate | ? | ? |
validImagesOnly (invalid refs rejected) |
createContainer guard | ? | ? |
envOnlyFromFile (no inline env when env_file set) |
EnvFileGate | ? | ? |
proxyLives |
error recovery | ? | ? |
volumesInWhitelist |
MountSourceGate | ? | ? |
flagsInAllowlist |
CmdGate | ? | ? |
routingTableComplete |
Router default-deny | ? | ? |
Also verify:
- All endpoints in the routing table match the specs
endpointsTable - Exec is denied (
execContainerunconditionally returns false) in all three languages - Spec README invariants count (currently says 7, CHANGELOG says 9) is corrected to match reality
Which implementation(s) would this affect?
- Go
- Rust
- TypeScript
- Quint specification
Additional context
- Spec:
spec/docker_socket_policy.qnt(P0 + P1 invariants,allInvariants) - Verification:
make verify/make typecheck/ CI quint job - Tracked by epic First release prep: Quint spec review, test parity, and release pipeline validation #4
Metadata
Metadata
Assignees
Type
Fields
Priority
None yet
Activity
spec: fix alwaysHostNetwork invariant to be relational, not hardcoded (…
abienkowski commentedon Aug 26, 2026
Full review complete (PR #23). Summary of findings:
Invariant mapping (all 9, 6 P0 + 3 P1): 7 of 9 map cleanly and identically to real guard/mutator code in Go, Rust, and TypeScript —
noPrivilegedAccess,imagesAlwaysAllowed,validImagesOnly,envOnlyFromFile,volumesInWhitelist,flagsInAllowlist, and (with caveats below)routingTableComplete.Real gap found and fixed:
alwaysHostNetworkwas a hardcodedc.networkMode == "host"check, but all three implementations actually copy the policy's configured network mode (not a hardcoded "host"). Fixed to be relational, matching thevolumesInWhitelist/flagsInAllowlistpattern — the real property is "caller can't override policy-configured network mode", not "network mode is always the literal string host".Modeling limitations documented (not code gaps):
proxyLivesandroutingTableCompleteare structurally tautological in the Quint model — they can't be falsified by any generated action sequence, soquint run/quint verifydoesn't give them real coverage. The actual guarantees they stand in for are covered by each implementation's own test suite instead (documented in spec/README.md's new "Modeling Notes" section).Routing table: all 26
endpointsTableentries resolve to the correct allow/deny outcome in all three languages. No functional mismatches, though some spec entries map to generic fallthrough rather than explicit per-path handling.Exec denial: confirmed unconditional in all three languages, enforced twice each (router + middleware, defense-in-depth).
Invariant count discrepancy (issue originally noted spec said 7, CHANGELOG said 9): already resolved by PR #13 before this review started — every doc currently says 9.
Follow-up filed separately: #24 — a real cross-language parity bug found along the way (Go's
extractContainerNamedoesn't exclude reserved path segments like Rust/TS do). Out of scope for this review since it's not one of the 9 invariants; tracked independently.Closed by #23.