§27. Changes from v4.4

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

Incorporates the spec vulnerability review of Oct 29 (findings B-1–B-18 against commit 1bc09b2).

• §5, §6, §7, §17b, §18: the bypass register docs/bypasses.md; principle 16 (name every way around); agent rule 18; no gate passes with an open High row (B-14 and the review’s appendix).
• §7: principle 6 and I14 extended from proposals to every request field (B-3); I2 states what the A–D core hash detects (B-12); I16 states the inspected set (B-2); I18 states whom the chain holds against (B-8).
• §10, §11: identity from a pidfd, never a bare pid (B-6); a caller property that matters is established by the daemon (B-3); agents are their own principals, started by planarian agent run with DynamicUser= (B-1); approval’s terminal established by the daemon (B-3); inferStops = false exempts units from residue inference, and inferred overrides stay listed until acknowledged (B-11; the review’s Critical sensitivity became this manifest option, so no proved type changes); sensitivity completeness with fail-closed defaults and a gym entry (B-5).
• §10: the boot report covers units in A, processes from C, and flags a test build (B-10, B-13).
• §12c: chain head in the signed health report for off-machine witnessing (C), measured-boot anchor (E); the external source’s sequence number in the checkpoint (B-8, B-16).
• §12d: alarms are local in A; a dead-man signal from C; the core hash covers every Planarian binary and script; a test build is an Integrity failure (B-9, B-12, B-13).
• §12e: the floor is derived from the whole system closure, with a CVE feed from B; gym case for a service-package fix (B-2).
• §12h (new): time on CLOCK_BOOTTIME for everything that does not survive a reboot; NTS recommended (B-7).
• §20, I9: the model is treated as an adversary, so its judgement is not a vector; containment is, and the model service’s sandbox is now normative, with a gym case in B (B-18; the review’s accepted row X-9 withdrawn).
• §11, §19: inferStops marked provisional, with the condition for replacing it by an importance property.
• §15, §16: test builds named and confined; socket slots reserved for administrators and sessions; agent run; new metrics (B-13, B-15, B-1).
• §17a: 𝒯 accounted as platform trust, proof-validity trust (now including the specifications, Verus, Z3, and rustc), and the internal-unproven count; every proved invariant gets a gym entry written from the English (B-4, B-14).
• Not spec changes: guarantees.md says Kani runs by hand, but CI runs it (B-17; correct the doc).