From 34927344345879c9c3b7fb5c79f44514c0c665aa Mon Sep 17 00:00:00 2001 From: "K. Isom" Date: Fri, 18 Sep 2026 22:13:28 -0700 Subject: [PATCH] Fix seven M3a spec review findings in policy and the audit chain Policy: a deny grant must apply at every taint; a result's label is combined over all matching grants and the longest matched path wins within a mode; a grant of / is invalid. Audit: a recovered line need not fail to parse; the writer never goes back to an earlier day's file; --accept-break verifies the whole log and the break record's fields are all checked, with a seq counted from lines; the Approval record carries the re-decision's grant and state; calls with no Result are reported. Co-Authored-By: Claude Fable 5.1 --- docs/decisions.md | 2 + docs/runbook.md | 28 +++- docs/specs/2026-09-18-m3a-decision-path.md | 165 ++++++++++++++++----- 3 files changed, 154 insertions(+), 41 deletions(-) diff --git a/docs/decisions.md b/docs/decisions.md index f08b454..aa1d25a 100644 --- a/docs/decisions.md +++ b/docs/decisions.md @@ -6,6 +6,8 @@ Newest first. A decision that changes `docs/design.md` lands in the same commit | Date | Decision | Reason | |---|---|---| +| 2026-09-18 | Spec review of M3a, policy. A `deny` grant must have `max_taint = "secret"` or the grant set is invalid. A result's `result_class` and `untrusted` are combined over every matching grant (highest class; untrusted if any says so), and within a mode the grant with the longest matched path wins before the id tie-break. A grant path of `/` is invalid. | A `deny` grant with a lower `max_taint` stopped denying once the session read a secret. With overlapping `auto` grants the id tie-break chose the label, so a secret could come back `private`. M3b mounts grant paths at the same path, where `/` would replace the tool image. | +| 2026-09-18 | Spec review of M3a, audit. A line followed by a matching `Recovery` is recovered whether or not it parses; an unparseable last line is recovered like a torn one. The writer never moves to an earlier day's file, and `Recovery` and `AcceptedBreak` go in the latest file. `--accept-break` verifies the whole log; the verifier checks an `AcceptedBreak`'s `file`, `line`, `last_good`, `prev` and `seq`, and the `seq` is counted from lines, not read from them. The `Approval` record carries the re-decision's grant and session state. The report lists allowed calls with no `Result`. | As first written, a record cut exactly before its newline made `brokerd` break its own chain; so did a clock stepped back over midnight; a break in an older file could never be accepted; and a damaged line could choose the next `seq`. | | 2026-09-18 | M3 is split. M3a is the decision path: grants and matching, session taint, the hash-chained audit log, approvals through `bxctl`, the `broker.sock` and `admin.sock` protocol, and `loopd`'s `BrokerPort`; tools do not run (the runner is a trait with a refusing implementation). M3b is the Podman runner, the four tools and the egress proxy. Review happens after each. | The security logic is reviewed before real tools run on it, as with M2a and M2b. Spec `docs/specs/2026-09-18-m3a-decision-path.md`. | | 2026-09-18 | Grant loading fails closed: one invalid grant file denies every call (`grants_invalid`) until it is fixed. M3 grants may not set `secret` or `patterns`; each tool has fixed rules for which constraints it takes. Among matching grants the most restrictive mode wins (deny, ask, auto). An approval re-decides against the current grants and taint, and runs only if the outcome is still ask or auto. | A skipped, mistyped `deny` grant would silently become an allow. Pattern-matching shell commands is a false comfort; the container is the boundary. | | 2026-09-18 | Every fail-closed state has an entry in `docs/runbook.md` with what you see, why, how to confirm, how to fix and how to check; its message ends with `see docs/runbook.md#`, and a gate script checks that every referenced entry exists. | Owner's requirement: a refusing system must come with clear, actionable remediation. | diff --git a/docs/runbook.md b/docs/runbook.md index a74a439..bc20efa 100644 --- a/docs/runbook.md +++ b/docs/runbook.md @@ -33,8 +33,10 @@ bxctl grants check It prints each problem as `:: `. Common ones: a misspelled field (unknown fields are errors); `secret` set (not supported until M4); `patterns` set (not supported); `hosts` -on a file tool or `paths` on `http_fetch`; a relative path or one with `..`, `.` or `//`; a host -with uppercase letters, a port, or an IP address; a file name with characters outside `[a-z0-9-]`. +on a file tool or `paths` on `http_fetch`; a relative path or one with `..`, `.` or `//`; the path +`/` (grant the directories you mean); a `deny` grant whose `max_taint` is not `"secret"` (it would +stop denying once the session read a secret); a host with uppercase letters, a port, or an IP +address; a file name with characters outside `[a-z0-9-]`. **Fix.** Edit the file, or move it out of `$GRANTS` while you work on it: @@ -74,13 +76,19 @@ directory 0700). Do not edit, move or delete audit files to make space: that bre ## audit-chain-broken **What you see.** `brokerd` refuses to start and prints `:: `, then this entry. -Or `bxctl audit verify` prints the same and exits 1. +Or `bxctl audit verify` prints the same and exits 1. If the break is in an older file, only +`bxctl audit verify` reports it: at an ordinary start `brokerd` checks the latest file alone. **Why.** A record does not parse, its `seq` is not the next number, its `prev` is not the hash of the line before, or a file does not continue from the one before it. Something changed the log after it was written: an edit, a deleted or reordered line, a file restored from a backup, a partial copy. `brokerd` will not add records after a history it cannot vouch for. +There is one innocent cause. After a crash `brokerd` recovers a torn last line by itself +([audit-recovered](#audit-recovered)), but if it is killed a second time while writing that +recovery record, the log is left with a line that nothing describes. The failure is then within +the last three lines of the latest file, and the last line is cut short. + **Confirm.** ```sh @@ -98,11 +106,14 @@ cp -a "$BOXMAKER_HOME/audit" ~/audit-copy-$(date +%F) brokerd serve --config --accept-break ``` -`brokerd` appends an `accepted_break` record naming the file and line, and continues from there. -Nothing is repaired or deleted. The break stays visible in every later verification. +With this flag `brokerd` checks the whole log, not only the latest file, and appends an +`accepted_break` record naming the file and line of the first failure. It continues from there. +Nothing is repaired or deleted. The break stays visible in every later verification. One accepted +break covers everything between the failure and the break record, including any further damage +there, so look at that whole stretch before accepting it. **Check.** `bxctl audit verify` prints `audit: ok` and lists the accepted break with its file and -line. A second failure later in the log needs its own accepted break. +line. Damage that happens after the break record needs its own accepted break. ## audit-recovered @@ -112,7 +123,10 @@ It starts normally. **Why.** The last record was being written when `brokerd` or the machine stopped, so the file ended without a newline. That is expected after a crash, not an error. `brokerd` kept the partial line, ended it, and wrote a `recovery` record holding its length and hash, chained from the last complete -record. The partial record was never acted on: records are written before the action they allow. +record. The partial line may even look like a whole record; it is not one, and the recovery record +takes its `seq`. It was never acted on: a record allows something only once it is on disk with its +newline. If the partial line was the `result` of a call, the call did run and its result was +never delivered; `bxctl audit verify` lists that call as unfinished. **Confirm.** `bxctl audit verify` lists the recovery with its file and line. diff --git a/docs/specs/2026-09-18-m3a-decision-path.md b/docs/specs/2026-09-18-m3a-decision-path.md index a4302b9..bd311d4 100644 --- a/docs/specs/2026-09-18-m3a-decision-path.md +++ b/docs/specs/2026-09-18-m3a-decision-path.md @@ -116,14 +116,23 @@ gives one, the line and field. | `shell` | optional | must be empty | | `http_fetch` | must be empty | required | -7. A path in `paths` is not a valid absolute path (section 3, "Paths"). +7. A path in `paths` is not a valid absolute path (section 3, "Paths"), or is `/`: "a grant of the + whole file system is not supported". 8. A host in `hosts` is not a valid host pattern (section 3, "Hosts"). +9. `mode` is `deny` and `max_taint` is not `secret`: "a deny grant must apply at every taint". **If any file is invalid, the whole set is invalid**, and every call is denied with `grants_invalid` until it is fixed. `brokerd` prints each problem, once per distinct set of problems, followed by `see docs/runbook.md#grants-invalid`. The reason: a mistyped `deny` grant that was skipped would silently turn into an allow wherever another grant matches. +Rule 9 has the same reason. A grant stops applying when the session's taint passes its +`max_taint`, so a `deny` grant with `max_taint = "private"` would stop denying as soon as the +session read a secret, and whatever `auto` grant lay behind it would take over: the model's own +actions would have removed the owner's prohibition. Rule 7 rejects `/` because M3b mounts a grant +path at the same path inside the container, where `/` would replace the tool image itself. M3b +may reserve further prefixes for the same reason. + ### Matching For a request to tool `T`, with the session's current taint `S`: @@ -131,14 +140,32 @@ For a request to tool `T`, with the session's current taint `S`: 1. Candidates are the grants whose `tool` is `T`. 2. A candidate is ruled out by the first of these that holds: it has expired (`now >= expires`); `S > max_taint`; its constraints do not cover the arguments. -3. Among those left, the most restrictive mode wins: `deny`, then `ask`, then `auto`. Ties go to - the lowest grant id in byte order. -4. If none is left, the reason is `grant_expired` if some candidate was ruled out only by expiry; +3. Among those left, the most restrictive mode wins: `deny`, then `ask`, then `auto`. Within that + mode the winner is the grant with the longest matched path (section 3, "Paths"); grants with no + matched path (`http_fetch`, and `shell` without `cwd`) all tie. Remaining ties go to the lowest + grant id in byte order. The winner is the grant that is recorded and, in M3b, the one whose + paths are mounted. +4. The result's label does not come from the winner alone. `result_class` is the highest among + all the grants left after step 2, and `untrusted` is true if any of them says so. +5. If none is left, the reason is `grant_expired` if some candidate was ruled out only by expiry; otherwise `taint_too_high` if some candidate was ruled out only by taint; otherwise `no_grant`. "Only by expiry" means the grant would have matched had it not expired: taint and constraints both pass. Likewise for taint. +Step 4 exists because grants overlap. With `a-home` (`paths = ["/home/kyle"]`, `result_class = +"private"`) and `b-keys` (`paths = ["/home/kyle/keys"]`, `result_class = "secret"`), both `auto`, +a read of `/home/kyle/keys/id` matches both. Whichever wins, the result is `secret`. The +longest-path rule then picks `b-keys`, so the mount is the narrower one. + +Two consequences for whoever writes grants: + +- An expired `deny` grant no longer denies. `expires` on a `deny` grant means "forbid this until + then". +- An `ask` grant with a lower `max_taint` than an `auto` grant over the same arguments drops out + when taint rises, and the call then runs without asking. Give the `ask` grant the higher + `max_taint`. Loading does not check this. + The outcome is one of: allowed by grant `g` (`auto`); ask, under grant `g`; denied by grant `g` (`denied_by_grant`); denied with no grant (`no_grant`, `grant_expired`, `taint_too_high`). @@ -170,7 +197,7 @@ component. Paths are compared as they are, never normalised, and matching is by | `/home/kyle/notes` | `/home/kyle/notes/../.ssh/id` | `invalid_arguments` (`..`) | | `/home/kyle/notes` | `notes/a.md` | `invalid_arguments` (relative) | | `/home/kyle/notes` | `/home/kyle//notes/./a.md` | `invalid_arguments` (`//`, `.`) | -| `/` | `/etc/passwd` | inside (a grant of `/` covers everything; allowed, not advised) | +| `/` | anything | the grant file is invalid (loading rule 7) | `brokerd` does not resolve symlinks. In M3b only the matched grant directory is mounted, at the same path, so a symlink pointing outside it points at nothing inside the container. @@ -238,7 +265,9 @@ pub enum AuditEvent { post: Option, // from M4, the Mattermost post id reason: Option, // the owner's text, for refusals outcome: DecisionRecord, // the re-decision (section 6); denied if refused or expired - }, + grant: Option, grant_sha256: Option, // as matched by the re-decision; + taint: DataClass, untrusted: bool, // the session's state at the re-decision + }, // for refused and expired: no grant, the state as it is Result { session: SessionId, call: CallId, decision: u64, status: ResultStatus, // result | failed @@ -262,7 +291,9 @@ secret into the audit log. Arguments are recorded in full; they are at most one ### The chain -- A record is one line of JSON written by serde, then `\n`. +- A record is one line of JSON written by serde, then `\n`. The line and its `\n` go out in one + `write_all`, followed by the sync; whatever the record allows happens only after the sync + returns. A line without its newline was therefore never acted on. - `hash(line)` is `proto::sha256` of the line's bytes without the `\n`. - `prev` is the hash of the previous line; the first record ever written has `prev` all zeros and `seq` 0. @@ -270,6 +301,12 @@ secret into the audit log. Arguments are recorded in full; they are at most one - The file is `audit/YYYY-MM-DD.jsonl` by the UTC date of the record's `time`. The first record of a new day starts a new file and chains from the last line of the previous file. Files are created with mode 0600; the directory is `fsync`ed after a file is created. +- The writer never goes back. If a record's date is earlier than the latest file's (the clock was + stepped back over midnight), the record goes in the latest file. Files are verified in name + order, so a record appended to an older file would break the chain. The verifier reports the + backwards time as a clock warning. +- `Recovery` and `AcceptedBreak` records always go in the latest file, whatever their date: they + belong next to the lines they describe. - `brokerd` is the only writer. It holds an exclusive `flock` on `audit/.lock` for its whole life and `fsync`s after every record. @@ -307,8 +344,10 @@ pub struct ChainReport { pub failure: Option, // the first one: file, line (1-based), what pub recoveries: Vec, pub accepted_breaks: Vec, pub abandoned: Vec, // seq of Ask decisions with no Approval after them + pub unfinished: Vec, // seq of allowed decisions, and of approvals whose + // outcome is allowed, with no Result after them pub clock_warnings: Vec, // time went backwards - pub torn_tail: Option, // last line of the last file has no newline + pub torn_tail: Option, // the last line of the last file needs recovery } ``` @@ -316,33 +355,67 @@ A line fails if it does not parse as an `AuditRecord`, its `seq` is not the next `prev` is not the hash of the line before. Files are fed in name order; a file whose first record does not chain from the previous file's last line fails at its line 1. Two cases are not failures: -- **Torn tail.** The last line of the last file has no newline. It is reported in `torn_tail`. -- **Recovered line.** A line that does not parse, immediately followed by a `Recovery` record whose - `torn_bytes` and `torn_sha256` describe exactly that line, and whose `prev` is the hash of the - line before the torn one and whose `seq` follows that line's. Reported in `recoveries`. +- **Torn tail.** The last line of the last file has no newline, or has one but does not parse (a + crash between ending a torn line and writing its `Recovery`). It is reported in `torn_tail` and + is not checked further. Treating an unparseable last line this way gives up nothing: whoever + could damage the last line could as easily remove its newline. +- **Recovered line.** A line immediately followed by a `Recovery` record whose `torn_bytes` and + `torn_sha256` describe exactly that line, whose `prev` is the hash of the line before it, and + whose `seq` follows that line's. "Immediately followed" spans files, though the writer never + produces that. **It makes no difference whether the recovered line parses**: a crash can cut a + record exactly before its newline, leaving complete JSON. A recovered line is not a record and + nothing may refer to its `seq`, which the `Recovery` record reuses. Reported in `recoveries`. -An `AcceptedBreak` record is accepted only if its `file` and `line` name the first failure found -since the last accepted break (or the start). The verifier then clears that failure, reports the -break, and continues with the break record as the new head. Lines between the failure and the -break record are not checked. +The verifier therefore holds each line back until it has seen the next one, and judges it then (or +at `finish`). + +An `AcceptedBreak` record is accepted only if all of these hold: + +- its `file` and `line` name the first failure found since the last accepted break (or the start); +- its `last_good` is the hash of the last line that verified before that failure (all zeros if + none did); +- its `prev` is the hash of the line immediately before the break record; +- its `seq` is the `seq` the failing line should have had, plus the number of lines from the + failure line up to the line before the break record (so a failure at line 7 with the break + record at line 10 adds 3). The count is of lines, not of what they say: a damaged + region must not choose the counter's value. After a deletion a later `seq` can therefore repeat + one inside the region; those lines are not vouched for, and a reference to a `seq` means the + latest record before it that has it. + +The verifier then clears that failure, reports the break, and continues with the break record as +the new head. Lines between the failure and the break record are read only to look for the break +record and are not checked, so one break covers every failure before it. + +A verifier started with `resume` has not seen the earlier files. When it meets an `AcceptedBreak` +whose `file` sorts before the first file it was given, it checks only `prev`, accepts it and +continues from it; the full verification judges the rest. ### Startup 1. Take the lock. If it is held: print "brokerd is already running" and `see docs/runbook.md#brokerd-already-running`, exit 1. -2. Verify the latest file, resumed from the last line of the file before it (if any). The earlier - files are not re-read; `bxctl audit verify` does that. -3. If the report has a torn tail: write `\n` after the torn bytes, then a `Recovery` record chained - from the line before the torn one. Print "audit: recovered a torn final line" and - `see docs/runbook.md#audit-recovered`. -4. If the report has a failure: without `--accept-break`, print the failure's file, line and what, - and `see docs/runbook.md#audit-chain-broken`, and exit 1. With `--accept-break`, append an - `AcceptedBreak` record naming it, with `last_good` the hash of the last line that verified, - `prev` the hash of the file's last line, and `seq` one more than the highest `seq` among lines - that parse (or than the failure line's predecessor if none after it parse). Print what was +2. Without `--accept-break`: verify the latest file, resumed from the last line of the file before + it (if any). That line must parse as a record, or it is the failure. The earlier files are not + re-read; `bxctl audit verify` does that. With `--accept-break`: verify every file, exactly as + `bxctl audit verify` does, because the break to accept must be the first failure of the whole + log, and it may lie in an older file that the short check never reads. +3. If the report has a failure: without `--accept-break`, write nothing, print the failure's file, + line and what, and `see docs/runbook.md#audit-chain-broken`, and exit 1. With `--accept-break`, + end a torn final line with `\n` if there is one, then append an `AcceptedBreak` record with the + four values the verifier will check (above; lines are counted across files). Print what was accepted. +4. Otherwise, if the report has a torn tail: write `\n` after the torn bytes if it is missing, + then a `Recovery` record chained from the line before the torn one. Print "audit: recovered a + torn final line" and `see docs/runbook.md#audit-recovered`. 5. `--accept-break` with no failure is an error: "nothing to accept". Exit 2. +An empty latest file (created, then a crash before its first record) is not a failure and needs +no recovery: the next record is its line 1 and chains from the file before. + +One crash is not recovered automatically: a crash while the `Recovery` record itself is being +written leaves a line that no `Recovery` describes. That is a chain failure, and the runbook entry +says so. It takes two crashes within two consecutive one-line writes. + Nothing is truncated, rewritten or deleted, ever. ## 6. Sockets and messages @@ -430,8 +503,9 @@ pub fn run(decision: Decision, runtime: &dyn Runtime) -> ToolResponse; ``` `RunSpec` has public getters and no public constructor; a `compile_fail` doctest proves it, like -`Decision`'s. `Decision` gains the parsed arguments and the matched grant (id, `result_class`, -`untrusted`, the matched path or hosts), all set by `policy`. +`Decision`'s. `Decision` gains the parsed arguments, the winning grant (id, file hash, the matched +path or hosts) and the result's label (`result_class` and `untrusted`, combined over every matching +grant as in section 3, step 4), all set by `policy`. What `run` puts in the spec, from the decision: @@ -496,8 +570,11 @@ processes, output size) are M3b's. - `bxctl grants check` prints each problem as `:: `, or `grants: ok`; exit status 1 if there are problems. - `bxctl audit verify [--home ]` reads `/audit/` itself (no daemon) and prints - `audit: ok, records, head `, then any recoveries, accepted breaks, abandoned approvals - and clock warnings, one per line; or the failure as `:: ` and exit status 1. + `audit: ok, records, head `, then any recoveries, accepted breaks, approvals "pending or + abandoned", calls "running or unfinished" and clock warnings, one per line; or the failure as + `:: ` and exit status 1. The two double names are because `bxctl` reads the + files without asking `brokerd`: an approval still waiting and a call still running look the same + on disk as ones a crash cut off. - `bxctl chat`: an `approval_pending` event prints the same two-line block as `approvals`. In the interactive mode it then asks `approve 41? [y/N] ` on stderr and reads one line from stdin; `y` sends `approve`, anything else sends `refuse`. `--say` and `--json` print the event only. @@ -539,12 +616,18 @@ first, as in M2. - **Policy tables.** Every row of every table in section 3 is a case, plus: mode precedence among three matching grants; the reason order when one candidate is expired and another has too much - taint; expiry exactly at `expires`; ties by grant id. + taint; expiry exactly at `expires`; the longest matched path winning within a mode; ties by + grant id; the `a-home` and `b-keys` example labelled `secret` whichever id sorts first; an + `untrusted = true` grant among the matches setting the flag when the winner says false; an + expired `deny` no longer denying. - **Loading.** One case per rule in "Loading", each with the problem text it must contain; one invalid file among valid ones denies a call a valid file would allow. - **Property test.** A seeded xorshift generator (no crate) makes grant sets, session taints and requests. A separate, deliberately naive oracle in the test file says what should happen; every - case must agree. Over sequences of calls: taint never goes down; every `Result` record follows a + case must agree. Two properties over single decisions, with restrictiveness ordered allowed, + ask, denied: adding a `deny` grant to a set never makes any outcome less restrictive; and a + call that is `denied_by_grant` at one taint is `denied_by_grant` at every higher taint. Over + sequences of calls: taint never goes down; every `Result` record follows a `Decision` for the same call; the fake runtime sees a call only after `allowed` or an approval. The seed is printed on failure. - **Audit.** The writer: chain across a day boundary, `seq` across files, sync on each record, the @@ -552,8 +635,22 @@ first, as in M2. middle line; a deleted line; two lines swapped; a `seq` gap; a file that does not chain from the one before; a middle line cut short. Each must fail at the right file and line in both `ChainVerifier` and `brokerd`'s startup. Not failures: a torn tail (startup writes a `Recovery`, - and the next verify reports it); an accepted break (reported by every later verify); an - `AcceptedBreak` naming the wrong line (a failure). + and the next verify reports it); an accepted break (reported by every later verify). Failures: + an `AcceptedBreak` naming the wrong line, or with the wrong `last_good`, `prev` or `seq`; a + `Recovery` whose hash or length does not match the line before it; a line no `Recovery` + describes followed by a torn `Recovery`. +- **Audit edges**, each a fixture or a scripted writer test: a torn tail that is complete JSON + lacking only its newline (recovered, and the chain verifies afterwards: this is the case a + "does not parse" rule gets wrong); an unparseable last line that has its newline (recovered + without a second newline); a torn first line of a file; an empty latest file; a clock stepped + back over midnight (the record goes in the latest file, one clock warning, the chain verifies); + a line torn on one day and recovered on the next (the `Recovery` is in the torn line's file); a + break in an older file (plain startup succeeds, `bxctl audit verify` fails, `--accept-break` + accepts it, both verify afterwards, and so does the next plain startup through `resume`); two + failures before one break record (one break covers both); a region holding a line with `seq` + 18446744073709551615 (the break's `seq` is unaffected). +- **Unfinished and abandoned.** An allowed `Decision` with no `Result` is listed in `unfinished`; + an `Ask` with no `Approval` in `abandoned`; neither is a failure. - **Audit before action.** A writer that fails on demand: the answer is `audit_unavailable` and the fake runtime's count is 0. A state writer that fails: `failed`, and the content is absent. - **Sockets.** Each admin kind on `broker.sock` and `tool_request` on `admin.sock` is `forbidden`.