Security Verification Track Registry

The S.x labels used across this manual are registry identifiers for the Security Verification Track. They are not product stages. When a section mentions one of these labels, read it as shorthand for the track name below.

• S.1 — CI bootstrap. Status: Landed.
• S.2 — Miri and proptest on capos-lib. Status: Landed.
• S.3 — Manifest and mkmanifest fuzzing. Status: Landed.
• S.4 — Ring Loom harness. Status: Landed.
• S.5 — Kani on capos-lib. Status: Initial bounded gate landed.
• S.6 — Security review docs stay aligned. Status: Ongoing.
• S.7 — Stage-6-aware security refresh. Status: Planned/ongoing.
• S.8 — Untrusted-service hardening gate. Status: Planned.
• S.9 — Authority graph and resource accounting. Status: Design landed.
• S.10 — Supply-chain and generated-code trusted computing base. Status: Partially landed.
• S.11 — Device and DMA isolation gate. Status: Design accepted; implementation gates open.
• S.12 — Kani harness bounds refresh. Status: Planned.
• S.13 — ELF parser arbitrary-input coverage. Status: Landed.
• S.14 — Telnet IAC filter fuzz coverage. Status: Landed.
• S.15 — Telnet differential round-trip and line-discipline extraction. Status: Landed.
• S.16 — Ring SQE wire-validation extraction and fuzz target. Status: Landed.
• S.17 — Sanitizers on host tests. Status: Planned.

Subtracks Used In This Manual

• S.10.0 under S.10 — Trusted build input inventory.
• S.10.2 under S.10 — Generated-code drift check.
• S.10.3 under S.10 — Dependency policy and no_std review gate.
• S.11.1 under S.11 — DMA capability invariants.
• S.11.2 under S.11 — Userspace-driver ownership-transition gate.

The S.11.2.0 through S.11.2.9 labels in the DMA chapter are local checklist rows for the userspace-driver transition gate. They are acceptance criteria under S.11.2, not separate project tracks.