Repository navigation
fix(host): record the host at create, read a token without host.json as unshared, freeze again - #303
Conversation
…as unshared, freeze again - allocateSession writes host.json for the launched host before the first manifest names it, so a CLI in another pid namespace reads a starting host as unknown instead of dead. - A token program.json without host.json reads as the unshared group: no record names the host's pid space. - stopProgramGroup sends SIGSTOP again at each judgement that reads gone, and sends none when /proc/self does not name this process.
… it by host.json The lifecycle model gains the CreateRecordsHost guard and CliHostAlive, the CLI's view of the host: in another pid space a host that host.json names reads alive, and one that it does not name reads dead. mutant-CreateRecordsHost-otherspace must violate R2. facts.mjs reads the new freeze, the /proc/self check and the host record at create. The docs describe the repeated SIGSTOP and the job-control effect.
|
@codex security review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
@codex review |
|
Codex Review: Didn't find any major issues. Bravo. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…eate # Conflicts: # .agents/skills/verify-session-lifecycle/SKILL.md # .agents/skills/verify-session-lifecycle/coverage.json # .agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla # .agents/skills/verify-session-lifecycle/scripts/check.sh
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…eate # Conflicts: # .agents/skills/verify-session-lifecycle/coverage.json
…eate # Conflicts: # .agents/skills/verify-session-lifecycle/coverage.json
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. Bravo. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…rites host.json before the first manifest
…another pid namespace as unshared #303 verifier: - N1: a host that could not read /proc/<pid>/ns/pid wrote a token without host.json, so destroy of its exited session failed with HOST_TIMEOUT. runHost now records the token only when it wrote host.json. - N3: a CLI in the host's pid namespace whose /proc belongs to another one scanned the wrong /proc and recorded destroyed over a live leftover. inPidNamespace now also needs /proc/self to name this pid, so the group reads unshared there. - N4: src/host/README.md and docs/USAGE.md describe both, the repeated SIGSTOP and the host.json write at create.
The guard facts, the model and check.sh equal those of the last full check (72/72 as expected), so the TLC results do not change.
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. 👍 Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
Why
Three gaps remained after #274, #283 and #291 in how a CLI judges a session's host and program group when it does not share the host's pid space. One of them let
listin another pid namespace record a starting session asfailedand make itscreatefail.Follow-ups of #274 (verifier note N4, refs #262), #291 (the start-up window in the lifecycle skill's Scope) and #283 (advisor follow-ups, refs #244).
What changes for users
Start-up window.
createnow writeshost.jsonfor the new host right after it launches the host, beforesession.jsonnames the host. The host writes it again when it starts. Before,host.jsonappeared only once the host had read its manifest. Alist,inspectorgcin another pid namespace that read the session before that point found no process with the host's pid and recorded the live sessionfailed. Thencreateitself failed. Now such a CLI reads the host asunknown(running) from the first manifest on.A token without
host.json(N4). Aprogram.jsonwith an autogroup token but nohost.jsonnow counts as out of the CLI's pid space. Its group reads as running and gets no signal. Before, a CLI in another pid namespace read such a group as gone, anddestroyrecordeddestroyedwhile a process that the program left still ran. Only unreleased development builds between fix(host): prove the program's group before every destroy kill #221 and fix(host): prove the host pid with a start-up record before reconcile or destroy --force trusts it #260 wrote this state: no tag up to v0.5.0 containsprogramGroup.tsorhostRecord.ts.Freeze (from fix(host): freeze a program group that no scan shows before the proven kill #283).
stopProgramGroupnow sends SIGSTOP again at each judgement that reads the group gone. A member that a SIGCONT from elsewhere resumed inside the window stops again./proc/selfdoes not name this process's pid. Then/procbelongs to another pid namespace, for example afterunshare --pid --forkwithout--mount-proc, and the group id can name the CLI's own group.Job-control side effect (declined, documented). A SIGSTOP to an unrelated group that is a job of an interactive shell makes the shell report the job as stopped. After the SIGCONT the job runs in the background. The session's own group never has a job-control parent, because its parent is the host. A freeze without this effect needs the cgroup freezer or ptrace, which costs more than the case is worth.
docs/USAGE.mdLimits item 3 now says it.A host that cannot record itself records no token (verifier N1). A host that cannot read
/proc/<pid>/ns/pidbut can read the autogroup used to write a token withouthost.json. Thendestroyof its exited session failed withHOST_TIMEOUT.runHostnow records the token only when it wrotehost.json, so a token always comes with a record of its pid space.A
/procof another pid namespace (verifier N3). Main had this gap too. A CLI in the host's pid namespace, but with the/procof another one (nsenter --pidwithout--mount), scanned the wrong/procand recordeddestroyedwhile a leftover ran.inPidNamespacenow also requires/proc/selfto name the CLI's own pid. That view reads the group as unshared, sodestroyfails withHOST_TIMEOUTand sends no signal.No CLI JSON shape changes.
What changes for maintainers
sharesHostPids(sessionDirectory, sharedWithoutRecord): token readers passfalse, thechildPidfallback passestrue. Released sessions have no token and nohost.json, so they keep the old answer.CreateRecordsHostandCliHostAlive, the CLI's view of the host. In another pid space, a host thathost.jsonnames reads alive, and one thathost.jsondoes not name reads dead.destroy --forcekills no host there.mutant-CreateRecordsHost-otherspace, which must violate R2.witness-WitnessUnrecordedHostMeetsKillnow runs without the guard, because a live host without a record is out of reach with it. With the main merges (fix(host): read a terminal session next to the destroy marker as destroyed #284 and fix: create stops its host and names the session on every error of its readiness wait #294), that makes 72 runs and thirty-two guards.facts.mjsreads the host record at create, the new freeze statement andprocShowsOwnPidSpace. It also reads the newsharesHostPidstext.RecordsProgramSyncnow also reads thatrunHostrecords the token only besidehost.json.Validation
8d8d515cadds 4 unit tests, and all 4 fail on main's source.records the host before the first manifest names it: a real child as host, then a reconcile from another pid namespace.reads alive and gets no kill without a host record.stops a group that reads gone again at each of its 5 judgements, then continues it.sends no SIGSTOP when /proc belongs to another pid namespace.writeHostRecord, restoredfrozen ||=, stubbedprocShowsOwnPidSpace, and restoredrecord === null ||. Each one flips its guard to FALSE.check.sh --update-coveragegave 72/72 runs as expected on fdbc191, the merge with fix: create stops its host and names the session on every error of its readiness wait #294.currenthas 24,686,944 distinct states andcurrent-no-tokenhas 24,467,356.check.shequal those of that run, so its results still hold, and I wrotecoverage.jsonfromfacts.mjs.destroy of an exited session whose host could not read its pid namespace ends ok(integration, preloadtest/fixtures/denied-pid-namespace.ts): on 5c3b329 the host recorded a token withouthost.json.reads alive in the host's pid namespace when /proc belongs to another one(unit).records the host before the first manifest names itnow checks thathost.jsonexists whensession.jsonis first renamed into place. It fails when I move the write afterwriteManifest.tsc --noEmit,oxlintandoxfmt --checkpass. Unit: 140 files, 1945 tests. Integration:lifecycle,gc,non-reaping-initandidle-timeout, 75 tests. Under load averages of 45 to 210, two of them hit time-outs in the full run:gc collects exited, failed, and destroyed sessionsanddestroy ends a program whose killed background process stays a zombie. Both passed when I reran them alone.list --allruns insudo unshare --pid --fork --mount-procas the same user:host.jsonwhensession.jsonfirst appearslistin another pid namespacefailedrunningcreateinspectafterwardsfailed, "host process died unexpectedly"runningGenerated with
xum• Model:anthropic:claude-opus-5-5• Thinking:xhigh