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
84 changes: 84 additions & 0 deletions artifacts/bmc/mtcollins1-diskless-boot.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
{
"attach": {
"configurations_after": {
"redirection_status": 100,
"session_index": 0
},
"endpoint": "POST /api/settings/media/remote/start-media",
"image_index_resolved_by": "reading /api/settings/media/remote/images, not assumed"
},
"boot_drive": {
"performed_by": "gunbc.machine_intake_mtcollins1_actuate mtcollins1_cdrom_handoff",
"precondition": "boot parameter 5 reset to 'No override' before the run"
},
"capture_subject": "mtcollins1-diskless-boot",
"claim": "the host booted an aarch64 Linux kernel and reached systemd with a squashfs+overlayfs root, from an image delivered entirely out of band, on a machine with no boot drive",
"delivery_chain": [
"srv2 NFS export /srv/bmc (ro, scoped to 192.168.1.228)",
"MegaRAC remote-media client on the controller fetches the image itself",
"virtual CD presented to the host",
"host UEFI -> GRUB 2.12 -> EFI stub"
],
"diskless_evidence": {
"kernel_cmdline": "BOOT_IMAGE=/casper/vmlinuz",
"memory_available_kib": 261972592,
"note": "diskless, not RAM-resident: casper mounts squashfs read-only under a tmpfs overlay, so the WRITABLE layer is memory-backed and no local disk is involved. Casper toram is absent from the observed command line, so the read-only lower layer is presumed to be read from the presented media on demand. A RAM-resident root does not follow from what was observed.",
"root": "squashfs 4.0 mounted read-only with an overlayfs upper"
},
"firmware_behaviours_that_a_modeled_caller_must_expect": {
"put_media_general": {
"body_code": 16425,
"consequence": "an operation treating nonzero as refusal will refuse a write that worked",
"http": 500,
"observed": "the write reported failure AND the share re-mounted; images re-enumerated 23s later"
},
"share_listing_is_available_pool_not_share_contents": "after start-media attaches an image, that name leaves /remote/images for /remote/configurations and survivors reindex. An empty or shorter images listing is not a stale cache. Re-asserting mount_cd appeared to refresh the listing because the toggle detaches everything and returns names to the available pool; that is not a remedy.",
"stop_media": {
"body_code": 1411,
"http": 500,
"observed": "reported failure; the subsequent start-media succeeded"
}
},
"host_side_acceptance_marker": {
"source": "serial-over-LAN console, not redirection_status",
"trace": [
"[2;30HGNU GRUB version 2.12",
"[5;3H*Try or Install Ubuntu Server ",
"[0;37;40mEFI stub: Booting Linux Kernel...",
"EFI stub: WARNING: Working around broken SetVirtualAddressMap()",
"EFI stub: Loaded initrd from LINUX_EFI_INITRD_MEDIA_GUID device path",
"EFI stub: Generating empty DTB",
"EFI stub: Exiting boot services...",
"[ 0.000000] Booting Linux on physical CPU 0x0000120000 [0x413fd0c1]",
"[ 0.000000] Linux version 6.8.0-71-generic (buildd@bos03-arm64-036) (aarch64-linux-gnu-gcc-13 (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0, GNU ld (GNU Binutils for Ubuntu) 2.42) #71-Ubuntu SMP PREEMPT_DYNAMIC Tue Jul 22 16:44:45 UTC 2025 (Ubuntu 6.8.0-71.71-generic 6.8.12)",
"[ 0.000000] Kernel command line: BOOT_IMAGE=/casper/vmlinuz --- console=tty0",
"[ 14.925304] squashfs: version 4.0 (2009/01/31) Phillip Lougher",
"[ 25.748415] overlayfs: \"xino\" feature enabled using 3 upper inode bits.",
"[ 26.406227] systemd[1]: systemd 255.4-1ubuntu8.10 running in system mode (+PAM +AUDIT +SELINUX +APPARMOR +IMA +SMACK +SECCOMP +GCRYPT -GNUTLS +OPENSSL +ACL +BLKID +CURL +ELFUTILS +FIDO2 +IDN2 -IDN +IPTC +KMOD +LIBCRYPTSETUP +LIBFDISK +PCRE2 -PWQUALITY +P11KIT +QRENCODE +TPM2 +BZIP2 +LZ4 +XZ +ZLIB +ZSTD -BPF_FRAMEWORK -XKBCOMMON +UTMP +SYSVINIT default-hierarchy=unified)",
"[ 26.442927] systemd[1]: Detected architecture arm64."
],
"why_this_is_the_marker": "a nonzero redirection_status proves a media session; only the booted program's own output proves the artifact executed on the host"
},
"image": {
"file": "ubuntu-24.04.3-live-server-arm64.iso",
"measured_sha256": "2ee2163c9b901ff5926400e80759088ff3b879982a3956c02100495b489fd555",
"pin_agrees_with": "extdeps.provisioning.ubuntu_install_media noble_numbat_2404_3_live_server_arm64.content_sha256, and upstream cdimage SHA256SUMS"
},
"not_established": [
"this is a stock live-server image; nothing per-host is injected and no identity is bound",
"the backing share is srv2, a fleet peer, so this is not yet independent of the fleet",
"UEFI HTTP Boot remains unmeasured; every boot so far was forced to a device over IPMI"
],
"observed_at_utc": "2026-09-05T22:55Z",
"media_detach_during_boot_observation": {
"observed_at": "2026-09-06",
"what_was_done": "mount_cd toggled 0 then 1 on the controller while the unit was booted from the presented ISO, to force the images listing to re-enumerate",
"why_it_was_done": "a wrong diagnosis: the image had left the available listing because it was ATTACHED, not because the listing was stale",
"observed_outcome": "the running Ubuntu installer survived; measured afterwards over IPMI SOL, still interactive at its own menu, and chassis power reported on",
"controller_retry_config": {
"rmedia_retry_count": 3,
"rmedia_retry_interval": 15
},
"what_this_does_not_establish": "that a detach during heavy reads is survivable. The system was idle at a prompt rather than reading, and casper reads the read-only lower layer from the presented medium on demand (toram is absent from the observed command line). One observation of one idle host bounds nothing."
}
}
126 changes: 126 additions & 0 deletions dag/extdeps/bmc/megarac.dag
Original file line number Diff line number Diff line change
Expand Up @@ -156,3 +156,129 @@ fn megarac_image_redirection_wire(r: MegaRacImageRedirectionRequired) -> NonEmpt
MegaRacImageRedirectionOn => "1"
}
}

