Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions DESIGN.md

Large diffs are not rendered by default.

90 changes: 90 additions & 0 deletions dag/extdeps/git/publication_transport.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
module extdeps.git.publication_transport

import std.types { Bool, CommitSha, GitRef, Int, List, NonEmptyStr, String }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "git-scm.com/docs/git-push"
}
}

data git_commit_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "git-scm.com/docs/git-commit"
}
}

data git_publication_transport_note: String = "Modeled upstream publication write operations de-fused from git.Core. PushRefUpdate and RecordCommit are the interface shapes for writing to a remote and recording a local commit respectively; the shell argv on each operation is ONE transport handler, never the semantic model. Consumers that need publication safety must route through gunbc.publication_publisher and admit an admitted public projection before binding a transport handler — raw argv push remains observable for shadow replay only in slice 1."

type GitRefUpdateSpec {
local_ref: GitRef
remote_ref: GitRef
}

type GitPushRequest {
remote: NonEmptyStr
ref_updates: List<GitRefUpdateSpec>
}

type GitCommitRequest {
message: NonEmptyStr
allow_empty: Bool
}

fn shape_git_push_refspec(update: GitRefUpdateSpec) -> String {
join([update.local_ref as String, ":", update.remote_ref as String], "")
}

fn shape_git_push_argv(request: GitPushRequest) -> List<String> {
fold(request.ref_updates, init: ["git", "push", request.remote as String], f: fn(argv, update) {
append(argv, items: [shape_git_push_refspec(update: update)])
})
}

fn shape_git_commit_argv(request: GitCommitRequest) -> List<String> {
if request.allow_empty {
["git", "commit", "--allow-empty", "-m", request.message as String]
} else {
["git", "commit", "-m", request.message as String]
}
}

service git.PublicationTransport {
operation PushRefUpdate {
input {
remote: NonEmptyStr
refspec: NonEmptyStr
}
output {
exit_code: Int from "exit_code"
stderr: String from "stderr"
success: Bool from "exit_success"
}
transport shell { argv: ["git", "push", "{remote}", "{refspec}"] }
exit {
0 => Unit
nonzero => String "Push failed"
}
}

operation RecordCommit {
input {
message: NonEmptyStr
allow_empty: Bool = false
}
output {
sha: CommitSha from "stdout"
success: Bool from "exit_success"
stderr: String from "stderr"
}
transport shell { argv: ["git", "commit", "-m", "{message}"] }
exit {
0 => Unit
nonzero => String "Commit failed"
}
}
}
25 changes: 8 additions & 17 deletions dag/gunbc/ci_deploy_access.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module gunbc.ci_deploy_access

