kyle/boxmaker
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fix seven M3a spec review findings in policy and the audit chain

Browse Source 
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 <noreply@anthropic.com>
This commit is contained in:
kyle
2026-09-18 22:13:28 -07:00
co-authored by Claude Fable 5.1
parent 180ef28833
commit 3492734434
3 changed files with 154 additions and 41 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/decisions.md
+2
View File
@@ -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#<entry>`, and a gate script checks that every referenced entry exists. | Owner's requirement: a refusing system must come with clear, actionable remediation. |
docs/runbook.md
+21 -7
View File
@@ -33,8 +33,10 @@ bxctl grants check
It prints each problem as `<file>:<line>: <problem>`. 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 `<file>:<line>: <what>`, 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 <path> --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.
docs/specs/2026-09-18-m3a-decision-path.md
+131 -34
View File
@@ -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<String>, // from M4, the Mattermost post id
reason: Option<String>, // the owner's text, for refusals
outcome: DecisionRecord, // the re-decision (section 6); denied if refused or expired
},
grant: Option<String>, grant_sha256: Option<Hash32>, // 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<ChainFailure>, // the first one: file, line (1-based), what
pub recoveries: Vec<Location>, pub accepted_breaks: Vec<Location>,
pub abandoned: Vec<u64>, // seq of Ask decisions with no Approval after them
pub unfinished: Vec<u64>, // seq of allowed decisions, and of approvals whose
// outcome is allowed, with no Result after them
pub clock_warnings: Vec<Location>, // time went backwards
pub torn_tail: Option<Location>, // last line of the last file has no newline
pub torn_tail: Option<Location>, // 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 `<file>:<line>: <problem>`, or `grants: ok`; exit
status 1 if there are problems.
- `bxctl audit verify [--home <path>]` reads `<home>/audit/` itself (no daemon) and prints
`audit: ok, <n> records, head <hex>`, then any recoveries, accepted breaks, abandoned approvals
and clock warnings, one per line; or the failure as `<file>:<line>: <what>` and exit status 1.
`audit: ok, <n> records, head <hex>`, then any recoveries, accepted breaks, approvals "pending or
abandoned", calls "running or unfinished" and clock warnings, one per line; or the failure as
`<file>:<line>: <what>` 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`.