// THE OPERATIONS ABOVE ARE A DESCRIPTION; THESE ARE THE OPERATIONS. megarac_api_operations records
// paths and contract notes and carries no transport, so nothing in this repository could invoke the
// MegaRAC media surface — the first attach against a Mt. Collins unit was therefore driven by a
// hand-written shell script, which is exactly the unmodeled realization DESIGN §6 names. These rows
// make that surface reachable from a workflow.
//
// SESSION AUTH IS COOKIE-AND-HEADER, NOT netrc, which is why these cannot reuse the redfish.Http
// shape beside them. POST /api/session returns a CSRFToken in its body and sets a session cookie;
// every subsequent request must present BOTH the cookie jar and an X-CSRFTOKEN header.
//
// THE JAR PATH BEING A PARAMETER DOES NOT MAKE AN ATTEMPT OWN ITS JAR, and an earlier revision of
// this note claimed it did. A parameter permits a per-attempt path; it does not require one, and
// the first production caller passed a fixed literal — so two concurrent attempts shared one bearer
// file, which is the opposite of what the note asserted. Ownership is a property of the CALLER's
// allocation, and the caller is where it has to be established.
//
// A SESSION THAT IS NEVER CLOSED IS A LEAKED REMOTE RESOURCE. CloseSession exists because the
// controller's session table is finite and this lane exhausted a service's sessions by opening one
// per probe and closing none. Every operation sequence that opens a session owes a close on every
// exit, including refusals — an operation that failed still allocated the session that carried it.
//
// THE CREDENTIAL IS FORM-ENCODED IN THE SESSION CALL AND NOWHERE ELSE. It reaches argv there, which
// is a real weakness and is stated rather than hidden: curl offers no netrc equivalent for a
// form-encoded POST body, and the alternative spellings (--data @file) put the credential in a file
// whose lifetime this operation does not control. Every operation AFTER the session carries no
// credential at all — the cookie is the bearer — so the exposure is one call, not the whole flow.
// The next-rung repair is a transport that reads a form body from a file the caller materializes
// and removes, which is the same missing mechanism the removed ipmi UserSetPassword operation
// needs.
//
// StartMedia's json_body MUST CARRY image_redirection AND ITS ABSENCE IS OPAQUE. The contract note
// on the operation row above records that omitting it makes the firmware refuse with codes
// 13410/13460, recovered from the firmware's own UI bundle rather than from documentation. The body
// is a caller parameter rather than a baked literal because image_index is resolved by READING the
// images listing, never assumed, and megarac_image_redirection_wire is the authority for the field
// itself.
service megarac.Media {

operation OpenSession {
input { bmc_host: NonEmptyStr, username: NonEmptyStr, password: NonEmptyStr, cookie_jar: NonEmptyStr }
output { body: String from "stdout", success: Bool from "exit_success" }
transport shell {
argv: ["curl", "--fail-with-body", "-sS", "-k", "-c", "{cookie_jar}", "-X", "POST", "-d", "username={username}", "-d", "password={password}", "https://{bmc_host}/api/session"]

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge URL-encode session credential fields

When either credential contains form delimiters such as &, +, %, or =, passing username={username} and password={password} through -d changes the submitted form fields and causes authentication to fail despite valid credentials. Local curl --help all identifies --data-urlencode as the option for URL-encoded POST data; use it for both named fields instead of raw -d values.

Useful? React with 👍 / 👎.

}
exit {
0 => Unit
nonzero => String "megarac session POST failed"
}
}

operation GetMediaGeneral {
input { bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, csrf_token: NonEmptyStr }
output { body: String from "stdout", success: Bool from "exit_success" }
readonly
transport shell {
argv: ["curl", "--fail-with-body", "-sS", "-k", "-b", "{cookie_jar}", "-H", "X-CSRFTOKEN: {csrf_token}", "https://{bmc_host}/api/settings/media/general"]
Comment on lines +210 to +215

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Add the missing media-configuration write

When the BMC has no mounted share, or when the newly recorded image-cache failure requires mount_cd to be reasserted, this service cannot establish media because its only operation for /api/settings/media/general is a GET. A repo-wide search for that endpoint finds no other executable PUT transport, while the existing contract row says the PUT supplies the server address, source path, share type, and mount_cd; therefore a workflow still cannot reproduce the attach flow this service is intended to expose.

Useful? React with 👍 / 👎.

}
exit {
0 => Unit
nonzero => String "megarac media general GET failed"
}
}

operation GetRemoteImages {
input { bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, csrf_token: NonEmptyStr }
output { body: String from "stdout", success: Bool from "exit_success" }
readonly
transport shell {
argv: ["curl", "--fail-with-body", "-sS", "-k", "-b", "{cookie_jar}", "-H", "X-CSRFTOKEN: {csrf_token}", "https://{bmc_host}/api/settings/media/remote/images"]
}
exit {
0 => Unit
nonzero => String "megarac remote images GET failed"
}
}

operation GetRemoteConfigurations {
input { bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, csrf_token: NonEmptyStr }
output { body: String from "stdout", success: Bool from "exit_success" }
readonly
transport shell {
argv: ["curl", "--fail-with-body", "-sS", "-k", "-b", "{cookie_jar}", "-H", "X-CSRFTOKEN: {csrf_token}", "https://{bmc_host}/api/settings/media/remote/configurations"]
}
exit {
0 => Unit
nonzero => String "megarac remote configurations GET failed"
}
}

operation StartMedia {
input { bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, csrf_token: NonEmptyStr, json_body: NonEmptyStr }
output { body: String from "stdout", success: Bool from "exit_success" }
transport shell {
argv: ["curl", "--fail-with-body", "-sS", "-k", "-b", "{cookie_jar}", "-H", "X-CSRFTOKEN: {csrf_token}", "-H", "Content-Type: application/json", "-X", "POST", "-d", "{json_body}", "https://{bmc_host}/api/settings/media/remote/start-media"]
}
exit {
0 => Unit
nonzero => String "megarac start-media POST failed"
}
}

operation StopMedia {
input { bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, csrf_token: NonEmptyStr, json_body: NonEmptyStr }
output { body: String from "stdout", success: Bool from "exit_success" }
transport shell {
argv: ["curl", "--fail-with-body", "-sS", "-k", "-b", "{cookie_jar}", "-H", "X-CSRFTOKEN: {csrf_token}", "-H", "Content-Type: application/json", "-X", "POST", "-d", "{json_body}", "https://{bmc_host}/api/settings/media/remote/stop-media"]

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Treat the observed HTTP 500 stop as indeterminate

On the Mt. Collins firmware recorded by this same commit, a successful stop-media returns HTTP 500/body code 1411. Local curl --help all documents --fail-with-body as “Fail on HTTP errors but save the body,” so this command exits nonzero and the following exit map reports failure before a workflow can perform the required read-back. Model this response as indeterminate and determine success from GetRemoteConfigurations, rather than making the known successful response a terminal refusal.

Useful? React with 👍 / 👎.

}
exit {
0 => Unit
nonzero => String "megarac stop-media POST failed"
}
}

operation CloseSession {
input { bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, csrf_token: NonEmptyStr }
output { body: String from "stdout", success: Bool from "exit_success" }
transport shell {
argv: ["curl", "--fail-with-body", "-sS", "-k", "-b", "{cookie_jar}", "-H", "X-CSRFTOKEN: {csrf_token}", "-X", "DELETE", "https://{bmc_host}/api/session"]
}
exit {
0 => Unit
nonzero => String "megarac session DELETE failed"
}
}
}
134 changes: 134 additions & 0 deletions dag/extdeps/tools/coreutils_stat.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,134 @@
module extdeps.tools.coreutils_stat

