Leveraging Rust for Lightweight OS Correctness

This paper reports our experience of providing lightweight correctness guarantees to an open-source Rust-based OS, Theseus. First, we report new developments in intralingual design that leverage Rust's type system to enforce invariants at compile time, trusting the Rust compiler. Second, we develop a hybrid proof approach that combines formal verification, type checking, and informal reasoning. By lessening the strength of correctness guarantees, this hybrid approach substantially lowers the proof burden. We share our experience of applying this approach to the memory subsystem of Theseus, demonstrate its utility, and quantify its reduced proof effort.