OSTD Trusted Core
What slopos-ostd owns
slopos-ostd is the Operating System Trusted Domain. Every runtime-unsafe
kernel mechanism belongs here or behind its safe APIs.
Main Responsibilities
| Area | Examples |
|---|---|
| CPU and arch | MSRs, CR3, CPUID, xsave, TSC, APIC MSR helpers |
| GDT/TSS/syscall data | Per-CPU descriptor tables, RSP0, syscall scratch slots |
| IRQ and exception substrate | IDT data, interrupt frames, raw handlers, IST-sensitive paths |
| Memory | frames, user frames, VM cursors, heap, DMA, I/O memory |
| Sync | spin locks, wait queues, event bus, intrusive lists, RCU-like helpers |
| Tasks | task handles, scheduler registry, kernel task internals |
| User access | user pointers, user-copy helpers, user contexts |
| FFI and link sections | Edition 2024 unsafe attribute wrappers, extern declarations |
| Test support | Hermetic state, architecture probes, Miri-facing tests |
Safe API Contract
Higher kernel crates call OSTD helpers instead of spelling raw unsafe blocks. That indirection is the whole design, not a workaround: the unsafe operation lives in the trusted crate, and a service crate reaches it through an API the type system checks.
The property it rests on is that those APIs are sound: no possible
safe caller can cause undefined behaviour. Folding unsafe behind a wrapper
that holds is the framekernel working. Folding it behind a wrapper that
merely documents what the caller must not do is not: the fault then lands
in OSTD's code while the cause is an ordinary safe call somewhere else, which
is the debugging cost of a trusted-core bug without the containment the
trusted core is supposed to buy. The gate that ratchets OSTD's remaining
# Safety-bearing safe functions exists to keep that set shrinking.
Typical examples:
- Use
KBox,KVec,KArc, andPinBoxinstead of directalloc. - Use
UserPtr,UserSlice, and user-copy wrappers at syscall boundaries. - Use OSTD frame and VM cursor APIs instead of manual page-table mutation.
- Use OSTD intrusive-list roles instead of open-coded raw task links.
- Use OSTD FFI macros for required
extern "C"symbols, andregistry_entry!for linker-section items. OSTD owns the section labels, so a kernel crate names a registry rather than a string. - Use
#[derive(SlotFields)]and thewrite_field!family to initialise a large struct in place; the field tokens are built fromoffset_of!and cost no unsafe at the call site.
Audited-Only Surface
Not every OSTD module is proved. The verified set focuses on memory-safety critical logic; the remaining unsafe modules are audited, require safety notes, and are covered by Miri where feasible.
The SlopRing volatile UFrame accessors are a good example: their byte-copy and
acquire/release behavior is small and audited, but the weak-memory protocol is
not modeled by Verus.