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
110 changes: 79 additions & 31 deletions dag/gunbc/host_effect_realize.dag
Original file line number Diff line number Diff line change
Expand Up @@ -711,42 +711,90 @@ fn realize_bmcweb_session_login_on_host(
}
}

// THE VERDICT IS PRODUCED BEFORE THE WRITE, NOT CHECKED AFTER IT (DESIGN §5).
// This extraction ran `jq -r '.token // empty'`, and jq's `//` alternative makes an ABSENT
// or NULL `.token` a run that prints nothing and exits 0 — indistinguishable, at the exit
// status the caller reads, from a token that was found. The realization then wrote
// jq_run.stdout to srv3_bmcweb_token_path unconditionally and reconciled on the WRITE's
// success, so a rejected or malformed BMC login produced an EMPTY CREDENTIAL FILE reported
// as Converged: the fabricated plausible output DESIGN §5 forbids, at a credential seam.
// BmcwebTokenExtraction, not the flag, is the wall. `-e` is loudness at the transport — jq
// exits 1 on a null/false last output and 4 when the filter produced none, so jq itself
// reports the absence instead of leaving the caller to infer it from empty output — but it
// is deliberately NOT what this fold relies on, for two reasons. `-e` reads the LAST OUTPUT,
// so on an arbitrary filter it would convert a legitimate `false` or `null` extraction into
// a failure; that is why it belongs at this site, where a token is required to be a nonempty
// string, and not as a blanket flag on a general extraction operation. And `-e` still admits
// the EMPTY STRING, which is a token this seam must refuse — so the blank arm below is
// load-bearing and the flag is defence in depth. Absence has no path to Filesystem.Write
// under either. The fix is not a
// non-empty check after the write, because such a check concedes the empty file is writable
// and was in fact satisfied by editing nothing (it lived in gunbc.srv3_os_install_actuate
// `srv3_bmcweb_login` as a shell.Test.IsNonEmpty on the file this fold had just produced,
// and is deleted with this climb per DESIGN §4b dissolution-on-climb).
type BmcwebTokenExtraction =
| BmcwebTokenExtracted { token: NonEmptyStr }
| BmcwebTokenExtractRefused { reason: String }

fn bmcweb_token_extract_jq_args(response_path: String) -> List<String> {
["-e", "-r", ".token", response_path]
}

fn bmcweb_token_extraction_verdict(jq_success: Bool, jq_stdout: String) -> BmcwebTokenExtraction {
if jq_success {
let token = trim(s: jq_stdout)
if token == "" {
BmcwebTokenExtractRefused {
reason: "host_effect_apply: Srv3BmcwebTokenExtract jq -e exited zero but produced no token text for `.token` in the bmcweb login response; fail-closed, no token file written.",
}
} else {
BmcwebTokenExtracted { token: token as NonEmptyStr }
}
} else {
BmcwebTokenExtractRefused {
reason: "host_effect_apply: Srv3BmcwebTokenExtract jq -e refused: `.token` is absent, null or false in the bmcweb login response (a rejected or malformed BMC login); fail-closed, no token file written.",
}
}
}

fn realize_bmcweb_token_extract_body(
intent: HostEffectIntent,
) -> Reconciliation<HostEffectIntent, HostEffectEvidence> {
match srv3_tool_bin_path(tool_name: jq_cli_tool.name, transport: LocalShell) {
Present { value: jq_path } => {
let jq_run = gunbc.WitnessBin.Run(
workdir: "/",
bin_path: jq_path,
args: ["-r", ".token // empty", srv3_bmcweb_login_response_path],
)
if jq_run.success {
let write = Filesystem.Write(path: srv3_bmcweb_token_path, content: jq_run.stdout)
srv3_shell_reconcile(
observed: ShellExecObserved {
exit_code: if write.success { 0 } else { 1 },
success: write.success,
stdout: "",
stderr: if write.success {
""
} else {
"host_effect_apply: Srv3BmcwebTokenExtract token write failed; fail-closed"
},
},
intent: intent,
)
} else {
srv3_shell_reconcile(
observed: ShellExecObserved {
exit_code: 1,
success: false,
stdout: "",
stderr: "host_effect_apply: Srv3BmcwebTokenExtract jq failed; fail-closed",
},
intent: intent,
)
}
let jq_run = gunbc.WitnessBin.Run(
workdir: "/",
bin_path: jq_path,
args: bmcweb_token_extract_jq_args(response_path: srv3_bmcweb_login_response_path),
)
match bmcweb_token_extraction_verdict(jq_success: jq_run.success, jq_stdout: jq_run.stdout) {
BmcwebTokenExtracted { token: token } => {
let write = Filesystem.Write(path: srv3_bmcweb_token_path, content: token as String)
srv3_shell_reconcile(
observed: ShellExecObserved {
exit_code: if write.success { 0 } else { 1 },
success: write.success,
stdout: "",
stderr: if write.success {
""
} else {
"host_effect_apply: Srv3BmcwebTokenExtract token write failed; fail-closed"
},
},
intent: intent,
)
}
BmcwebTokenExtractRefused { reason: why } =>
srv3_shell_reconcile(
observed: ShellExecObserved {
exit_code: 1,
success: false,
stdout: "",
stderr: why,
},
intent: intent,
)
}
}
Absent =>
srv3_shell_reconcile(
Expand Down
11 changes: 7 additions & 4 deletions dag/gunbc/srv3_os_install_actuate.dag
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,13 @@ func srv3_bmcweb_session_login() -> ProcessExit
}
}

// THE EMPTY-TOKEN CHECK THAT STOOD IN THIS FOLD IS DELETED, NOT MOVED (DESIGN §4b,
// dissolution on climb). It ran shell.Test.IsNonEmpty on srv3_bmcweb_token_path — the file
// the extract step had just written — so it conceded that writing an empty credential file
// was a reachable state and merely reported it afterwards. gunbc.host_effect_realize
// `bmcweb_token_extraction_verdict` now refuses an absent, null or blank token BEFORE
// Filesystem.Write, so a converged extract cannot have produced an empty file and a second
// reading of that file has nothing left to discover.
func srv3_bmcweb_session_login_resolved(resolution: BmcCredentialResolution) -> ProcessExit
uses net: std.resources.Network
{
Expand Down Expand Up @@ -97,10 +104,6 @@ func srv3_bmcweb_session_login_resolved(resolution: BmcCredentialResolution) ->
_ => return extract_exit
}

let verify = shell.Test.IsNonEmpty(path: srv3_bmcweb_token_path)
if verify.nonempty == false {
return exit_failure(reason: "bmcweb-login: empty token — check BMC credentials and /login response")
}
ExitSuccess
}

