Repository navigation
Conversation
The first cut's claim that websocat_after is the sole transition authority was true of
the stop-or-continue decision and NOT true of the stage edge. Every driver site matched
`WebsocatContinue { next: _ }` and then ran the stage it was written to expect, so the
order existed twice: once as data in websocat_after, once as a hardcoded call chain.
That permitted a divergence no witness could see. Rewrite an edge -- EnsureDirectory
continuing to Download instead of EnsureOwnership -- and the trace, which follows `next`,
would report the new order while production carried on chowning in the old one. The
never-stops mutation could not catch it: it mutates the stop decision, not the edge.
Raised in side-chat review of #8747, verified here before acting on it (six sites
discarded `next`).
The driver now consults the authority. Each site checks that the stage websocat_after
named is the stage that site implements, and a disagreement REFUSES with both stage
names rather than running the code it happens to have. Comparison goes through
websocat_stage_label because that fold is already the total projection of the stage type;
a second equality over the same coproduct would be the fork this removes.
srv3_websocat_install_from is now one function per stage rather than one function nesting
five matches. That is not tidying: at depth five the guard and the effect it guards were
no longer visible together, which is the condition under which this file's defects have
been introduced twice.
Evidence, by mutation: rewriting the EnsureDirectory edge to Download reddens exactly the
directory-edge witness and the full-chain trace, and leaves the other three edge witnesses
green -- located, not just red. The guard's own negative control (an edge deliberately
compared against a stage no site implements) proves it can answer false at all.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rate ids
The chown that srv3's websocat install performs took its owner as a String composed
as uid + ":" + gid from two raw stdout captures, and ran under a hardcoded
"/usr/bin/sudo" with a bare "-n" at the head of the args list. Both are the
String-as-anemic-modeling class: there was no state in which a bad `id` read could be
noticed, because concatenation always succeeds.
POSIX owns the ids, so extdeps.posix.identity mints PosixUserId, PosixGroupId and
PosixOwnerSpec, and owns the ":" form chown takes. It is not a second spelling of
extdeps.access.posix_effective_principal, which models the principal's NAME as
whoami reports it -- POSIX keeps those two facts apart and so does this.
sudo's calling convention was spelled at four call sites. extdeps.sudo.elevation now
owns it: sudo_elevate takes the argv a command would run unelevated and returns the
elevated invocation, so elevation is a transformation OF an invocation rather than a
second way to spell one. All four "/usr/bin/sudo" literals and all three hand-carried
"-n" prefixes are gone. extdeps.tools.chown and extdeps.tools.mkdir own their argv and
their absolute paths; extdeps.tools.id gains id_binary_path. The absolute paths are
load-bearing rather than pedantry -- a sudoers NOPASSWD rule matches on command path.
The LocalShell arm also stopped reading .stdout raw. It goes through the same trimmed
token shape the ssh arms use, which was a live cross-transport disagreement: `id`
emits a trailing newline, ssh trimmed it and local did not.
DECODING DID NOT BY ITSELF CLOSE THE HOLE, and a witness is what proved it.
integer_lexeme_to_int_optional answers Present { value: 0 } for "", and 0 is root, so
an `id` that printed nothing decoded to the most privileged principal on the host and
was chowned to. The witness asserting that empty text does not decode came back FALSE
on its first run. The decoder now answers its own degenerate cases: empty,
whitespace-only and negative are refused; "0" is admitted, because root is a real
principal. The law is not "zero is invalid" -- it is that only the explicit lexical
representation of zero may construct id zero.
WHAT THIS DOES NOT CLAIM. Ownership is not ensured. This grounds the operands and the
privilege lowering; it does not observe the current owner, does not skip a chown that
is unnecessary, and does not read ownership back afterwards. A successful chown process
is still the only evidence, which is why nothing here is named EnsurePathOwner.
15 witnesses, all measured green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
force-pushed
the
srv3-principal-privilege
branch
from
August 21, 2026 12:13
5454540 to
854b571
Compare
gunbai-bot
Bot
changed the title
Contributor
|
Superseded by #8796, which carries this work unchanged along with the rest of the srv3 stack and the fleet-converge capability binding. Consolidated at the operator's request (too many open PRs). Verified before closing: every declaration, module and witness file this PR introduced is present on Nothing is dropped. Review history stays here; the diff to review is now #8796. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Cut 2a of the srv3 anemic-execution dissolution. Stacked on #8759 (websocat stage-edge binding); #8747 is merged.
The defect
The chown that srv3's websocat install performs took its owner as a String composed as
uid + ":" + gidfrom two raw stdout captures, and ran under a hardcoded"/usr/bin/sudo"with a bare"-n"at the head of the args list.There was no state in which a bad
idread could be noticed, because concatenation always succeeds. Anidthat printed a warning banner, an empty line, or nothing at all still produced a syntactically plausible owner argument for a privileged chown.What this lands
uid + ":" + gidStringextdeps.posix.identity—PosixUserId,PosixGroupId,PosixOwnerSpec, partial decode"/usr/bin/sudo"× 4,"-n"× 3extdeps.sudo.elevation—sudo_elevate(command)extdeps.tools.chown—chown_argv(owner, path)["mkdir", "-p", dir]extdeps.tools.mkdir—mkdir_parents_argv"/usr/bin/id"literalextdeps.tools.id—id_binary_pathElevation is a transformation of an invocation:
sudo_elevatetakes the argv a command would run unelevated. A caller therefore cannot elevate a command it could not otherwise name.extdeps.posix.identityis not a second spelling ofextdeps.access.posix_effective_principal— that models the principal's name aswhoamireports it, deliberately opaque. These are the numeric ids chown's owner argument takes. POSIX keeps the two facts apart andgetpwnamis the mapping; nothing here pretends that mapping is free.The absolute binary paths are load-bearing rather than pedantry: a sudoers NOPASSWD rule matches on command path, so the bare and absolute spellings are different subjects.
A finding: decoding did not by itself close the hole
integer_lexeme_to_int_optionalanswersPresent { value: 0 }for"". Zero is uid 0 — root. So anidthat printed nothing decoded to the most privileged principal on the host and got chowned to.The witness asserting that empty text does not decode came back
falseon its first run. The String predecessor had the same hole from the other direction (an empty capture produced the owner":1000").The decoder now answers its own degenerate cases. The law is not "zero is invalid" — root is a real principal:
"""-1""0""1000","1000\n"The general lesson I am taking: a decode is a wall only if the decoder's own degenerate cases are answered. Otherwise it is a validation that relocates the fabrication into a type, which is worse than the String, because the type now asserts something.
Also fixed: a live cross-transport disagreement
The
LocalShellarm read.stdoutraw while the ssh and fleet arms trimmed.idemits a trailing newline, so the two transports disagreed about what the same command returned, and only one was right. Local now goes through the same trimmed token shape. The gid probe also moved inside the uid arm rather than sitting beside it in a secondlet— both are readonly so the harm is small, but it is the shape that produced this file's two worst defects.What this does NOT claim
Ownership is not ensured. This grounds the operands and the privilege lowering. It does not observe the current owner, does not skip an unnecessary chown, and does not read ownership back afterwards — a successful chown process is still the only evidence. Nothing here is named
EnsurePathOwner, deliberately. That is cut 2b, and per side-chat review it belongs inside a semantic ownership operation (observe → optional mutation → independent readback) rather than as a new outer stage in the websocat walk.Rung, stated honestly
The decoder is the construction path, but
PosixUserId { value: ... }remains a public record constructor, so a caller inside the corpus can still mint one without decoding. This is mechanically preventable, not structurally guaranteed: the invalid state is still writable, and safety depends on the decoder being the route callers take. Constructor confinement is a separate change and belongs with 2b.Evidence
15 witnesses, all measured green, including four that are discriminating REDs for states the predecessor could not represent. The 7 witnesses from the merged sequencing cut and the 5 edge witnesses from #8759 were re-measured green on this combined branch.