import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.access.posix { FileOwnership }
import std.types { Bool, Int, List, NonEmptyStr, String }
import std.algebra { trim }

// OBSERVING WHO OWNS A PATH, as a modeled operation. extdeps.access.posix owns the CONCEPT --
// FileOwnership is a uid and a gid, cited to the Open Group's sys/stat.h -- and this module is one
// transport realizing an observation of it, through the coreutils stat(1) utility. The split is the
// usual one: a future realization reading stat(2) directly, or reading a remote host's ownership
// over a transport, binds to the same shape rather than replacing this.
data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.gnu.org/software/coreutils/manual/html_node/stat-invocation.html"
}
}

// THE FORMAT STRING IS THE CONTRACT AND IT IS DELIBERATELY NUMERIC-FIRST. %u and %g are the uid and
// gid; %U and %G are the names the local name service resolves them to. Both are taken because they
// answer different questions and a consumer needs both: an admission decision that keys on the
// NUMBER is the one that stays correct when a name lookup fails or resolves differently on another
// host, while the NAME is what a refusal has to print for anyone to act on it.
//
// A COLON IS SAFE AS THE FIELD SEPARATOR HERE, unlike in most path contexts, because none of the
// four fields can contain one: uid and gid are decimal, and a POSIX login name is restricted to the
// portable filename character set, which excludes the colon. That is a property of the fields, not
// an assumption about the data, which is why the separator is not a configurable parameter.
service coreutils.Stat {
operation PathOwnership {
input { path: NonEmptyStr }
output {
line: String from "stdout"
success: Bool from "exit_success"
}
readonly
transport shell { argv: ["stat", "-c", "%u:%g:%U:%G", "{path}"] }
exit {
0 => Unit
nonzero => String "stat could not read the path"
}
}
}

