Repository navigation
docker: add the quota supervisor, its tests and its runtime contract - #713
luisleo526 wants to merge 1 commit into
Conversation
Add docker/pf_quota_run.py, the supervisor that runs one command under the launcher-hosted run_quota ledger service and reports a trusted receipt on a descriptor the child never inherits: the ledger verdict, the wait status or signal, the kernel's out-of-memory attribution and the deadline. An absent --deadline-seconds means no expiry and no deadline kill; a present value must be a strict positive finite decimal. A refused memory.events observation is reported as a nullable oom.diagnostic and stays nonfatal. When the interpreter has no os.pidfd_open or signal.pidfd_send_signal (an old C library under a new kernel), the supervisor calls the kernel syscalls (434 and 424, the same numbers on x86_64 and aarch64) through ctypes and raises the same errors; any other architecture keeps the typed refusal. Tests: docker/run_json_quota_supervisor_test.py (129 non-root rows, run by the preflight glob with or without the native pidfd functions), docker/pf_quota_run_privileged_proof.py (176 root rows) and docker/pf_quota_policy_privileged_proof.py (47 root policy rows) run as explicit separate actions. No row has a time limit of its own. The contract is in docs/design/quota-supervisor-runtime-contract.md. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
![github-code-quality[bot]](https://avatars.githubusercontent.com/u/9919?s=60&v=4){kind=small}
| "assertion_id": error.assertion_id, "expected": error.expected, "actual": error.actual, | ||
| }) | ||
| return result_files(directory, result, 1, complete=True) | ||
| except BaseException as error: |
| verdict = "RED" if any(row.get("verdict") == "RED" for row in result["rows"]) else "GREEN" | ||
| result.update(state="COMPLETE", verdict=verdict) | ||
| return result_files(directory, result, 1 if verdict == "RED" else 0, complete=True) | ||
| except BaseException as error: |
| handed_to_serve = True | ||
| q.serve(self.ledger, self.channel, owner) | ||
| return | ||
| except BaseException as error: |
| if owner is not None and not handed_to_serve: | ||
| try: | ||
| self.ledger.disconnect(owner) | ||
| except BaseException as error: |
| self.errors.record(error, "endpoint_disconnect") | ||
| try: | ||
| self.channel.close() | ||
| except BaseException as error: |
![graphify-labs[bot]](https://avatars.githubusercontent.com/in/4356270?s=60&v=4){kind=small}
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 5 advisory finding(s) below merit a look before merge.
Not checked: tests were not run; no formal proof of the changed code.
Graphify review — findings
Adds a root-only policy proof script that runs the shipped supervisor as a subprocess, never importing it, across registered rows: a deliberate-crash recorder control, normal/refusal/cleanup/signal/deadline controls, the refused-path diagnostic rows, and the absent-deadline rows. Each work process gets its own RESULT, completion binding and recorded controller wait, a failed control halts the run, and missing facilities or broken evidence report INCOMPLETE rather than target RED. A name-based guard refuses sensitive paths (.ssh, .aws, .env, and the like) before any read, and output is meant to stay under .policy-author-scratch, but that confinement is checked lexically, so a symlinked parent can still let writes escape it, and forked actors and the traced-run exit status are where the recorded evidence could go wrong.
Worth a look
- new_file scratch-confinement check ignores the symlink-resolved parent, so writes can land outside scratch —
docker/pf_quota_policy_privileged_proof.py:141· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
- mkdir_new scratch-confinement check also bypassable via a symlinked parent —
docker/pf_quota_policy_privileged_proof.py:191· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
- Traced path never sets returncode, so wait() in finally fabricates exit status 0 —
docker/pf_quota_policy_privileged_proof.py· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
- Forked 'reuse' child returns from workload() instead of calling os._exit —
docker/pf_quota_policy_privileged_proof.py· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
- Forked tree actors can unwind into parent code paths when a check fails —
docker/pf_quota_policy_privileged_proof.py:390· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
Review partial — this diff was larger than one review pass covers, so later files were not reviewed; some findings may be missing.
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 287 functions depend on the 286 functions this change touches.
Health — this change adds coupling hotspots:
- new:
_admission()— 12 callers, 6 callees - new:
main()— 1 callers, 16 callees - new:
_exercise_outside_hello()— 2 callers, 8 callees - new:
new_file()— 5 callers, 3 callees - new:
_exercise_shared_endpoints()— 2 callers, 7 callees - new:
worker()— 1 callers, 13 callees - new:
controller()— 1 callers, 12 callees - new:
main()— 1 callers, 11 callees - …and 18 more — each is listed as a finding
Verification — 287 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 287 function(s) in the blast radius were not formally verified this run
Docs that may be stale (advisory)
AGENTS.md§ REQUIRED before claiming any change is done (lines 5-45): references changed symbolsrows,stepAGENTS.md§ Test Commands (lines 66-72): references changed symbolsprepareAGENTS.md§ SOP: adding a runtime PF_API export (CI gate — recurring failure) (lines 73-97): references changed symbolsrunAGENTS.md§ Refactor workers (native-engine programme, R4 and later) (lines 105-141): references changed symbolssourcesCHANGELOG.md§ Unreleased (lines 8-126): references changed symbolsrunCHANGELOG.md§ Closed-trade reads (lines 250-300): references changed symbolsrowsCHANGELOG.md§ Live ledger report-checkpoint layouts (lines 337-344): references changed symbolsrunCHANGELOG.md§ Native live report stream updates (lines 377-441): references changed symbolsrunCHANGELOG.md§ Live ledger resource control (lines 518-537): references changed symbolsrunCHANGELOG.md§ Native live report stream (lines 602-623): references changed symbolsrun
…and 10 more.
· 7 grounded finding(s) anchored inline below; 19 more finding(s) on lines outside this diff (see the check run).
| return read_bytes(path).decode("ascii") | ||
|
|
||
|
|
||
| def new_file(path, data): |
There was a problem hiding this comment.
new_file()
high coupling complexity (Ca·Ce = 15).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| client.close() | ||
|
|
||
|
|
||
| def workload(args, row): |
There was a problem hiding this comment.
workload()
fans out to 9 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return status | ||
|
|
||
|
|
||
| def worker(args, row, directory): |
There was a problem hiding this comment.
worker()
fans out to 13 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return result | ||
|
|
||
|
|
||
| def controller(args, directory): |
There was a problem hiding this comment.
controller()
fans out to 12 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return result_files(directory, result, 2, complete=False) | ||
|
|
||
|
|
||
| def main(): |
There was a problem hiding this comment.
main()
fans out to 11 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| fcntl.fcntl(fd, fcntl.F_SETFL, flags) | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 16 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return int(fields[1]), int(fields[2]), int(fields[3]), int(fields[19]) | ||
|
|
||
|
|
||
| def _admission(*, policy=POLICY, omit=None, overrides=None, |
There was a problem hiding this comment.
_admission()
fans out to 6 callees (efferent coupling); 12 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
What this adds
docker/pf_quota_run.py, the supervisor that runs one command under the launcher-hostedrun_quotaledger service and reports a trusted receipt on a descriptor the child never inherits: the ledger verdict, the wait status or signal, the kernel's out-of-memory attribution and the deadline.--deadline-secondsmeans no expiry and no deadline kill. A present value must be a strict positive finite decimal.memory.eventsobservation is reported as a nullableoom.diagnostic(the existing launcher error envelope, the exact requested path, never opened or created) and stays nonfatal.os.pidfd_openorsignal.pidfd_send_signal(an old C library under a new kernel), the supervisor calls the kernel syscalls (434 and 424, the same numbers on x86_64 and aarch64) through ctypes and raises the same errors. Any other architecture keeps the typedlinux_containment_unavailablerefusal. The native functions are used whenever they exist.docs/design/quota-supervisor-runtime-contract.mdstates the contract.Tests
docker/run_json_quota_supervisor_test.py: 129 non-root rows, collected by the preflight glob. They run with and without the native pidfd functions (eight rows hide them in a real subprocess and check descriptors, errors, signals and the typed refusal against the real kernel).docker/pf_quota_run_privileged_proof.py: 176 root rows, run explicitly on a root host.docker/pf_quota_policy_privileged_proof.py: 47 root policy rows, run explicitly on a root host.No test waits on a clock: waits block on events (EOF, child exit, readable descriptor). The rows that exercise the caller's
--deadline-secondskeep an explicit deadline because the supervisor arms its clock at admission; they assert at most a lower bound on elapsed time.Evidence
pidfd_open, and forpidfd_send_signal) make five and three of them fail.What the root run does and does not show
pf_quota_policy_privileged_proof.py: the controller returns 0 only when every required row ran, none is red and the sources are unchanged); its result file was not copied back, and the 47 rows were not recounted from a file.176 passed.setprivcommand line in the log, not by a printed id. The script's shell is an unprivileged user; the root acts are itssudo -nlines.Review scope
docker/pf_quota_run.py(receipt built from real wait, ledger and cgroup facts; verified privilege drop; gated exec; cleanup by process group, pidfd and subreaper with the pid held bywaitid(WNOWAIT); kernel-credential authentication; no default deadline; no descendant cap).🤖 Generated with Claude Code