Repository navigation
Scoped just-in-time operator token grant: extend WorkflowApprovalState so a credential grant names scope, resource, expiry and consuming attempt - #10010
Conversation
…aming scope, resource, expiry and consuming attempt
An operator approval carried no security content. WorkflowApprovalState's
ApprovalGranted { escalation_id, granted_by } named no access, no resource, no
attempt and no end, so once granted it was a standing credential wearing an
approval's name: a second run reused it, and any action reused it.
std.scoped_authorization is the one carrier for the act an operator actually
performs -- authorize ONE named action, on ONE named resource, for ONE named
attempt, until ONE named instant. Scope is not a new noun: AuthorizationScope is
{ verb, resource, action } over std.effect_grant's Verb and NamespacePosition, so
the prefix relation that already exists is what makes a grant on one secret
version refuse a request for another.
TWO carriers are dissolved into it, not one. std.temporal_effect declared
DurableApprovalGrant -- expiry and single-use modeled, ZERO production consumers
-- beside the production carrier that had neither. One meaning, two names (section 3).
Its intent-hash check also compared with ==, which is fail-open, since
std.content_hash.compare_content_hash deliberately refuses to collapse a
cross-family pair to false; AuthorizationIntentIncomparable is now its own cause.
Refusal is eight located causes, and only ONE of them awaits. NotGranted routes
to StepAwaitingApproval; Expired, AlreadyConsumed, and the escalation/scope/
attempt/intent mismatches all BLOCK. Folding them into the awaiting arm would
make the natural remedy "ask again and it proceeds" -- the absorbing fallback
section 5 names, where the precise deficit disappears and the widened arm succeeds.
Single use is a terminal state with no path back to granted, produced only by
consume_authorization, so a replayed step cannot re-consume by re-reading a flag.
At the live consumer, srv3_boot_once_cd now reads a clock and REFUSES when it
cannot tell whether the grant expired. The source-declared grant reaches only
/redfish/v1/Systems/system/Boot, is bound to one attempt and one planned action,
and ends -- carrying a dissolution row stating that re-dating the constant
satisfies nothing and the out-of-band grant channel is the fix.
The Spark first-boot agreement acceptance is the second instance of this same
shape and needs no new modeling: it is verb Write, a position naming the device's
agreement, action "accept-agreement".
Evidence: whole-closure typecheck of dag/gunbc/srv3/srv3_boot_once_cd.dag reports
0 blocking error(s). Witness coverage is a discriminating pair per claim -- the
same grant runnable before expires_at and refused after, a second attempt refused
with AttemptMismatch, a wider resource refused with ScopeMismatch, a changed
planned action refused with IntentMismatch, and a consumed grant blocked rather
than awaited.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KSJzcs7mrYBcD1Rsca831J
…ake single-use a CAS transition rather than a check
Three corrections from review, each of which changed the shape rather than
polishing it.
1. THE SUBJECT IS PARAMETERIZED, NOT A COPRODUCT. A
`AuthorizationSubject = EulaSubject | SecretSubject | ...` would make the generic
module depend on every consuming domain and require an edit here every time any
lane needs a grant -- a growth surface of one row per consumer. So
AuthorizationRequest<Subject>, OperatorGrant<Subject>,
ScopedAuthorization<Subject>, and the domain owns its Subject. Scope and subject
stay two facts and only the first enforces: AuthorizationScope is typed, closed,
and compared by verb equality plus the namespace prefix relation, and no
decision in std reads the Subject at all.
2. A THIRD CARRIER, FOUND BY REVIEW, FOLDED. gunbc.spark.grant_privileged_operation
declared OperatorBootstrapCredentialLease { host, bootstrap_principal,
administrator, authorized_purpose, attempt_identity } -- the third independent
spelling of this concept. It had independently reached attempt identity and
purpose and was missing expiry, consumption state, and any ENFORCING scope:
authorized_purpose was a sentence built by join(), and a rendered sentence
decides nothing.
It folds to AuthorizationRequest, NOT OperatorGrant, and that distinction is the
honest part: the value is constructed by the RUN, not by an operator, so there is
no granted_by to name and no expiry to carry. Calling it a grant would have
manufactured consent nobody gave. It gains a real scope -- verb Write on the
host's sudoers drop-in position, action posix.sudoers.install -- so a request
against another drop-in now fails the prefix relation instead of passing because
the prose read plausibly. It also settles the parameterization question against
the previous shape: `administrator: SparkCredentialStanding` is a domain payload
that cannot become a NamespacePosition without stringifying it, which that
module's own §3 note already forbids.
3. SINGLE USE IS A TRANSITION, AND THE CHECK IT REPLACES RACED. AuthorizationConsumed
as a state arm plus AlreadyConsumed as a cause validates single use at the
READER: two concurrent runs, or one run restarted after a crash, each read the
same valid grant, each observe "not yet consumed", and each proceed. So
consumption is now AuthorizationClaimState = Unclaimed | ClaimedBy | CompletedBy
| AbortedBy, moved through std.durable_compare_and_set -- whose losing arm IS the
concurrent-claim refusal, and whose CasPreconditionFailed carries both sides so a
loser can tell "another attempt claimed this" from "I addressed the wrong slot".
Hand-rolling a second race resolver beside that module would have been the fork
this change exists to remove. An unreadable claim slot refuses: "we could not
tell whether anyone holds this" is not evidence that nobody does.
AbortedBy is distinct from CompletedBy because the remedies differ -- an aborted
attempt may warrant re-issuing a grant and a completed one never does.
Evidence: whole-closure typecheck of dag/gunbc/srv3/srv3_boot_once_cd.dag and of
dag/gunbc/spark/grant_privileged_operation.dag both report 0 blocking error(s).
New discriminating witnesses: a grant held by a different attempt refuses while
the holder's own attempt still proceeds (the pair, since a check refusing
everyone would pass either half alone); a CAS loser reads the winner's identity
out of its own outcome; an unreadable claim store yields ClaimUndecided rather
than either verdict.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…at guards it discriminate Review found the intent hash was `content_hash_of_value` over a hand-authored string, "srv3-boot-source-override-cd-once-uefi+force-restart" -- a nickname for what Srv3BootOverrideSubject already carries structurally. Editing srv3_boot_cd_reset_type to ResetGracefulRestart would have changed the planned action while leaving the hash identical, so AuthorizationIntentMismatch could never fire for the one class it is named after. Permanently green by construction, which section 4b calls worse than absent because it gets cited as coverage. The hash is now derived from the subject via the cited Redfish wire projections -- the same total renderings the PATCH body is built from -- so it moves exactly when the bytes that reach the BMC move. THE REVIEW ALSO INDICTS THE WITNESS THAT WAS SUPPOSED TO GUARD THIS, and that is the more serious half. srv3_grant_refuses_a_changed_planned_action supplied a different string LITERAL as the changed hash, so it passed whether or not the hash was derived from anything: it discriminated the literal, not the wall. It now computes the changed hash from a subject differing in exactly one field, so it reds the moment the derivation stops depending on the subject. Added srv3_intent_hash_moves_with_every_subject_field, per field rather than in aggregate: an aggregate "some mutation changes it" is satisfied by a hash reading only ONE field, which is the degenerate shape the literal had. Four one-field mutations plus a positive control that the same subject hashes the same -- without the control, every "differs" conjunct would be satisfied by a hash that never agrees with itself. Evidence: whole-closure typecheck of dag/gunbc/srv3/srv3_boot_once_cd.dag reports 0 blocking error(s). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…nsumed DCH-1 cohort required-witnesses-floor refused at 78051a5 with `namespace-wave-admission (4 unadjudicated delta(s))`: moving srv3_boot_cd_target/enabled/mode/reset_type into gunbc.srv3_os_install_actuate_workflow re-points four bindings inside srv3_boot_once_cd_resolved. Each is a TargetChanged binding on a declaration that was neither renamed nor minted, so each gets an exact row naming the (module, declaration, spelling) triple, and a fifth re-pointed binding anywhere in the corpus still refuses. The same run reported the nine DCH-1 rows as CONSUMED ADMISSION -- their declared trigger, "#9985 merging", fired in the base this change merges. Per the fourteenth dissolution's own recipe the trigger question was asked of both sides: the imported cohort goes, this change's cohort stays. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QakmRm5FF5ZspXYUNgbf9
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
…ee with it Review 58653 observed that authorization_scope_render printed the path without its tree, so two positions with identical segments in different trees rendered identically in a refusal. Reading the renderer against scope_covers found the same defect one field wider: the VERB was not rendered either, so a Read-vs-Write scope mismatch printed the same string on both sides of a refusal it had just issued -- a diagnostic that cannot distinguish the two sides of its own verdict. namespace_position_render was also a nickname for std.effect_grant effect_target_label. It is deleted; the tree and verb spellings now come from that module, which owns NamespaceTree and Verb, via namespace_tree_label and namespace_position_label declared there rather than re-coined here. srv3_scope_render_separates_verb_and_tree discriminates on each axis independently -- verb alone, tree kind alone, ServiceOpTree service alone -- with an equal-renders positive control so a renderer returning a constant fails it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QakmRm5FF5ZspXYUNgbf9
…fore mutating Review 58686 named two defects and both were real. THE RESET WAS AUTHORIZED BY OMISSION. srv3_boot_once_cd_resolved performs two Redfish writes -- PATCH the boot source override, then POST ComputerSystem.Reset -- while the grant named only the first. The reset sits under Actions, which the prefix relation cannot reach from the Boot root, so the second capability was covered by nothing. AuthorizationRequest and OperatorGrant now carry a SET of scopes; coverage is universal over the required side and existential over the granted side. An empty required set REFUSES (AuthorizationScopesUnstated) rather than passing vacuously, which is the shape every universal quantifier has on degenerate input. THE CLAIM HAD NO PRODUCTION CONSUMER. claim_authorization existed and only witnesses called it, so single-use was specification-without-execution: the live path evaluated the grant and executed. It could not have been wired as written -- the claim was typed over AuthorizationClaimState while the durable store reads and writes NonEmptyStr, so the two could never meet. The state is now serialized into the slot, the attempt's digest derives from those same bytes, and srv3_boot_once_cd_gated wins the compare-and-set BEFORE resolving credentials and long before the first write, then settles the slot to CompletedBy or AbortedBy. Losing refuses naming the holder's payload; an unreadable store refuses. A terminal write that does not land does not silently pass: the exit says the claim was left unterminated. authorization_is_permitted is dissolved. Its one consumer matches the decision directly, so the coproduct is no longer collapsed to a boolean in passing. Witnesses: a boot-only grant refuses and names the missing reset capability, with a both-scopes positive control so the refusal is about the gap rather than the check; and a request stating no scopes refuses. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QakmRm5FF5ZspXYUNgbf9
|
Review 58686: both findings verified and fixed in 8425d5e. The third is addressed by deletion. The reset was authorized by omission. Confirmed: The claim had no production consumer. Confirmed, and worse than a missing call: it could not have been wired as written.
Evidence: — sent from cool-fox-125 |
Auto-opened by session-dashboard for session
cool-fox-125.Pushing to
session/cool-fox-125advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan