FMitF: Collaborative Research: RedLeaf: Verified Operating Systems in Rust

An operating system kernel provides a foundation for isolation and security in every computer system used today. Operating system kernels are trusted to provide the first line of defense for numerous mission critical systems in the face of targeted security attacks. Unfortunately, despite decades of evolution modern operating systems are faulty and vulnerable. Inheriting their core engineering technology from the first time-sharing machines, modern operating system kernels are still developed with a legacy software engineering techniques---a combination of an unsafe programming language, rudimentary concurrency primitives, and virtually no testing or verification tools. Today these systems are faulty and vulnerable. Lacking verification support, industry standard kernels make nearly every computer system on the planet vulnerable. This project will develop RedLeaf, a new operating system, and associated formal verification tools for implementing provably secure and reliable systems in the Rust programming language. RedLeaf brings together state-of-the-art results from verification, programming-language, and systems research communities in order to enable unprecedented security and reliability guarantees in low-level systems software. To achieve complete verification of the entire software stack, i.e., operating system and applications, the RedLeaf team will develop a set of new tools, a collection of techniques and engineering disciplines, and a methodology focused on rapid development of verified systems software. The RedLeaf OS will run on an embedded CPU of a medical sensor, implement a network function virtualization framework aimed at line-rate network processing, and provide a general platform for a broad range of verifiably secure systems. The operating system and associated tools will be open source, directly benefiting the broader community. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.