Skip to content
Merged
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
16 changes: 16 additions & 0 deletions dag/extdeps/systemd/systemd_run.dag
Original file line number Diff line number Diff line change
Expand Up @@ -144,6 +144,22 @@ fn systemd_run_user_scope_command(properties: List<SystemdRunProperty>, command:
)
}

// ONE COMMAND IN A TRANSIENT SCOPE OF THE SYSTEM MANAGER, RUN AS A NAMED ACCOUNT
// (`systemd-run --scope --uid=U --gid=G -p NAME=VALUE ... -- CMD`). The user-manager form above needs
// the account's own session bus, which a command elevated with `sudo -u` from another login does not
// have. The system manager starts the scope, and systemd-run drops to the named uid and gid before it
// execs the command (systemd-run(1) --uid/--gid; src/run/run.c start_transient_scope applies
// arg_exec_user/arg_exec_group to the scope's child). So the command runs as that account inside a
// cgroup the kernel bounds. The caller must be root, since only the system manager can start a scope
// for another uid, and elevation is the caller's business, not this rendering's. The words come in
// the same order as the user form, so the property rendering stays in one place.
fn systemd_run_scope_as_account_argv(account: NonEmptyStr, properties: List<SystemdRunProperty>, command_argv: List<String>) -> List<String> {
let head = ["systemd-run", "--scope", concat("--uid=", account as String), concat("--gid=", account as String)]
let with_properties = fold(systemd_run_property_argv(properties: properties), init: head, f: (acc, word) => list_push(acc, word))
let with_separator = list_push(with_properties, "--")
fold(command_argv, init: with_separator, f: (acc, arg) => list_push(acc, arg))
}