// AN UNREADABLE PATH IS A REFUSAL, NOT AN OWNERSHIP OF NOBODY, for the same reason an unreadable
// digest is not the digest of nothing. A path that could not be observed must never be folded into
// a record that reads as an observation, because the whole value of an ownership admission is that
// something looked.
type PathOwnershipObservation
= PathOwnershipObserved {
path: NonEmptyStr
ownership: FileOwnership
owner_name: NonEmptyStr
group_name: NonEmptyStr
}
| PathOwnershipUnobservable { path: NonEmptyStr, reason: String }

fn stat_field(line: String, index: Int) -> String? {
get(xs: split(s: trim(s: line), delimiter: ":"), index: index)
}

// parse_int RETURNS AN OPTION AND THE ABSENT ARM IS TAKEN SERIOUSLY, rather than being collapsed
// to a zero the way the one other consumer of it in this repository does. A uid defaulted to 0 is
// not a neutral placeholder here: 0 IS ROOT, so an unparseable field would arrive at the admission
// as the single most privileged answer available. That is the fabricated-plausible-output failure
// aimed directly at the check this observation exists to feed.
//
// THE PARSE REFUSES ON ANY MISSING OR EMPTY FIELD rather than defaulting one. A missing owner name
// defaulted to the empty string would compare unequal to every declared principal and so present as
// a WRONG-OWNER refusal -- naming a principal, sending the reader to check an account -- when what
// actually happened is that the observation failed. Those have different remedies, so they get
// different arms.
fn coreutils_stat_path_ownership(path: NonEmptyStr) -> PathOwnershipObservation
{
let observed = coreutils.Stat.PathOwnership(path: path)
if observed.success == false {
PathOwnershipUnobservable { path: path, reason: "stat could not read the path" }
} else {
match stat_field(line: observed.line, index: 0) {
Absent => PathOwnershipUnobservable { path: path, reason: "stat printed no uid field" }
Present { value: uid_text } =>
match stat_field(line: observed.line, index: 1) {
Absent => PathOwnershipUnobservable { path: path, reason: "stat printed no gid field" }
Present { value: gid_text } =>
match stat_field(line: observed.line, index: 2) {
Absent => PathOwnershipUnobservable { path: path, reason: "stat printed no owner-name field" }
Present { value: owner } =>
match stat_field(line: observed.line, index: 3) {
Absent => PathOwnershipUnobservable { path: path, reason: "stat printed no group-name field" }
Present { value: group } =>
coreutils_stat_ownership_record(
path: path,
uid_text: uid_text,
gid_text: gid_text,
owner: owner,
group: group,
)
}
}
}
}
}
}

fn coreutils_stat_ownership_record(
path: NonEmptyStr,
uid_text: String,
gid_text: String,
owner: String,
group: String,
) -> PathOwnershipObservation {
if owner.length() == 0 || group.length() == 0 {
PathOwnershipUnobservable { path: path, reason: "stat printed an empty ownership name field" }
} else {
match parse_int(s: uid_text) {
Absent =>
PathOwnershipUnobservable { path: path, reason: "stat printed a uid field that is not an integer" }
Present { value: uid } =>
match parse_int(s: gid_text) {
Absent =>
PathOwnershipUnobservable { path: path, reason: "stat printed a gid field that is not an integer" }
Present { value: gid } =>
PathOwnershipObserved {
path: path,
ownership: FileOwnership { uid: uid, gid: gid },
owner_name: owner as NonEmptyStr,
group_name: group as NonEmptyStr,
}
}
}
}
}
Loading
Loading