Assert mkDevVm token file arguments are paths, never strings #69
No reviewers
Labels
No labels
bug
duplicate
enhancement
help wanted
invalid
question
wontfix
bug
duplicate
enhancement
help wanted
invalid
question
wontfix
No milestone
No project
No assignees
2 participants
Notifications
Due date
No due date set.
Dependencies
No dependencies set
Reference
allod/archetypes!69
Loading…
Reference in a new issue
No description provided.
Delete branch "agent/assert-token-paths"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
This does not stop a dev VM from carrying the whole secrets repository. That already happens today through a different seam, and it still happens after this merges. What this adds is a guard on one specific way it could get worse:
mkDevVmaccepts its two encrypted-token arguments as either a Nix path or a string, and a string can drag a whole repository into a machine's closure. The change refuses a string at the one point every value for those two arguments arrives, and adds two deliberately broken fixtures that prove the guard fires. Nothing about a running machine changes: all three machines produce byte-identical derivations to master. If it is ever wrong, a rebuild stops with a message naming the machine and the argument, and the fix is to spell that value./secrets + "/x.age". The larger leak — every Forge-enabled dev VM already carrying the entire secrets flake — is allod/archetypes#21 and is untouched here, so read this as regression prevention whose benefit stays bounded until #21 lands.What changed
flake.nix,mkDevVm: a newnonPathTokenArgumentsbinding filters{ tokenFile, httpsTokenFile }for values that are neithernullnorbuiltins.isPath, and anassertbetween the builder'sletand itsnixpkgs.lib.nixosSystemcall refuses any that remain. This matches the contractmodules/pi-provider-lifecycle.nixalready enforces for Pi token ciphertexts (badTokenFiles), and the message follows the same shape: it names the machine, the offending argument(s), and the correct form.The assertion reads the effective argument values rather than any one supplier, because that is the single funnel every value for these two arguments passes through:
identity.agentTokenFileandidentity.forgeTokenFile, which the secrets template spells as./secrets + "/…"today;profiles.lib.profileData.<machine>, documented inallod/profilesas "builder-arg overrides merged into that machine's builder call" and empty in the public example, so a private profiles fork can set either argument;machines.<name>.profileminusdefinition, merged into the same builder call atmachineConfigurations;mkDevVmcalls from the checks in this flake.All four land in the formal arguments before the builder body runs, so none of them can bypass the assertion. Note that the
productionPiContractforcing atmachineConfigurationscovers only the four Pi arguments — the token arguments are still overridable from profiles and inventory, which is why the check belongs in the builder rather than at the secrets template.What this does not fix
The option class this assertion protects is not closed by it, and two measured counterexamples are open right now. Both are allod/archetypes#21.
modules/agent-hooks.nix:14-20interpolatesgitPolicySourceper policy file with a bare"${gitPolicySource}/git/…". Measured on this branch:nixosConfigurations.allod-dev.config.home-manager.users.allod.home.file.".config/git/protected-branches".sourceis/nix/store/43y4nc3czj9dbn2pbyndil0hl6ra46fh-source/git/protected-branches, whose string context is the whole secrets flake input, andnix-store --query --requisiteson allod-dev'stopleveldrv contains that store path. So every Forge-enabled dev VM already carries the entire secrets repository, independently of anything this PR does.modules/github-credentials.nix:33setsage.secrets.<name>.file = "${secrets}/${consumer.secret}"— a whole-repository-context string written directly into the very option this assertion is about, from inside a composed module, with nomkForceneeded and no way for a builder-boundary assertion to see it. It is inert in public data becausesecrets.lib.githubCredentialTargetsis{}, but #21 records it as measured on a real deployment.Stated plainly: after this merges,
age.secrets.<name>.fileis not a guarded option class. What is guarded ismkDevVm's two token arguments.String context, measured
The two spellings do not behave alike, which is why the message wording changed in the second commit. With
da directory path:"${d}/a.age"interpolates the directory: context is the whole directory's store path."${d + "/a.age"}"interpolates the file: context is only that one file's store path — the same closure as passing the path.The assertion refuses both anyway. The contract is the value's type, not the spelling, because the leaking form is one keystroke from the safe one and nothing downstream separates them. The message says that instead of claiming, as the first commit did, that every string carries the whole repository.
Witness
Rung 2 of
testing.md: the standing witness is the evaluation assertion itself, so no fixture check re-simulates the property. What thedev-forge-opt-outcheck gains is the sabotage pair that principle 11 requires — proof the validator can fail. It reuses that check's existingwithTokensseam, which already varies only the two token files, so the check's derivation content is unchanged and the new proof is entirely at evaluation time.There are two sabotages rather than one because each defends its own argument's membership in the filtered attrset: with one fixture, deleting
httpsTokenFilefrom the guard would leave the check green. ApathTokenscontrol forces the identical fixture with both values left as paths, so a sabotage failing for an unrelated construction reason cannot read as proof. Neither fixture asserts on message text, so the reword does not touch them.Risk
Low, and the blast radius is evaluation only. The assertion adds nothing to any closure and changes no generated output; the three machines'
system.build.toplevelderivation paths are identical before and after (see Validation). The one behavioural change is that a deploy that today passes a string token file throughprofileDataor an inventory profile setting would stop evaluating instead of building a leaking machine — which is the point, and it fails loudly with an actionable message rather than silently.One narrowing deserves calling out, because it is easy to discover later rather than now. Pure evaluation cannot mint a path value into another flake's tree:
flakeInput + "/x.age"and.outPathare strings, not paths. So after this PR the override seams described above can supply onlynullor a path inside the overriding repo's own tree. A private profiles fork can no longer pointtokenFileat a file in thesecretsinput, and out-of-store runtime strings such as"/persist/…"are refused too. That is security-aligned, and no current caller is affected — every machine and every dev-VM check evaluates green — but it does foreclose part of the flexibility the override seam otherwise offers.The
evaluateshelper in the check forces its fixture only to weak head normal form, deliberately: the guard runs before there is a configuration to evaluate, so forcing deeper would let an unrelated evaluation failure read as proof of the guard.Validation
All commands run in the change worktree with
nix eval --no-write-lock-file; nothing beyond the one small check derivation was built. Everything below was re-run after the second commit's reword.Positive evaluation:
nix eval .#nixosConfigurations.{allod-dev,nexus,privacy-1}.config.system.build.toplevel.drvPath— all three evaluate./nix/store/wwcq3mjn6090671z48vyjjf69snjpnhv-nixos-system-allod-dev-25.11.20260630.b6018f8.drv. Generated output is unchanged.nix eval .#checks.x86_64-linux.<name>.drvPathfor every check that composes a dev VM —dev-forge-opt-out,runtime-module-selection,microvm-credentials,microvm-host-join,agent-vm-status,pi-integration,pi-provider-lifecycle— all evaluate, anddev-forge-opt-out's derivation path is unchanged from master.nix build .#checks.x86_64-linux.dev-forge-opt-outsucceeds.Failure demonstrations, each run against a temporary sabotage and then reverted:
tokenFile ? "${identity.agentTokenFile}"(a string arriving through the default seam) makesnix eval .#nixosConfigurations.allod-dev…drvPathfail witherror: machine 'allod-dev' passes a non-path value to mkDevVm argument(s) tokenFile; each must be null or a Nix path — write ./secrets + "/agent-pr-token.age", not a string. ….httpsTokenFilefails with the same message naminghttpsTokenFile.falsemakesnix eval .#checks.x86_64-linux.dev-forge-opt-out.drvPathfail witherror: dev-forge-opt-out: mkDevVm accepted a string agentTokenFile, so the path-form contract is no longer enforced on that argument.httpsTokenFilefrom the guard's attrset makes the same evaluation fail with theforgeTokenFilevariant. Each sabotage fixture defends its own argument.Supporting measurements:
builtins.getContexton a scratch directory.agent-hooks.nixleak, measured withbuiltins.getContexton the generatedhome.filesource and confirmed withnix-store --query --requisiteson allod-dev's toplevel drv.Not run, and not claimed: no VM was built or booted, and
nix flake checkwas not run in full — evaluating every check attribute in one process was killed for memory on this machine, so the checks above were evaluated one process at a time.Observed, not changed
While reading
dev-forge-opt-outI probed its header claim that "a machine with one but not the other refuses to evaluate". It does not: a fixture withagentTokenFileset andforgeTokenFile = nullevaluates to a fullconfig.age.secrets, and no fixture in the check witnesses that sentence. This matches the secrets template's own comment that the dev builder "treats each file as independently optional and does not check them against each other". The comment is stale, but correcting it is unrelated to this change and is left alone rather than folded in.Closes allod/archetypes#66
The message claimed that every string form carries the whole source repository into the closure. Measured: "${dir}/x.age" does, while "${dir/x.age}" carries only the one file. The rule still refuses both, because the value type is the contract rather than the spelling, but the message now states the rule without asserting a consequence that does not always follow. The two check assertions are reworded the same way. The comment also described a consumed-file carve-out that exists in no public repo; allod/archetypes#21 is unimplemented. It is replaced with the two measured leaks of this shape that this assertion does not reach: agent-hooks.nix interpolating gitPolicySource per policy file, and github-credentials.nix writing an interpolated string straight into age.secrets.<name>.file. Refs allod/archetypes#66An adversarial read-only review ran on a different model and returned "merge with changes — prose only". It re-derived every validation claim in the body independently and all of them held exactly, including the three byte-identical
system.build.toplevelderivation hashes and all four sabotage demonstrations. It also independently confirmed the "observed, not changed" finding about the staledev-forge-opt-outheader comment. The mechanism was not in question; the defects were in how the change described itself. Recording the findings and the responses here.The summary overstated the security benefit. It read as though a string token file were the way a dev VM comes to carry the secrets repository. It is not. The reviewer measured this branch:
nixosConfigurations.allod-dev.config.home-manager.users.allod.home.file.".config/git/protected-branches".sourceis/nix/store/43y4nc3czj9dbn2pbyndil0hl6ra46fh-source/git/protected-branches, whose string context is the whole secrets flake input, and that store path is a requisite of allod-dev's toplevel derivation. The source is the bare"${gitPolicySource}/git/…"interpolations atmodules/agent-hooks.nix:14-20. Every Forge-enabled dev VM already carries the entire secrets repository, and this assertion does not change that. The owner summary now leads with exactly that, and says the benefit is bounded until allod/archetypes#21 lands.A standing counterexample inside the guarded option class was unnamed.
modules/github-credentials.nix:33setsage.secrets.<name>.file = "${secrets}/${consumer.secret}"— a whole-repository-context string written straight into the option this assertion is about, from inside a composed module, needing nomkForceand invisible to a builder-boundary check. It is inert in public data becausesecrets.lib.githubCredentialTargetsis{}, but #21 records it as measured on a real deployment. Without it a reader concludesage.secrets.<name>.fileis now guarded, which it is not. The body has a new "What this does not fix" section naming both leaks and stating plainly that what is guarded ismkDevVm's two token arguments, not the option class.The new code comment described a mechanism that does not exist. The "consumed-file carve-out sweeps
home.fileonly" sentence came from issue #66's own text, but there is nobuiltins.pathcarve-out anywhere in any public repo — #21 is unimplemented. The comment no longer claims it, and now names the two real, measured leaks instead.The assertion message was factually wrong for one string shape. Confirmed with a
builtins.getContextmicro-experiment:"${d}/a.age"carries whole-directory context, while"${d + "/a.age"}"carries only that one file's context — the same closure as passing the path. The assertion refuses both, which is deliberate and conservative, but the old message asserted a consequence that does not always follow. This is the only code change in the second commit. The message now reads:The two check assertions carried the same inaccuracy and were reworded the same way, to "…so the path-form contract is no longer enforced on that argument". Neither fixture asserts on message text, so nothing depended on the old wording, but all four sabotage demonstrations were re-run afterwards and all four still fail with the new messages. Both derivation paths — allod-dev's toplevel and the check — are unchanged by the reword.
A restriction the Risk section understated. Pure evaluation cannot mint a path value into another flake's tree:
flakeInput + "/x.age"and.outPathare strings. So after this PR theprofileDataand inventory override seams can supply onlynullor a path inside the overriding repo's own tree — a private profiles fork can no longer pointtokenFileat a file in thesecretsinput, and out-of-store strings such as"/persist/…"are refused too. Security-aligned, and no current caller is affected, but it narrows the very seam the body cites as the reason the builder is the right boundary, so it now appears under## Riskrather than waiting to be discovered by a private fork.Second commit:
89bac5e. Apart from the assertion message wording, no code moved.