Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Combining Type Checking and Formal Verification for Lightweight OS Correctness

Ramla Ijaz, Kevin Boos, Lin Zhong

TL;DR

This work demonstrates a practical path to OS correctness by combining Rust's type system with selective formal verification and informal reasoning. The authors develop an Intralingual Representation System (IRS) that uses linear types and typestates to model resources as unique representations whose access is compiler-checked, and they pair this with a hybrid verification approach to extend invariants beyond what the type system alone can guarantee. Applied to Theseus memory management and the ixgbe NIC driver, the approach yields substantial proof-effort reductions (e.g., memory subsystem ratio $1:117$, ixgbe driver ratio $1:8.3$) with negligible runtime overhead, while still achieving important invariants like bijective page-frame mappings. The resulting framework supports correctness-by-construction while maintaining practicality for real systems, and it uncovers and prevents bugs that elude traditional approaches, offering a scalable path toward safer Rust-based OS software.

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.

Combining Type Checking and Formal Verification for Lightweight OS Correctness

TL;DR

This work demonstrates a practical path to OS correctness by combining Rust's type system with selective formal verification and informal reasoning. The authors develop an Intralingual Representation System (IRS) that uses linear types and typestates to model resources as unique representations whose access is compiler-checked, and they pair this with a hybrid verification approach to extend invariants beyond what the type system alone can guarantee. Applied to Theseus memory management and the ixgbe NIC driver, the approach yields substantial proof-effort reductions (e.g., memory subsystem ratio , ixgbe driver ratio ) with negligible runtime overhead, while still achieving important invariants like bijective page-frame mappings. The resulting framework supports correctness-by-construction while maintaining practicality for real systems, and it uncovers and prevents bugs that elude traditional approaches, offering a scalable path toward safer Rust-based OS software.

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.
Paper Structure (42 sections, 3 figures, 4 tables)

This paper contains 42 sections, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Background and Related Work
  3. Rust's Type System
  4. Rust for Correctness
  5. Formal Verification
  6. Other Related Work
  7. Intralingual Design
  8. Intralingual Representation System
  9. Changing Access Rights via Typestates
  10. Delegation via Ownership Transfer, Sharing, Borrowing
  11. Returning Representations via Automatic Destructors
  12. Linear Types as Proof of Work
  13. Intralingual Hardware Abstraction Layers
  14. Limitations of Intralingual Design
  15. Hybrid Approach for Correctness
  16. ...and 27 more sections

Figures (3)

  • Figure 1: The Interplay of an IRS and Formal Verification in Theseus: We create representations for Pages, Frames and PciDevices using the RepCreator, ensuring there is a 1-to-1 mapping between the hardware resource and the software representation 1, 4. Functions consume instances of Pages and Frames to transition them into the next state and to maintain the 1-to-1 mapping 2. Once PTEs are added, a Pages instance is in the Mapped state and its represented memory can be cast to other representations 3. We formally verify the cast functions to uphold uniqueness. IxgbeNIC consists of multiple representations and is unique by Rule of Composition 5.
  • Figure 2: The individual time to map, remap, and unmap a 4 KiB page does not increase when verification is added to Theseus. The results presented are the mean times for 1 page, with the error bars representing the standard deviation.
  • Figure 3: A performance comparison of ixgbe drivers demonstrates that the hybrid driver has only 5% lower maximum throughput than DPDK and has a latency profile similar to other research drivers like safe_rust pirelli2023safe. The observed latency spike at 10 Gbps is likely a hardware issue and has been reported in previous works pirelli2020tinynf-osdipirelli2023safe. In the legend, the OS for each driver is indicated alongside its name. The shaded region illustrates the range between the 5th and 95th percentiles.