Verified Paging for x86-64 in Rust

Abstract

Writing correct operating systems is hard because they interact with complex computer hardware. At the same time, their reliability is extremely important because they represent the foundation of the many other software systems relying on them. Machine-checked formal verification can provide strong guarantees about a program’s behavior in all possible situations. SeL4 and other projects have demonstrated that the complete verification of an operating system’s kernel is feasible but time-consuming. More recently, the VeriBetrKV project has shown that SMT-based verification workflows can scale to large end-to-end verification projects of low-level systems software. In this thesis we develop paging functions targeting x86-64 hardware. We implement the functions in Rust and verify them using the new SMT-based verifier Verus. Finally, we integrate the functions into a research operating system and evaluate their performance. By verifying one subsystem of an OS, we demonstrate that an approach based on Verus and state machine refinement is effective for proving complex properties about operating systems. Our work has influenced Verus’ development in multiple ways and we found and reported a large number of bugs, including ones affecting the soundness of verification results.