Compare commits
1
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
73aea4582b |
@@ -31,13 +31,39 @@ the logging/USB-lifecycle track).
|
|||||||
|
|
||||||
## Status
|
## 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] **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] **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] **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)
|
- [x] **merge** group 1 → main, push (f3bc23c, 2026-07-31)
|
||||||
- [ ] **P1** — envelope module + `Define`; vfs `NodeKind.protocol` + open-reply-capability; client `Channel`
|
- [x] **P1** — envelope module + `Define`; vfs `NodeKind.protocol` + open-reply-capability; client `Channel` (mechanics only, nothing converted; suite unchanged at 107)
|
||||||
- [ ] **P2** — registry in init; `/protocol` reserved; ServiceId flag-day (11 binds, 17 lookups)
|
- [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.
|
||||||
- [ ] **P3** — open grants: `protocol.csv` enforcement, denial test
|
- [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
|
- [ ] **merge** group 2 → main, push
|
||||||
- [ ] **P4a** — clean protocols rebased onto `Define` (vfs, block, display, scanout, input)
|
- [ ] **P4a** — clean protocols rebased onto `Define` (vfs, block, display, scanout, input)
|
||||||
- [ ] **P4b** — misfit protocols rebased (device-manager, power, usb-transfer)
|
- [ ] **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),
|
`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
|
not in extra init.csv columns — today every post-path init.csv field is
|
||||||
argv, and overloading that is ambiguous. init parses both files.
|
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
|
4. **Test fixtures bind under `/protocol/test/...`**, granted to any
|
||||||
binary whose path starts `/test/` — the subtree-scoping rule from the
|
binary whose path starts `/test/` — the subtree-scoping rule from the
|
||||||
design doc, dogfooded. `shared_memory_test` (the borrowed-ServiceId
|
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
|
process-test) either spawn init first or move to init.csv-driven
|
||||||
scenario boots — resolved per-case in P2 with the suite as the
|
scenario boots — resolved per-case in P2 with the suite as the
|
||||||
arbiter.
|
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
|
10. **The capsule-staleness caveat is documented, not fixed.** On-volume
|
||||||
edits to `/system/configuration/*.csv` do not reach the initrd copy
|
edits to `/system/configuration/*.csv` do not reach the initrd copy
|
||||||
the loader boots (capsule shadows tree). Same drift exists today with
|
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
|
the first succeeds and the second fails identically to not-found. Suite
|
||||||
109.
|
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
|
## P4a — clean protocols onto Define
|
||||||
|
|
||||||
vfs, block, display, scanout, input — the modules whose shapes map
|
vfs, block, display, scanout, input — the modules whose shapes map
|
||||||
|
|||||||
Reference in New Issue
Block a user