import std.types { NonEmptyStr, List, String, Bool }
import std.access { AccessDecision, Permit, Deny }
import std.access { AccessDecision, Permit, Deny, access_policy_refusal, access_refusal_reason }
import std.disposition { Disposition, Scaffold, RealizationDispatch, Terminal }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import std.materialization_ladder { Frame, SharedStateFrame }
Expand Down Expand Up @@ -295,38 +295,29 @@ fn deploy_access_sudo_miss_reason(access: DeployAccess) -> String {
fn deploy_access_check(access: DeployAccess, actor: DeployAccessActor) -> AccessDecision {
let expected = grounded_posix_principal_name(p: access.principal)
if actor.observed_name != expected {
Deny {
reason: Present {
value: concat(
access_policy_refusal(
profile: "deploy-access", subject: actor.observed_name, action: "execute", object: expected,
reason: concat(
concat(
concat(deploy_access_refusal_prefix, " — principal mismatch expected="),
expected
),
concat(" actual=", actor.observed_name)
)
}
}
),
)
} else {
if actor.sudo_granted {
Permit
} else {
Deny {
reason: Present {
value: deploy_access_sudo_miss_reason(access: access)
}
}
access_policy_refusal(profile: "deploy-access", subject: actor.observed_name, action: "execute", object: expected, reason: deploy_access_sudo_miss_reason(access: access))
}
}
}

fn deploy_access_decision_reason(d: AccessDecision) -> String {
match d {
Permit => ""
Deny { reason: r } =>
match r {
Present { value: why } => why
Absent => deploy_access_refusal_prefix
}
Deny { refusal: refusal } => access_refusal_reason(refusal: refusal)
}
}

Expand Down
32 changes: 13 additions & 19 deletions dag/gunbc/ci_deploy_target_host.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module gunbc.ci_deploy_target_host

import std.types { String, NonEmptyStr, Bool, List }
import std.access { AccessDecision, Permit, Deny }
import std.access { AccessDecision, Permit, Deny, access_policy_refusal, access_refusal_reason }
import std.disposition { Disposition, Scaffold, SingleAuthority }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import extdeps.shell
Expand Down Expand Up @@ -57,11 +57,7 @@ fn deploy_target_host_observed() -> DeployTargetHostObservation {
fn deploy_target_host_decision_reason(d: AccessDecision) -> String {
match d {
Permit => ""
Deny { reason: r } =>
match r {
Present { value: why } => why
Absent => deploy_target_host_refusal_prefix
}
Deny { refusal: refusal } => access_refusal_reason(refusal: refusal)
}
}

Expand All @@ -70,7 +66,7 @@ fn deploy_target_host_check(
observed: DeployTargetHostObservation
) -> AccessDecision {
if !deploy_target_ssh_proof_structurally_valid(proof: proof) {
Deny { reason: Present { value: deploy_target_host_refusal_ssh } }
access_policy_refusal(profile: "deploy-target-host", subject: "runner", action: "deploy", object: "target-host", reason: deploy_target_host_refusal_ssh)
} else {
if deploy_target_host_apply_permitted(
proof: proof,
Expand All @@ -81,9 +77,9 @@ fn deploy_target_host_check(
} else {
match proof {
RunnerIdentityOnHost { host: id } =>
Deny {
reason: Present {
value: concat(
access_policy_refusal(
profile: "deploy-target-host", subject: observed.runner_name, action: "deploy", object: id,
reason: concat(
concat(
concat(deploy_target_host_refusal_prefix, " — "),
deploy_target_host_refusal_local
Expand All @@ -95,21 +91,19 @@ fn deploy_target_host_check(
concat(" runner=", observed.runner_name)
)
)
)
}
}
),
)
SshExplicitHost { host: id, ssh_host: h } =>
Deny {
reason: Present {
value: concat(
access_policy_refusal(
profile: "deploy-target-host", subject: observed.runner_name, action: "deploy", object: id,
reason: concat(
concat(deploy_target_host_refusal_prefix, " — "),
concat(
deploy_target_host_refusal_ssh,
concat(" expected=", concat(id, concat(" ssh_host=", h)))
)
)
}
}
),
)
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/design_document.dag

Large diffs are not rendered by default.

7 changes: 7 additions & 0 deletions dag/gunbc/doc_graph_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -357,6 +357,13 @@ data hand_authored_doc_binds: List<HandAuthoredDocBind> = [
additional_works: [],
dissolution: HasTrigger { text: "Nat lives only in std.nat (coproduct + Peano ops), v2.std.nat imports rather than redefines it, the 138-entry co-occurrence class is gone, and integer's GroupCompletion<Nat> cites the unified type — then this per-concept census doc deletes with this row (full criteria in the doc §9)" },
},
HandAuthoredDocBind {
home: PlanDoc,
slug: "sole-modeled-publisher-design",
primary_work: DeclarationRef { module_path: "tools.publication_publisher", decl_name: "PublicationAuthority", field: WholeDeclaration },
additional_works: [DeclarationRef { module_path: "tools.publication_push_shadow", decl_name: "shadow_replay_public_pushes", field: WholeDeclaration }],
dissolution: HasTrigger { text: "Stage 2 binds git.PublicationTransport dispatch to PublicationAuthority (live refuse, not shadow-only), shadow_replay_public_pushes becomes a permanent regression control, and the staged migration either registers as a gunbc.plan.Plan row or deletes when enforcement lands on carriers" },
},
]

fn hand_authored_doc_graph_roots() -> List<String> {
Expand Down
17 changes: 8 additions & 9 deletions dag/gunbc/host_effect_realize.dag
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ import gunbc.srv3_actuate_shell_paths {
srv3_bmcweb_login_response_path,
srv3_bmcweb_token_path,
}
import std.access { AccessDecision, Permit, Deny }
import std.access { AccessDecision, Permit, Deny, access_policy_refusal }
import gunbc.ci_deploy_access {
DeployAccess,
DeployAccessActor,
Expand Down Expand Up @@ -1797,14 +1797,13 @@ fn deploy_access_check_observed(access: DeployAccess) -> AccessDecision {
match deploy_access_observed_actor(access: access) {
Present { value: actor } => deploy_access_check(access: access, actor: actor)
Absent =>
Deny {
reason: Present {
value: concat(
access_policy_refusal(
profile: "deploy-access-observation", subject: "unobserved", action: "execute", object: "host-effect",
reason: concat(
deploy_access_refusal_prefix,
" — could not observe principal (ReadEffectivePosixPrincipal failed)"
)
}
}
),
)
}
}

Expand Down Expand Up @@ -1869,7 +1868,7 @@ fn host_effect_apply_gated(
NotConverged { reason: "host_effect_apply: RedfishAction realization is a fail-closed Unimplemented stub in Phase A; neat-boar-71 realizes it over RedfishRest in Phase C. No plausible no-op for a power/boot action (DESIGN section 5).", applied: intent }
IncompatibleCell { reason: why } => NotConverged { reason: why, applied: intent }
}
Deny { reason: _ } =>
Deny { refusal: _ } =>
NotConverged {
reason: deploy_access_decision_reason(d: verdict),
applied: HostEffectIntent {
Expand Down Expand Up @@ -1897,7 +1896,7 @@ fn host_effect_drive_directive(r: Reconciliation<HostEffectIntent, HostEffectEvi
Converged { evidence: _, applied: _ } => Settled
NotConverged { reason: why, applied: intent } =>
match intent.privilege_denial {
Present { value: Deny { reason: _ } } => Refused { reason: why }
Present { value: Deny { refusal: _ } } => Refused { reason: why }
Present { value: Permit } => not_converged_directive(drive: host_effect_drive(intent: intent))
Absent =>
match resolve_host_effect_cell(target: intent.target, effect: intent.effect) {
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/host_identity_converge.dag
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ fn host_identity_unprivileged_refusal_has_no_marker(
NotConverged { reason: why, applied: intent } =>
!string_contains(s: why, pattern: marker)
&& match intent.privilege_denial {
Present { value: Deny { reason: _ } } => true
Present { value: Deny { refusal: _ } } => true
_ => false
}
Converged { evidence: _, applied: _ } => false
Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/live_deploy/apply.dag
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@ fn live_deploy_fold(
fixture_host: fixture_host
)
match gate {
Deny { reason: _ } =>
Deny { refusal: _ } =>
live_deploy_mutation_denied(
target: target,
effect: effect,
Expand Down Expand Up @@ -383,7 +383,7 @@ fn live_deploy_access_preflight_for(access: DeployAccess) -> Reconciliation<Host
},
applied: intent,
}
Deny { reason: _ } =>
Deny { refusal: _ } =>
NotConverged {
reason: deploy_access_decision_reason(d: gate),
applied: HostEffectIntent {
Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/live_deploy/readiness.dag
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ fn show_healthz_read_for_deploy(
) -> ShowEffectiveRead<HealthzEffectiveRead> {
let verdict = host_effect_privilege_verdict(access: access, fixture_actor: Absent)
match verdict {
Deny { reason: _ } =>
Deny { refusal: _ } =>
ReadObserved {
value: HealthzEffectiveRead {
body: "",
Expand Down Expand Up @@ -269,7 +269,7 @@ fn capture_unit_diagnosis(
) -> String {
let verdict = host_effect_privilege_verdict(access: access, fixture_actor: Absent)
match verdict {
Deny { reason: _ } =>
Deny { refusal: _ } =>
concat("unit diagnosis capture failed: ", deploy_access_decision_reason(d: verdict))
Permit =>
unit_status_capture_text(
Expand Down
52 changes: 52 additions & 0 deletions dag/gunbc/principal_projection.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
module gunbc.principal_projection

import std.types { NonEmptyStr }
import extdeps.auth.jwt { JwtStringOrUri }
import extdeps.auth.oidc { OidcIdTokenClaims }
import extdeps.access.posix_effective_principal { EffectivePosixPrincipalRead }

data principal_projection_note: String = "A gunbc principal is a projection of external authentication evidence, never an independently authored identity. OidcProjectedPrincipal reads issuer and subject directly from extdeps.auth.oidc.OidcIdTokenClaims (whose vocabulary is extdeps.auth.jwt.JwtStringOrUri). PosixProjectedPrincipal reads the non-empty observed result of extdeps.access.posix_effective_principal.EffectivePosixPrincipalRead. PrincipalProjection couples each evidence kind to its only matching constructor, and projected_principal derives rather than stores the principal, so contradictory principal/evidence pairs are unrepresentable. Future policy vocabulary must project the named external authorities rather than mint local substitutes: extdeps.access.aws_iam.PolicyDocument, extdeps.access.rbac.RbacPolicy, and extdeps.access.zanzibar.CheckRequest."

type OidcProjectedPrincipal {
issuer: JwtStringOrUri
subject: JwtStringOrUri
}

type PosixProjectedPrincipal {
effective_name: NonEmptyStr
}

type GunbcPrincipal
= OidcPrincipal { principal: OidcProjectedPrincipal }
| PosixPrincipal { principal: PosixProjectedPrincipal }

type PosixEffectivePrincipalEvidence {
read: EffectivePosixPrincipalRead
observed_name: NonEmptyStr
}

type PrincipalProjection
= OidcProjection { claims: OidcIdTokenClaims }
| PosixProjection { observation: PosixEffectivePrincipalEvidence }

fn oidc_principal_projection(claims: OidcIdTokenClaims) -> PrincipalProjection {
OidcProjection { claims: claims }
}

fn posix_principal_projection(
observation: PosixEffectivePrincipalEvidence,
) -> PrincipalProjection {
PosixProjection { observation: observation }
}

fn projected_principal(projection: PrincipalProjection) -> GunbcPrincipal {
match projection {
OidcProjection { claims: claims } => OidcPrincipal { principal: OidcProjectedPrincipal {
issuer: claims.issuer,
subject: claims.subject,
} }
PosixProjection { observation: observation } => PosixPrincipal { principal: PosixProjectedPrincipal {
effective_name: observation.observed_name,
} }
}
}
Loading
Loading