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.
| Track | Name | Status |
|---|---|---|
| S.1 | CI bootstrap | Landed |
| S.2 | Miri and proptest on capos-lib | Landed |
| S.3 | Manifest and mkmanifest fuzzing | Landed |
| S.4 | Ring Loom harness | Landed |
| S.5 | Kani on capos-lib | Initial bounded gate landed |
| S.6 | Security review docs stay aligned | Ongoing |
| S.7 | Stage-6-aware security refresh | Planned/ongoing |
| S.8 | Untrusted-service hardening gate | Planned |
| S.9 | Authority graph and resource accounting | Design landed |
| S.10 | Supply-chain and generated-code trusted computing base | Partially landed |
| S.11 | Device and DMA isolation gate | Design accepted; implementation gates open |
| S.12 | Kani harness bounds refresh | Planned |
| S.13 | ELF parser arbitrary-input coverage | Landed |
| S.14 | Telnet IAC filter fuzz coverage | Landed |
| S.15 | Telnet differential round-trip and line-discipline extraction | Landed |
| S.16 | Ring SQE wire-validation extraction and fuzz target | Landed |
| S.17 | Sanitizers on host tests | Planned |
Subtracks Used In This Manual
| Subtrack | Parent | Meaning |
|---|---|---|
| S.10.0 | S.10 | Trusted build input inventory |
| S.10.2 | S.10 | Generated-code drift check |
| S.10.3 | S.10 | Dependency policy and no_std review gate |
| S.11.1 | S.11 | DMA capability invariants |
| S.11.2 | 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.