CSR: Small: Lightweight Correctness of System Software Leveraging Rust

Systems software, such as an operating system, is relied upon by the applications and services built upon it. However, due to rapidly evolving complexity, ensuring the correctness of systems software through formal verification, which provides very strong guarantees, is costly. This project leverages the type system of the Rust programming language to achieve correctness more cost-effectively, albeit with weaker guarantees, complementing formal verification. In doing so, the project targets several scientific contributions. It will develop an intralingual representation system where a system resource is represented by a linear-type instance, and its runtime management can be reasoned about at compile-time. Additionally, the project will discover and apply design patterns for operating system implementation, where correctness theorems, their assumptions, and hardware knowledge are encoded into Rust types and checked at compile-time. The project will also develop a hybrid approach that selectively employs formal and informal reasoning to further enhance intralingual design. Lastly, the project will extend the aforementioned technologies to Linux kernel modules written in Rust. This project aims to make correctness more affordable for systems software developers, thereby improving the security and reliability of computer systems, ranging from embedded devices to datacenter servers. It is expected to significantly influence the development of systems software, and consequently impact many aspects of computer users' lives. The project will foster interaction with other research fields, specifically programming languages and formal methods, by inspiring new language features and introducing additional ways to ensure correctness statically, as well as by extending the scope of formal verification to large-scale systems software. Additionally, the project will provide resources to modernize introductory systems courses and serve as a platform to engage both undergraduate and high school students in computer systems research. 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.