docs: the security track plan carries its live state on main
The plan is the only progress view from a plain main checkout, and the work lands on a feature branch that reaches main a group at a time — so between merges the file said less than was true. It now opens with where the work is, which branch carries it, and what main itself holds, refreshed on main after every phase rather than at merges alone.
This commit is contained in:
parent
ac01f627d1
commit
73aea4582b
|
|
@ -31,13 +31,39 @@ the logging/USB-lifecycle track).
|
|||
|
||||
## Status
|
||||
|
||||
**Live state — updated on `main` after every phase, so this file read from a
|
||||
plain `main` checkout always tells the truth about where the work is.**
|
||||
|
||||
| | |
|
||||
|---|---|
|
||||
| Working on | **P3** — green at 109/109, adversarial review running, not yet committed |
|
||||
| Branch carrying it | `feat/security-group-2` (pushed to origin) |
|
||||
| On `main` | through the group 1 merge (`f3bc23c`): Phase 0, PM, H1 |
|
||||
| Committed on the branch, awaiting the group 2 merge | P1 (`1ff0991`), P2 (`1379b69`) |
|
||||
| Suite | 109 cases, all passing |
|
||||
| Last updated | 2026-08-01 |
|
||||
|
||||
A checkbox below means the phase met its definition of green and was
|
||||
committed — on the branch named above, which reaches `main` at the next
|
||||
group boundary.
|
||||
|
||||
- [x] **Phase 0** — baseline: suite green on `main` (106/106, 2026-07-31; `zig build` + `zig build test` clean at 9a32380), plan committed
|
||||
- [x] **PM** — path-migration flag-day (`/etc`→`/system/configuration`, `/var/log`→`/system/logs`, `/mnt/usb`→`/volumes/usb`; vfs carve-out for the two writable `/system` subtrees, FAT's `/var` mount split in two; suite 106/106)
|
||||
- [x] **H1** — the `user-memory` module; nine stragglers converted; leaf U/S+W checks (plus physmap-coverage confirmation, so an `mmio_map`'d buffer cannot fault ring 0 — this also closes the same hazard on the IPC path; `fs_resolve`'s out-capacity bound made overflow-safe; suite 107/107)
|
||||
- [x] **merge** group 1 → main, push (f3bc23c, 2026-07-31)
|
||||
- [ ] **P1** — envelope module + `Define`; vfs `NodeKind.protocol` + open-reply-capability; client `Channel`
|
||||
- [ ] **P2** — registry in init; `/protocol` reserved; ServiceId flag-day (11 binds, 17 lookups)
|
||||
- [ ] **P3** — open grants: `protocol.csv` enforcement, denial test
|
||||
- [x] **P1** — envelope module + `Define`; vfs `NodeKind.protocol` + open-reply-capability; client `Channel` (mechanics only, nothing converted; suite unchanged at 107)
|
||||
- [x] **P2** — registry in init; `/protocol` reserved; ServiceId flag-day (11 binds, 17 lookups; `protocol.csv` grants, chain-attested identity, dead-owner rebind; the kernel's endpoint-death sweep generalized off the retired registry; suite 108/108). Three adversarial review rounds closed six defects a green suite had missed: a forged power event could shut the machine down; the ping path leaked a capability per call, first in init and then in the shared harness; supervisor attestation by name was defeated by a laundering deputy; and the kernel let any handle-holder bind signals, timers, exits and IRQs to an endpoint it did not own.
|
||||
- [x] **P3** — open grants: `protocol.csv` enforcement, denial test. `onOpen`
|
||||
consults the manifest with the same chain-attested identity a bind uses, and a
|
||||
refused caller gets the *same* answer as one naming a contract nobody bound —
|
||||
`-ENOENT`, no capability, the same reply bytes, no log line, and both questions
|
||||
asked on every open so there is nothing to time. Twenty-seven `open` rows cover
|
||||
the whole live client set. One wrinkle the plan had not foreseen: the driver
|
||||
tree is three deep (device manager → PS/2 bus → keyboard/mouse) and attestation
|
||||
is one hop, so a legitimate grandchild read exactly like a laundering deputy;
|
||||
the manifest gained a third permission, `supervise`, which names an authorized
|
||||
supervising task per contract and is deliberately **open-only**, leaving P2's
|
||||
bind attestation and every refusal it makes untouched (suite 109/109)
|
||||
- [ ] **merge** group 2 → main, push
|
||||
- [ ] **P4a** — clean protocols rebased onto `Define` (vfs, block, display, scanout, input)
|
||||
- [ ] **P4b** — misfit protocols rebased (device-manager, power, usb-transfer)
|
||||
|
|
@ -87,6 +113,35 @@ that implements it.
|
|||
`init` for init's own children, `kernel` for harness-spawned fixtures),
|
||||
not in extra init.csv columns — today every post-path init.csv field is
|
||||
argv, and overloading that is ambiguous. init parses both files.
|
||||
*(P2 spelling: the supervisor column carries the binary exactly as the
|
||||
kernel stamped it, so init's own children say `/system/services/init` and
|
||||
the drivers say `/system/services/device-manager`; `kernel` stays a bare
|
||||
word because a kernel task has no binary. A trailing `*` on any field
|
||||
matches a subtree, which is how decision 4's `/test/` rule is expressed.)*
|
||||
*(Clarification, 2026-08-01: the supervisor column names **the authorized
|
||||
supervising task, matched by identity** — the binary is how the row spells
|
||||
it, but init checks the task id. `kernel` is satisfied only by supervisor
|
||||
id 0 (which only the kernel confers — user `system_spawn` always stamps the
|
||||
caller); init's own path only by this init's task id; any other path only by
|
||||
a task init spawned itself or one the kernel spawned. Matching the supervisor
|
||||
by *name* alone is defeated by a laundering deputy — an attacker runs its own
|
||||
instance of `/system/services/init`, has that spawn `/system/services/input`,
|
||||
and both stamped names satisfy the row while the chain is entirely the
|
||||
attacker's. Walking to the root of the chain does not fix it either, since
|
||||
the laundered chain still roots at the real PID 1.)*
|
||||
*(P3 amendment: a third permission, `supervise`, joins `bind|open`. One-hop
|
||||
attestation cannot express the one three-deep chain in the tree — the device
|
||||
manager starts the PS/2 bus, and the bus starts the keyboard and mouse
|
||||
drivers — and nothing structural tells that chain apart from the laundering
|
||||
deputy, since both are a granted binary spawned by a granted binary. Only
|
||||
policy can: a `supervise` row names the authorized supervising task the way
|
||||
every other row names a claimant (binary, its own supervisor, the contract it
|
||||
concerns), and an `open` row may then name that task in its supervisor
|
||||
column. The delegate is itself attested the ordinary strict way, so the chain
|
||||
still anchors in init or the kernel one hop above it and the recursion stops
|
||||
there. It is **open-only** on purpose — a delegate may vouch for what its
|
||||
children *reach*, never for what they *claim* — so the bind path is
|
||||
byte-for-byte P2's and the laundering-deputy refusal is untouched.)*
|
||||
4. **Test fixtures bind under `/protocol/test/...`**, granted to any
|
||||
binary whose path starts `/test/` — the subtree-scoping rule from the
|
||||
design doc, dogfooded. `shared_memory_test` (the borrowed-ServiceId
|
||||
|
|
@ -115,6 +170,10 @@ that implements it.
|
|||
process-test) either spawn init first or move to init.csv-driven
|
||||
scenario boots — resolved per-case in P2 with the suite as the
|
||||
arbiter.
|
||||
*(P2 resolution: init gained a `registry` argv role — it mounts
|
||||
`/protocol`, reads the grants, and starts no services — and each affected
|
||||
case calls `spawnRegistry(rd)` before its own providers. Every case keeps
|
||||
its own spawn set, so no scenario had to be re-shaped.)*
|
||||
10. **The capsule-staleness caveat is documented, not fixed.** On-volume
|
||||
edits to `/system/configuration/*.csv` do not reach the initrd copy
|
||||
the loader boots (capsule shadows tree). Same drift exists today with
|
||||
|
|
@ -277,6 +336,34 @@ Every existing scenario doubles as conversion proof. Suite 108.
|
|||
the first succeeds and the second fails identically to not-found. Suite
|
||||
109.
|
||||
|
||||
*Landed. Four things the plan did not foresee, recorded because P4 and P5
|
||||
inherit them:*
|
||||
|
||||
- *`supervise` — decision 3's amendment. The PS/2 keyboard and mouse drivers
|
||||
are started by the PS/2 bus driver, which the device manager started: the
|
||||
tree's one three-deep chain, and one hop deeper than attestation reaches.
|
||||
Nothing structural separates it from the laundering deputy, so the manifest
|
||||
says which delegate is authorized, per contract. Open-only, so P2's bind
|
||||
attestation is unchanged.*
|
||||
- *Indistinguishability is a claim about work, not only about bytes. `onOpen`
|
||||
refreshes the process table, identifies the caller, scans the grants and
|
||||
scans the bindings on **every** open and forms one verdict at the end; and
|
||||
it logs nothing on any branch, because `klog_read` is ungated (a line
|
||||
written on one branch is a line the refused caller can read) and a serial
|
||||
line is milliseconds it could time. The operator's diagnosis is the pair the
|
||||
namespace publishes anyway: `readdir /protocol` for what is bound, the
|
||||
manifest for who may reach it.*
|
||||
- *The fixture is `protocol-denied-test`, and its scenario boots the **input
|
||||
service** so the forbidden name is genuinely bound — the fixture reads the
|
||||
namespace listing to prove it before asking for it. Without a live provider
|
||||
the case would be comparing two boot races and asserting nothing.*
|
||||
- *Two channels stay open by design, named rather than papered over: `readdir`
|
||||
over `/protocol` lists every bound name to anyone (deliberate — the tree is
|
||||
diagnosable), and `/system/configuration/protocol.csv` is world-readable on
|
||||
the `/system` mount. Stage one hides neither the set of contracts nor the
|
||||
policy; what it removes is the **oracle in the reply**, which is what stage
|
||||
two's parked and faked opens depend on.*
|
||||
|
||||
## P4a — clean protocols onto Define
|
||||
|
||||
vfs, block, display, scanout, input — the modules whose shapes map
|
||||
|
|
|
|||
Loading…
Reference in New Issue