Repository navigation
D13 audit: requires none / opaque on extdeps ops (134 none, 120 opaque; 267 Network) - #12972
Conversation
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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 07b6e25a56
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
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".
|
|
||
| service tmux.Session { | ||
| operation New { | ||
| requires none |
There was a problem hiding this comment.
Mark runtime tmux commands as opaque
inner_argv is appended as tmux's trailing new-session [shell-command], so a caller can supply a program such as curl that opens a non-local connection. Classifying this operation as requires none consequently derives an empty demand for an arbitrary runtime program, unlike the equivalent systemd-run command_argv operations; use requires opaque so callers receive DemandUndecided rather than silently appearing network-free.
Useful? React with 👍 / 👎.
| // carried no readonly marker. The process handler is a realization, not an observation. | ||
| service hostnamectl.Process { | ||
| operation Run { | ||
| requires none |
There was a problem hiding this comment.
Require network for remote-capable hostnamectl arguments
This handler accepts a generic ProcessArgvExpansion, and hostnamectl --help documents -H --host=[USER@]HOST Operate on remote host; supplying that option makes the process open an SSH connection (confirmed locally by its attempted connection to port 22). The service boundary itself does not restrict the expansion to the sealed hostname-setting plan, so requires none under-declares valid inputs and should be replaced with a network requirement or a network-incapable argument type.
Useful? React with 👍 / 👎.
| } | ||
|
|
||
| operation ListUnits { | ||
| requires none |
There was a problem hiding this comment.
Do not classify remote-capable systemctl patterns as local
When pattern is --host=<host>, this exact systemctl list-units ... {pattern} argv treats it as the documented global option -H --host=[USER@]HOST Operate on remote host and attempts an SSH connection, because option parsing continues after the verb. Thus this operation may contact a non-local endpoint despite requires none; either prevent option-shaped patterns with an option terminator/refined type or declare the Network requirement.
Useful? React with 👍 / 👎.
| // string, which is the failure this operation's first consumer exists to catch. | ||
| service sed.Sed { | ||
| operation InPlaceSubstitute { | ||
| requires none |
There was a problem hiding this comment.
Treat executable sed expressions as opaque
GNU sed expressions can contain the e command, which executes a shell command; the installed help explicitly notes that --sandbox disables e/r/w, but this argv does not enable that mode. For example, an expression such as 1e curl … can open a network connection while this operation contributes no demand, so the unrestricted runtime expression must be classified as opaque or constrained to a non-executable substitution representation.
Useful? React with 👍 / 👎.
…56sum get rows as ImportsFixed Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…declarer std.resources (#12960) made the bare read ambiguous; the module calls Filesystem.Write, the extdeps.filesystem.filesystem_io service. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
HOLD at exact head 402ceb4e022f13d6ad86ca38f9bf8dfd6e78f691.
The three-form substrate from #12960, one-clause population, single-authority placement of each verdict on its operation, class-level audit citations, and the incidental provider-import repairs are coherent. Exact-head CI is green. But the population is only mechanically complete: several requires none rows contradict the audit's own fail-closed rule and would let D13 step (b) derive empty demand for an operation that may open a non-local connection or execute runtime-supplied behavior.
P1 — runtime behavior and remote-capable arguments are classified none
-
tmux.Session.Newtakesinner_argv: List<String>and appends it as the command run bytmux new-session. That is a runtime program, the same semantic class this PR correctly marks opaque forsystemd-run command_argvandshell.Exec. It must berequires opaqueunless the input is replaced by a carrier whose admitted program demand is known. -
hostnamectl.Process.Runtakes an unrestrictedProcessArgvExpansionand forwards it afterhostnamectl.hostnamectl -H/--host=operates on a remote host over SSH. The service boundary does not restrict its input to the sealed localset-hostnameplan, sorequires noneis false for admitted inputs. Declare Network or narrow the operation input so remote options are structurally impossible. -
systemd.Systemctl.ListUnitsandListUnitsAllLoadedappend an unrefinedpatternafter the verb and options. A value such as--host=<host>is accepted by systemctl as its remote-host option and uses SSH. Either prevent option-shaped patterns by construction/argv termination or declare Network. -
sed.Sed.InPlaceSubstituteandScriptsSuppressAutoPrintaccept runtime sed programs. GNU sed'secommand ands///eexecute shell commands; these operations do not use--sandbox. Their demand is opaque unless the input becomes a non-executable typed sed subset or sandbox mode is enforced. -
browser.Page.Evaluateandbrowser.Element.EvaluateOnaccept runtime JavaScript. Playwright evaluates it in the page context, where it can callfetch. These are runtime-program inputs and cannot truthfully declare no Network demand; mark them opaque or restrict them to a structurally non-network expression vocabulary.
The first four classes were already reported on the initial 07b6e25 head. The commits after it merge main and repair imports; the exact head still carries the same none rows. The Playwright runtime-expression rows are the same underlying class found by this re-review.
Please correct these rows and re-derive the 520-way partition rather than preserving 236 / 12 / 272 mechanically. The required invariant is one correct declaration per operation, not merely one syntactic clause. D13 step (b) must remain ordered after the corrected population lands.
Non-blocking but worth fixing on the refreshed head: the PR title still says requires Network, and the body is the untouched session-dashboard TODO rather than this PR's none/opaque population and test evidence.
Exact-head floor, generated, emit-build, and witnesses pass. This hold is semantic, not CI-related. No direct merge or check bypass.
…ows (210 none / 19 opaque / 291 Network) Manager rulings (quiet-seal-543, 2026-10-02) on the HOLD review plus the re-audit of all 236 none rows against the two classes the first audit missed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…que, partial-clone git reads Network; NSS boundary (170 none / 29 opaque / 321 Network) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
HOLD at exact head 400fc3eee647e259dcdaffa6f6064666b13a516c.
The five rows from review 5388658399 are corrected, and the wider re-audit of runtime positionals, remote-selecting options, live browser operations, partial-clone reads, title/body, and the 321 Network / 29 opaque / 170 none partition is coherent as far as those classes go. Exact-head CI is green.
P1 — Git commands still marked none execute repository-selected programs
The revised rule now catches a runtime program supplied in an argv argument, but not a runtime program selected from the repository/configuration that is itself the operation's input.
Concrete rows on this exact head:
git.Core.CommitInRepoisrequires noneand executesgit -C {repo} commit -q -m {message}.git.PublicationTransport.RecordCommitandRecordEmptyCommitarerequires noneand executegit commit.
Git's own git-commit documentation says the command can run pre-commit, prepare-commit-msg, commit-msg, post-commit, and post-rewrite hooks. Those are repository/config-selected executables, and can open a non-local connection. The argv here does not disable them; moreover prepare-commit-msg is not suppressed by --no-verify, so merely adding that flag would not close the class.
There is a second direct specimen:
git.Core.AddAllInRepoisrequires noneand executesgit -C {repo} add -A.
Git's gitattributes contract permits repository/config-selected clean and long-running process filter commands, and explicitly notes that git add --all can invoke the process filter. This operation can therefore execute an arbitrary runtime program too.
CheckoutNewBranchInRepo is another likely member: git checkout invokes post-checkout. More generally, this needs a bounded Git re-audit over commands that invoke hooks or external filter drivers, not three isolated clause edits. The repository is not host-wide ambient NSS/DNS: it is the command's selected input, exactly as the partial-clone ruling treats repository state.
Required correction
Add the missing rule: a program selected from an input repository or its Git configuration and executed by the invoked command is OpaqueDemand unless the operation structurally disables that execution surface. Then re-audit the Git rows against upstream hook/filter behavior and re-derive the 520-way partition.
At minimum, the commit and add rows above cannot remain requires none. Either make them requires opaque, or change their realization so hooks/filters are structurally impossible and cite that boundary. Keep D13 step (b) ordered after the corrected population.
This is semantic, not a CI failure. No direct merge or check bypass.
…, drivers, transport helpers, cargo build scripts, npmrc git, agent hooks); 149 none / 91 opaque / 280 Network Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ike its RunArgv siblings Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… toolchain proxies in an input cwd are opaque; 135 none / 119 opaque / 267 Network Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
HOLD at exact head 60e301ddba42e864e20035487d40bee760f32949.
The repository/config-selected execution rule is now stated at the right authority and the Git, Cargo, npm, agent, fsmonitor/index, toolchain-proxy, live-browser, runtime-program, and remote-option populations are coherently re-derived. The prior Git hook/filter hold is resolved. Exact-head CI is green. One P1 remains.
P1 — codex_app_server.Cli.GenerateJsonSchema executes a runtime-selected program but declares requires none
The audit's governing rule says a runtime program supplied in an argument is OpaqueDemand. This operation accepts:
CodexAppServerExecutable { path: FilePath }
and places executable.path directly in argv[0]:
["{executable.path}", "app-server", "generate-json-schema", ...]
Nothing in the type or operation constrains that FilePath to the cited/pinned Codex executable. The adjacent prose says it is the same executable, but the representation admits any program path. A caller can therefore supply an arbitrary executable whose demand is unknown, exactly the class already marked opaque for gunbc.WitnessBin.Run, runtime interpreters, shell.Exec, and the agent operations.
This is also the only dynamic executable-position spelling found under dag/extdeps (argv: ["{...), so it is a bounded correction rather than another open-ended audit class.
Required correction: either:
- change
codex_app_server.Cli.GenerateJsonSchematorequires opaque, update its audit citation, and re-derive the partition (absent another change: 267 Network / 120 opaque / 134 none); or - replace the open
FilePathcarrier with a structurally closed identity that can only denote the pinned Codex executable, and provide the corresponding discriminator.
The operation cannot remain requires none solely because the intended Codex subcommand writes local schema files; the program that is actually executed is still caller-selected.
No direct merge or check bypass.
…ot ImportsFixed; codex GenerateJsonSchema opaque (runtime argv[0]); 134 none / 120 opaque / 267 Network get is a std.algebra profile method with no importable declaration; the pair stopped being derived because the parsed reader does not read it as a bare reference (same as grub.dag and 35 other get rows), not because an import was added. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
APPROVE-MERGE at exact head 0f6bd55b0e1cec9c5bec60f8138fa08dcc43a56f.
The remaining P1 from review 5389618425 is resolved. codex_app_server.Cli.GenerateJsonSchema now declares requires opaque, matching the actual representation: a caller supplies CodexAppServerExecutable.path, and that open FilePath occupies argv[0]. The audit rule and class citation now name this runtime-selected executable explicitly, and the partition is consistently re-derived as 267 Network / 120 opaque / 134 none = 521.
The dashboard correction to the two get roster rows is also right. Neither coreutils_stat.dag nor sha256sum.dag gained an import that could justify ImportsFixed; each still uses get(...), while the roster's own authority defines NotAReference for names the old textual reader mistook for a bare reference and the parsed reader no longer derives. The new dispositions agree with the existing grub.dag#get and other profile-method precedents.
The disclosed gate gap is real: unimported_bare_provider_row_standing checks carriage and file presence but does not prove that an ImportsFixed retirement actually added a provider import. That is a pre-existing follow-up, not a remaining false assertion on this head; the two affected rows now carry the verified cause.
Exact-head floor, generated, emit-build, and witnesses are green. No findings. Merge-queue landing only; the composed merge_group candidate must pass against then-current main. No direct merge or check bypass.
… lane/reference-evidence-consumer Eight conflict hunks in five files, each resolved by keeping this lane's structure and taking main's label constructors inside it: the import unions in resolve/infer/eval, body_lower_callable_arrow and its callers (whose arrow-body edge is now core_edge_label(ArrowBodyEdge)), the fold seam's slot binder under main's LoopCarrierEdge etc., and resolve_match_arm_admitted reading the pattern edge through edge_is_core(MatchArmPatternEdge) as main's inline arm did. #12799 also broke lane code git merged cleanly, swept by grep for every lane-added Named label and every lane-added lookup of a symbol that became a core marker: infer's match-arm reads use find_core_child(MatchArmPatternEdge / MatchArmBodyEdge); variant-tag and pattern-field readers match Authored and give StructuralLabel its own arm (skipped for tags; refused as an unread pattern for fields); infer_where_predicate_set_edge matches Authored with a StructuralLabel arm; three test fixtures build Authored / core labels. No lane-added label match lacks the structural arm, and no lane-added code looks up a core symbol by name. Rebuilt claim_executor, gunbc and claim_batch for this tree (private CARGO_TARGET_DIR): parameter_reference 14/14, callable_binder_slice 9/9, field_projection_stages 24/24. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
D13 Network audit, second half: every
dag/extdepsoperation now carries exactly onerequiresclause (521 of 521;shell.Exec.RunArgvStdinarrived from #12973 and is opaque like its siblings). This PR adds therequires noneandrequires opaquerows; #12965 already landedrequires Network. The selection rule and per-class citations are indocs/plans/d13-network-audit.md; each verdict lives only on its operation's clause.Partition
requires Networkrequires opaquerequires noneRule additions (rulings 2026-10-02, after the HOLD review)
git grep -O).systemctl -H. The exception is when the argv structurally prevents it (--, or the string is an option's value).Reclassified (66 from the first two rounds, then 62 for repository-selected executables)
Manager rulings (7):
tmux.Session.New→ opaque;hostnamectl.Process.Run→ Network;systemd.Systemctl.ListUnits,ListUnitsAllLoaded→ Network;sed.Sed.InPlaceSubstitute,ScriptsSuppressAutoPrint→ opaque;browser.Page.Evaluate,browser.Element.EvaluateOn→ opaque.Re-audit, remote option (16):
systemd.SystemctlEnable,Restart,DisableNow,Start,Stop,ResetFailedUnit,KillUnitTerm,MaskNow,SetProperty,RevertMemoryCaps,IsActive,ShowProperty,ShowUserProperty,ShowLoadState,Status→ Network ({unit}is an unrefined positional before which no--appears).http.Client.PostStdinWithinUnixSocket→ Network ({url}can carry-K/-x).Re-audit, runtime program (2):
git.Inspect.GrepMatchesAtRevision,GrepFixedAtRevision→ opaque (-O<pager>through{pattern}/{ref}).Second rulings (40): live browser page → Network (
Context.Launch,Page.CurrentUrl,Page.Title); runtime positionals to the unverifiableplaywright-runner→ opaque (Context.Close,Page.WaitForSelector,QueryAll,Click,Fill,UploadFile,Screenshot,Wait,Element.IsVisible,InnerText). Git reads that may lazily fetch in a partial clone → Network:git.CoreTrackedWorktreeDiffFromInRepo,Diff,DiffNameOnly,DiffNameOnlyNoRenames,DiffNameOnlyMerge,DiffUnified0,DiffNameStatus,LogPathCommits,Show,RestoreBlobTo,CheckoutNewBranchAtInRepo,CheckoutBranchInRepo,MergeNoEditInRepo,CatFileBlobInRepo,ResetHardInRepo;git.Worktree.Add;git.InspectReadTreeIntoIndex,ListTreePathsAtRevision,ListTreeEntriesAtRevision,MergeTreeWriteTree;git.PlumbingCatFileBlob,CatFileExists,CatFileSize,UnpackObject,ReadTreeIntoIndex,ReadTreeIntoIndexPrefixed,CheckoutIndexToPrefix.Kept
noneby ruling: jqProcess.Run*;rustc.Check.CheckSourceText(fixed argv admits no--extern/-L/-Z);cron.Tab.Replaceandgit.Core.ConfigLocalSet(they store a program but execute nothing). Host resolver configuration (NSS, DNS) is the sandbox's environment, not demand.Third ruling, repository-selected executables → opaque (62; 21 were
none, 41 were Network):git.Core:WriteTreeInRepo,TrackedWorktreeDiffFromInRepo,Diff,DiffUnified0,RestoreBlobTo,AddAllInRepo,CommitInRepo,CheckoutNewBranchInRepo,CheckoutNewBranchAtInRepo,CheckoutBranchInRepo,MergeNoEditInRepo,UpdateRefCompareAndSwapInRepo,ListUntrackedInRepo,ResetHardInRepogit.Worktree.Addgit.Inspect:WorkingTreeStatus,ReadTreeIntoIndex,StatusAgainstIndex,IgnoredAgainstIndex,IgnoredFiles,MergeTreeWriteTreegit.Plumbing:HashObjectWrite,ReadTreeIntoIndex,ReadTreeIntoIndexPrefixed,AddAllIntoIndex,UpdateIndexCacheInfo,WriteTreeFromIndex,CheckoutIndexToPrefix,CreateRefIfAbsent,AdvanceRefIfExpected,DeleteRefIfExpectedgit.PublicationTransport:RecordCommit,RecordEmptyCommitcore.sshCommand,uploadpack,pre-push):git.Core:LsRemoteHeads,FetchNoTags,FetchPrune,LsRemoteRefInRepo,FetchForcedRefInRepo,FetchForcedRefInRepoTrustingSource,PushForcedRefInRepo,PushRefInRepo,PushRefWithLeaseInRepogit.PublicationTransport:PushRefUpdate,PushRefUpdateWithLeasecargo.Buildoperations, includingFmt.npm.CiIgnoreScriptsandIgnoreScriptsOffline(.npmrcgit).claude.Invoke.Run,llm.Anthropic.CliPrompt,llm.Codex.Review.Fourth ruling (27; 14 were
none, 13 Network). Index reads → opaque, because fsmonitor can run on the first index load and:pathrevisions read the index:git.Core:LsFiles,LsFilesUnmergedInRepo,LsFilesStageZPathspecInRepo,LsFilesStageZInRepo,CommitTreeInRepo,RevList,RevParseInRepo,ReflogInRepo,DiffNameOnly,DiffNameOnlyNoRenames,DiffNameOnlyMerge,DiffNameStatus,Show,CatFileBlobInRepogit.Inspect:MergeBase,ResolveRefCommit,ShowTree,ListTreePathsAtRevision,ListTreeEntriesAtRevisiongit.Plumbing:CommitTree,ObserveRef,CatFileBlob,CatFileExists,CatFileSize,UnpackObjectToolchain proxy in an input cwd → opaque:
rustfmt.Parse.Files(rustuprust-toolchain.toml) andtypescript.Compiler.Compile(project.npmrc).cargo --versionandrustc --versiontake no cwd input, so they staynone.Fifth ruling:
codex_app_server.Cli.GenerateJsonSchema→ opaque, because argv[0] is the caller-suppliedCodexAppServerExecutable.path, a runtime-selected program.Narrowing the inputs instead (argv termination, typed sed subset, sandbox) is listed as follow-ups in the doc.
Incidental repairs
GETin the docker inspect/stats modules, and retired thecoreutils_stat.dag#getandsha256sum.dag#getroster rows asNotAReference.ImportsFixed, which was false: neither file imports anything forget.getis astd.algebraprofile method with no importable declaration.get(...)as a bare reference. That is the same cause asgrub.dagand 35 othergetrows.Gate gap (follow-up)
The floor's unimported-bare-provider gate (
v2.workflow.floor_unimported_bare_provider_debtunimported_bare_provider_row_standing) does not catch a falseImportsFixed. A retired row is checked only for not-carried-and-file-present; that check is identical forImportsFixedandNotAReference. So the cause is unverified: no check asks whether the file's imports actually changed to name the provider. TheRosterStalemessage also recommendsImportsFixedunconditionally, which is how the wrong cause was written here. HoldingImportsFixedtrue would need the host to supply, per row, whether the file now imports the pair's provider. Otherwise the gate should name both causes and let the author choose.Filesystemingunbc.runner_microvm_boot_probe. requires none / requires opaque in both seeds; an absent requirements edge is undeclared, not none (D13 ruling B) #12960'sstd.resourcesmade the bare read ambiguous.D13 step (b) stays ordered after this population lands.
🤖 Generated with Claude Code