Combining Type Checking and Formal Verification for Lightweight OS Correctness

TL;DR

This paper presents a hybrid approach combining Rust's type system, formal verification, and informal reasoning to improve lightweight correctness guarantees in the Theseus OS, reducing proof effort while maintaining reliability.

Contribution

It introduces a novel hybrid method that leverages Rust's type system alongside formal verification to enhance OS correctness with less proof effort.

Findings

Successfully applied to memory subsystem and Ethernet driver

Reduced proof effort compared to full formal verification

Demonstrated utility in a real open-source OS environment

Abstract

This paper reports our experience of providing lightweight correctness guarantees to an open-source Rust OS, Theseus. First, we report new developments in intralingual design that leverage Rust's type system to enforce additional invariants at compile time, trusting the Rust compiler. Second, we develop a hybrid approach that combines formal verification, type checking, and informal reasoning, showing how the type system can assist in increasing the scope of formally verified invariants. By slightly lessening the strength of correctness guarantees, this hybrid approach substantially reduces the proof effort. We share our experience in applying this approach to the memory subsystem and the 10 Gb Ethernet driver of Theseus, demonstrate its utility, and quantify its reduced proof effort.