fn systemd_run_property(name: String, value: String) -> String {
join([name, "=", value], "")
}
Expand Down
28 changes: 25 additions & 3 deletions dag/gunbc/auth/approval_device_enrolment_code_issue.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,11 @@ import std.algebra { trim }
import std.process { ProcessExit, ExitSuccess, ExitFailure, exit_failure }
import std.resources { Network }
import gunbc.cli_wire { CliWireResponse, CliWirePrintable, CliWireUnprintable }
import extdeps.sudo.elevation { sudo_elevate_as }
import extdeps.sudo.elevation { sudo_elevate }
import extdeps.systemd.systemd_run { SystemdRunProperty, systemd_run_scope_as_account_argv }
import extdeps.systemd { MemoryMax, MemoryHigh }
import std.measure { byte_size_count }
import gunbc.live_deploy.slice_bounds { approval_broker_slice_memory_max, approval_broker_slice_memory_high }
import extdeps.tools.env { env_prefixed_argv }
import v2.std.orchestration { EnvSet }
import gunbc.cli_run_workspace_root_scaffold { gunbc_workspace_root_env_name }
Expand Down Expand Up @@ -69,10 +73,28 @@ fn enrolment_code_issue_ssh_target() -> SshTarget {
// elevation through env(1), because sudo's env_reset would drop a variable set outside it.
// The elevated principal is the operator's POSIX user as modeled; /home/ubuntu in that refusal was
// the SSH login's working directory, which sudo keeps, not the account the verb ran as.
//
// AND IT RUNS IN A MEMORY-BOUNDED SCOPE, because the seed refuses to resolve without one. Its
// typed-module cache cap is derived from the cgroup's memory.high/memory.max, and with neither bound
// it refuses HostBudgetUnreadable rather than guessing (fleet-converge run 36556990543). An SSH
// session binds no such limit. The scope is a system-manager transient scope that runs the verb as
// the operator's account (extdeps.systemd.systemd_run systemd_run_scope_as_account_argv). A user
// scope would need that account's session bus, which the elevated command lacks. The bounds are the
// broker's own slice rows (gunbc.live_deploy.slice_bounds approval_broker_slice_memory_max and _high).
// The verb resolves the broker's routes closure, the same program the broker boots, so the same
// measured demand bounds it. It gets its OWN scope rather than joining the broker's slice, because
// joining would split one budget between the running broker and this run and put the broker at risk.
fn enrolment_code_issue_scope_properties() -> List<SystemdRunProperty> {
[
SystemdRunProperty { property: MemoryMax, value: to_string(byte_size_count(b: approval_broker_slice_memory_max)) as NonEmptyStr },
SystemdRunProperty { property: MemoryHigh, value: to_string(byte_size_count(b: approval_broker_slice_memory_high)) as NonEmptyStr },
]
}

fn enrolment_code_issue_remote_argv(revision: ReleaseRevisionBinding) -> List<String> {
let root = srv1_gunbc_approval_broker_root as String
let release_dir = approval_broker_release_dir(root: root, revision: revision)
let inv = sudo_elevate_as(user: fleet_posix_operator_user.name, command: env_prefixed_argv(bindings: [
let inv = sudo_elevate(command: systemd_run_scope_as_account_argv(account: fleet_posix_operator_user.name, properties: enrolment_code_issue_scope_properties(), command_argv: env_prefixed_argv(bindings: [
EnvSet { name: gunbc_workspace_root_env_name, value: release_dir },
], command_argv: [
approval_broker_release_binary_path(root: root, revision: revision),
Expand All @@ -82,7 +104,7 @@ fn enrolment_code_issue_remote_argv(revision: ReleaseRevisionBinding) -> List<St
"--entry", release_dir + "/dag/gunbc/auth/approval_device_routes.dag",
"--function", "issue_device_enrolment_code",
"--arg", "revision=" + release_revision_execstart_text(binding: revision),
]))
])))
concat([inv.bin_path], inv.args)
}

Expand Down
26 changes: 25 additions & 1 deletion dag/gunbc/auth/approval_device_redemption.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,11 @@
module gunbc.auth.approval_device_redemption

import std.decl_ref { decl_ref }
import std.types { NonEmptyStr, String, Timestamp, Int, List }
import gunbc.managed_directory { ManagedDirectory, DirectoryDependent, EntriesUnmanaged }
import gunbc.ownership { Ensured }
import std.effect_grant { Read, Write, Execute }
import gunbc.fleet_posix_accounts { fleet_posix_operator_user }
import std.types { NonEmptyStr, String, Timestamp, Int, List, FilePath }
import std.logic { Bool }
import std.dissolution { DissolutionCondition, unbound_dissolution }
import extdeps.crypto.signature { VerifyingKey, SignatureVerification, SignatureVerified }
Expand Down Expand Up @@ -505,6 +509,26 @@ fn redeem_device_over_store(
// an EnrolmentAdmitted value, under a root no other principal can write.
data approval_device_store_root: NonEmptyStr = "/var/lib/gunbc/approval-devices"

// THE STORE DIRECTORY IS CONVERGED BY THE BROKER INSTALL, and until this row nothing in the model
// created it. The first issued enrolment code (srv1, 2026-09-29) needed proud-deer-538 to create it by
// hand as briansrls:briansrls 0700. That hand step is closed by this row: the broker's dark install
// ensures it (gunbc.live_deploy.emit approval_broker_dark_install_release_steps). The owner is the
// operator's account, because the verbs that read and write it (approval_device_routes, the
// enrolment code issue) run as that account and nothing else needs it, so the derived mode is
// owner-only. Ownership is Ensured, not Owned: the directory holds enrolled devices, which must
// survive a retract of the deployment that created it.
fn approval_device_store_directory() -> ManagedDirectory {
ManagedDirectory {
member: "approval-device-store" as NonEmptyStr,
path: approval_device_store_root as String as FilePath,
owner: fleet_posix_operator_user,
group_principal: fleet_posix_operator_user,
dependents: [DirectoryDependent { who: fleet_posix_operator_user, needs: [Read, Write, Execute] }],
ownership: Ensured,
entries: EntriesUnmanaged,
}
}

type DeviceStoreWrite
= DeviceStoreWritten
| DeviceStoreSlotOccupied
Expand Down
37 changes: 34 additions & 3 deletions dag/gunbc/auth/approval_ntfy_deployment.dag
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,28 @@ data approval_ntfy_config_file_name: NonEmptyStr = "server.yml"
data approval_ntfy_config_path: NonEmptyStr = join([approval_ntfy_config_dir as String, "/", approval_ntfy_config_file_name as String], "") as NonEmptyStr
// The server's auth database, under its state root. Declared so the config's auth-file is checked
// against it and so the one elevated stat of it is an exact sudoers argv rather than a pattern.
data approval_ntfy_auth_file_path: NonEmptyStr = join([approval_ntfy_state_root as String, "/user.db"], "") as NonEmptyStr
//
// IT STAYS A DECLARATION, NOT A VALUE READ FROM THE CONFIG, because both of its consumers need a path
// fixed before the read. The stat runs through `sudo -n` at an exact argv that an operator-installed
// sudoers line must name, and a path taken from the config at runtime could only be covered by a
// pattern grant. The readback then refuses unless the running config names exactly this path, so the
// config is checked rather than trusted.
//
// THE FILE NAME WAS A GUESS, AND srv1 FALSIFIED IT. It read `user.db`. The server srv1 runs was
// installed with `auth-file: /var/lib/gunbc-ntfy/auth.db` in /etc/gunbc-ntfy/server.yml, and that file
// exists while user.db does not. proud-deer-538 read this on 2026-09-29 running
// issue_device_enrolment_code by hand against release 02568b3046, and the readback refused before
// minting. The name is now the observed one, and it changes the exact stat argv that this module's
// human step asks the operator to grant.
//
// THAT GRANT DOES NOT EXIST ON srv1 TODAY, and the stat still runs. proud-deer-538 read srv1 on
// 2026-09-29: sudoers.d holds only the broker-helpers grant, and the stat of auth.db succeeds under
// the operator account's own broader sudo. The narrow, exact-argv grant this module asks for is
// therefore an unmet posture, not a failing read. The earlier refusal was the missing user.db, not a
// missing grant. Nothing installs this server or that grant from the model yet
// (gunbc.auth.approval_ntfy_converge names the server as outside its roster). This row becomes that
// installer's destination when one exists, and the grant becomes its sudoers member.
data approval_ntfy_auth_file_path: NonEmptyStr = join([approval_ntfy_state_root as String, "/auth.db"], "") as NonEmptyStr
data approval_ntfy_unit_name: NonEmptyStr = "gunbc-ntfy.service"

// THE TWO ntfy USERS THE ACCESS LIST MAY NAME, declared so the ACL readback
Expand All @@ -60,8 +81,18 @@ data approval_ntfy_unit_name: NonEmptyStr = "gunbc-ntfy.service"
// only WRITE the topic; the operator is the phone's sign-in and may only READ it. A server whose
// users carry other names reads back as a deviation and enrolment-code issuance refuses -- loudly,
// never by guessing which user is which.
data approval_ntfy_publisher_user: NonEmptyStr = "gunbc-approval-publisher"
data approval_ntfy_operator_user: NonEmptyStr = "gunbc-approval-operator"
//
// THE NAMES ARE THE ONES srv1's SERVER CARRIES, AND THE PREVIOUS ONES WERE NEVER CREATED. They read
// gunbc-approval-publisher and gunbc-approval-operator, names chosen here that no step on the host
// used. The live `ntfy access` that proud-deer-538 read on srv1 on 2026-09-29, running
// issue_device_enrolment_code by hand, lists publisher `gunbc-broker` (write-only on the topic) and
// operator `briansrls` (read-only), with anonymous access denied. Those accounts already carry the
// broker's publisher token and the operator's phone subscription, so the declaration follows them
// rather than asking for both credentials to be minted again. These stay declarations: the readback
// compares the live list against them and refuses any other shape. Nothing creates these users from
// the model yet. The ntfy installation vertical owns that, and these rows become its contract.
data approval_ntfy_publisher_user: NonEmptyStr = "gunbc-broker"
data approval_ntfy_operator_user: NonEmptyStr = "briansrls"
// THE SERVER BINARY THE HOST ACTUALLY RUNS. Absolute because it runs under sudo as the server's
// principal; an absent binary is a failed readback, which refuses. The readback compares the running
// process's executable against THIS row, and that comparison is only a check because the row is not
Expand Down
9 changes: 7 additions & 2 deletions dag/gunbc/live_deploy/emit.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
module gunbc.live_deploy.emit

import gunbc.auth.approval_device_redemption { approval_device_store_directory }
import gunbc.live_deploy.release_locus {
ReleaseRevisionBinding,
RevisionBoundAtEmission,
Expand Down Expand Up @@ -27,6 +28,7 @@ import std.evaluation_budget { EvaluationLimit, LimitSet, LimitUnset }
import std.types { String, List, Bool, NonEmptyStr, Int, FilePath, CommitSha, Port }
import gunbc.managed_directory {
ManagedDirectory,
managed_directory_admit,
ManagedDirectoryAdmission, ManagedDirectoryAdmitted, ManagedDirectoryRefused,
managed_directory_mode_octal,
attempt_state_directory_at,
Expand Down Expand Up @@ -3133,8 +3135,11 @@ fn live_deploy_wholesale_refused_poison(refusals: List<MemberRefusal<DeploymentS
// rather than rendering the whole orchestrated script (DESIGN section 3).
fn approval_broker_dark_install_release_steps(spec: DeploymentSpec, revision: ReleaseRevisionBinding) -> List<PipelineStep> {
concat(
approval_broker_tree_copy_steps(spec: spec, revision: revision),
approval_broker_helper_grant_steps(spec: spec, revision: revision),
[deploy_raw(command: ensure_managed_directory_command(admission: managed_directory_admit(d: approval_device_store_directory())))],
concat(
approval_broker_tree_copy_steps(spec: spec, revision: revision),
approval_broker_helper_grant_steps(spec: spec, revision: revision),
),
)
}

Expand Down
13 changes: 11 additions & 2 deletions dag/test/claim/approval_device_enrolment_code_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ import gunbc.live_deploy.release_locus {
import gunbc.fleet_intent_network { operator_host_srv1 }
import gunbc.fleet_posix_accounts { fleet_posix_operator_user }
import gunbc.cli_run_workspace_root_scaffold { gunbc_workspace_root_env_name }
import std.measure { byte_size_count }
import gunbc.live_deploy.slice_bounds { approval_broker_slice_memory_max, approval_broker_slice_memory_high }
import gunbc.fleet_converge_workflow {
ApprovalDeviceEnrolmentCodeIssue, fleet_converge_workflow_mode_wire, fleet_converge_workflow_modes, fleet_converge_mode_fleet_ssh_key_demand, FleetSshKeyConsumed,
}
Expand Down Expand Up @@ -65,11 +67,18 @@ test fn the_delivered_receipt_comes_from_the_published_message_and_its_line_neve
// POSIX user under non-interactive sudo, and names the verb by its module and function. It also
// hands the seed the release directory as its checkout root, inside the elevation and ahead of the
// binary. Without that binding the seed walks up from the SSH login's home and refuses before minting
// (fleet-converge run 36415852659), so removing it turns this claim red.
// (fleet-converge run 36415852659), so removing it turns this claim red. The whole verb runs in a
// system scope as the operator's account, bounded by the broker's slice rows. Without a memory bound
// the seed refuses HostBudgetUnreadable (run 36556990543), so dropping the scope or its bounds also
// turns this claim red.
test fn the_remote_argv_runs_the_release_verb_as_the_operator_user() -> Bool {
let argv = enrolment_code_issue_remote_argv(revision: RevisionBoundAtEmission { revision: "0123456789abcdef0123456789abcdef01234567" })
let joined = join(argv, " ")
string_contains(s: joined, pattern: "/usr/bin/sudo -n -u " + (fleet_posix_operator_user.name as String) + " /usr/bin/env " + gunbc_workspace_root_env_name + "=/opt/gunbc/approval-broker/releases/0123456789abcdef0123456789abcdef01234567 /opt/gunbc/approval-broker/releases/0123456789abcdef0123456789abcdef01234567/gunbc run ")
let op = fleet_posix_operator_user.name as String
string_contains(s: joined, pattern: "/usr/bin/sudo -n systemd-run --scope --uid=" + op + " --gid=" + op
+ " --property=MemoryMax=" + to_string(byte_size_count(b: approval_broker_slice_memory_max))
+ " --property=MemoryHigh=" + to_string(byte_size_count(b: approval_broker_slice_memory_high))
+ " -- /usr/bin/env " + gunbc_workspace_root_env_name + "=/opt/gunbc/approval-broker/releases/0123456789abcdef0123456789abcdef01234567 /opt/gunbc/approval-broker/releases/0123456789abcdef0123456789abcdef01234567/gunbc run ")
&& string_contains(s: joined, pattern: "/releases/0123456789abcdef0123456789abcdef01234567/gunbc run ")
&& string_contains(s: joined, pattern: "--entry /opt/gunbc/approval-broker/releases/0123456789abcdef0123456789abcdef01234567/dag/gunbc/auth/approval_device_routes.dag --function issue_device_enrolment_code --arg revision=0123456789abcdef0123456789abcdef01234567")
}
Expand Down
17 changes: 12 additions & 5 deletions dag/test/claim/approval_ntfy_access_readback_wet_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,7 @@ import gunbc.auth.approval_ntfy_runtime_observe {
// passes is never installed, so the one read that can bind the process -- the per-release helper at
// /opt/gunbc/approval-broker-helpers/<revision> -- cannot run on any host, and the verdict over
// every reading is refusal: a failed or inactive unit, any runtime gap, or that failed helper read.
// So the claim holds on ANY host: the verb refuses before any code is minted and the store root is
// never created. Forcing the verdict (the verb proceeding without its
// So the claim holds on ANY host: the verb refuses before any code is minted and creates no store root. Forcing the verdict (the verb proceeding without its
// reading) reds it: it then goes on to the clock, the entropy and the store. Every refusal arm is
// witnessed hermetically over supplied readings in
// test.claim.approval_ntfy_access_readback_witness_test; this is the one claim that runs the real
Expand All @@ -33,15 +32,23 @@ fn path_exists(path: String) -> Bool {
run_shell_command_observe(command: posix_sh_program_command(script: "test -e '" + path + "'\n"), transport: LocalExec).exit_code == 0
}

//
// THE STORE'S EXISTENCE IS COMPARED, NOT ASSUMED ABSENT. This claim once required that the store root
// not exist on the runner. That premise came from the host, not the subject, and srv1 falsified it on
// 2026-09-29: the root was created there by hand for the first issued code, and the broker install now
// ensures it (gunbc.auth.approval_device_redemption approval_device_store_directory). The claim went red
// on srv1-09 (#12614 floor run 36562259065) while the verb behaved correctly. The subject is that the
// verb refuses before minting and creates nothing. So it asserts the refusal, and that the call leaves
// the store's existence as it found it. That holds on a host with a store and on one without, and a
// verb that went on to the store still reds it on a host without one.
test fn the_root_refuses_before_minting_on_this_host_by_real_execution() -> Bool {
let before = path_exists(path: approval_device_store_root as String)
let r = issue_device_enrolment_code(revision: never_installed_revision)
!before
&& (match r {
(match r {
CliWireUnprintable { cause: c } => string_contains(s: c as String, pattern: "refused before any code was minted")
_ => false
})
&& !path_exists(path: approval_device_store_root as String)
&& path_exists(path: approval_device_store_root as String) == before
}

// THE HELPER'S REAL OUTPUT READS THROUGH THE REAL CODEC. The helper entry
Expand Down
Loading
Loading