Verification

TCB Discipline

How SlopOS keeps the trusted base measurable

The trusted computing base is the code that can violate Rust's safety guarantees if it is wrong. In SlopOS, that should be mostly OSTD.

Measurement

just tcb-ratio

The measurement counts unsafe lines in slopos-ostd against total kernel Rust lines in the actual kernel dependency closure. The current public target is less than 1 percent.

Read it as a trend rather than as a TCB fraction comparable to other projects'. The denominator is raw first-party lines, including the vendored DWARF reader, and published comparators measure post-LTO linked code size. The number that actually bounds what has to be trusted is the size of OSTD's exported obligation surface: its pub unsafe fns, its pub unsafe traits, and, the one that matters most, the safe functions that still carry a # Safety section. A # Safety section on a function that is not unsafe fn says a safe caller can break it, which is the property the whole arrangement exists to rule out. That count is ratcheted and may fall but never rise. It now stands at zero: every contract the gate once counted turned out to be expressible as a capability witness, a validated newtype, a linear handle, or a sealed trait.

Source Gates

GatePurpose
Unsafe boundaryKeep unsafe out of kernel crates outside OSTD, and assert every crate the kernel links carries the lint
Unsafe expansionKeep macro-injected unsafe out of what the compiler actually sees
Registry sectionsKeep the built image to the linker sections the script declares
Contract surfaceRatchet OSTD's safe functions that still carry a caller obligation
Allocation boundaryKeep direct allocation policy inside OSTD
Async boundaryKeep async out of kernel crates
Stack boundCatch excessive final stack frames
Wait predicate disciplineKeep wait predicates side-effect disciplined

Allowed exemptions outside OSTD

The exemptions are enumerated rather than described, and each has a reason recorded beside it:

  • The allocator entry point in the kernel binary, which must name alloc directly.
  • Three C-ABI entry points whose callers are assembly, so the symbols have to resolve at link time.
  • Linker-section attributes, but only for sections the linker script declares. OSTD owns every label, so a kernel crate cannot name one of its own.
  • unsafe impl of a small set of OSTD traits, listed with what discharges each: the Pod/Zeroable derives check representation and field bounds; the hermetic-state and PCR-stack markers carry an obligation that genuinely belongs to the invoking crate.

None of these opens a path to runtime unsafe in an ordinary kernel crate, and the expansion audit fails on anything not in the list.

Contributor Rule

If a change appears to require unsafe, first ask whether it belongs in OSTD as a small safe API. If it does, give the unsafe block a concrete safety argument, add or extend Miri coverage where practical, and consider whether the invariant belongs in the Verus proof set.

On this page