Expand Down
68 changes: 68 additions & 0 deletions dag/test/claim/srv3_host_effect_apply_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,14 @@
module test.claim.srv3_host_effect_apply_witness

import std.dissolution { dissolution_description }
import gunbc.srv3_actuate_shell_paths { srv3_bmcweb_login_response_path }
import gunbc.host_effect_realize {
bmcweb_token_extract_jq_args,
bmcweb_token_extraction_verdict,
BmcwebTokenExtraction,
BmcwebTokenExtracted,
BmcwebTokenExtractRefused,
}

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down Expand Up @@ -250,3 +258,63 @@ test fn srv3_nbd_proxy_serve_realize_layer_dissolves_via_host_effect_nbd_proxy_s
&& string_contains(s: dissolution_description(condition: host_effect_nbd_proxy_serve_dissolution_trigger), pattern: "P6 Part 2")
}


// THE FIVE WITNESSES BELOW DISCRIMINATE THE BMCWEB TOKEN-EXTRACT FAIL-OPEN.
// jq's `// empty` alternative turns an absent or null `.token` into a run that
// exits 0 and prints nothing, so the pre-fix realization wrote an EMPTY file to
// srv3_bmcweb_token_path and reconciled Converged — a rejected BMC login
// reported as a successful convergence at a credential seam (DESIGN §5,
// fabricated plausible output). The verdict now lives in
// bmcweb_token_extraction_verdict, ahead of the write, so an absent token has no
// path to Filesystem.Write at all rather than being caught after the fact.
//
// THE ARGV CLAIM IS ABOUT THE FILTER, NOT THE FLAG. It asserts that the filter does not
// carry an absence-swallowing alternative — the exact defect as found — and deliberately
// does NOT assert the `-e` spelling. `-e` is loudness at the transport: it makes jq itself
// report the absence rather than leaving the caller to infer it from empty output, and the
// argv-migration lane will delete this flattened-argv form outright, so pinning its spelling
// would pin a deletion-bound artifact instead of the requirement. The WALL is the verdict
// below, which refuses blank stdout on its own — that is what makes `-e` optional rather
// than load-bearing here, and it is also why `-e` alone would be insufficient: jq exits zero
// on an empty-STRING token, which the blank arm catches and the flag does not.
test fn witness_bmcweb_token_extract_argv_demands_a_value() -> Bool {
let argv = bmcweb_token_extract_jq_args(response_path: srv3_bmcweb_login_response_path)
let surface = fold(
argv,
init: "" as String,
f: (acc, word) => if acc == "" { word } else { concat(acc, concat(" ", word)) },
)
string_contains(s: surface, pattern: ".token")
&& !string_contains(s: surface, pattern: "// empty")
&& string_contains(s: surface, pattern: srv3_bmcweb_login_response_path)
}

test fn witness_bmcweb_token_extract_absent_token_refuses_typed() -> Bool {
match bmcweb_token_extraction_verdict(jq_success: true, jq_stdout: "") {
BmcwebTokenExtractRefused { reason: why } =>
string_contains(s: why, pattern: "Srv3BmcwebTokenExtract")
&& string_contains(s: why, pattern: "fail-closed")
BmcwebTokenExtracted { token: _ } => false
}
}

test fn witness_bmcweb_token_extract_blank_token_refuses_typed() -> Bool {
match bmcweb_token_extraction_verdict(jq_success: true, jq_stdout: "\n") {
BmcwebTokenExtractRefused { reason: _ } => true
BmcwebTokenExtracted { token: _ } => false
}
}

test fn witness_bmcweb_token_extract_jq_nonzero_refuses_typed() -> Bool {
match bmcweb_token_extraction_verdict(jq_success: false, jq_stdout: "") {
BmcwebTokenExtractRefused { reason: _ } => true
BmcwebTokenExtracted { token: _ } => false
}
}

test fn witness_bmcweb_token_extract_present_token_extracts_trimmed() -> Bool {
match bmcweb_token_extraction_verdict(jq_success: true, jq_stdout: "3wMhV2QcT0k\n") {
BmcwebTokenExtracted { token: token } => (token as String) == "3wMhV2QcT0k"
BmcwebTokenExtractRefused { reason: _ } => false
}
}
Loading