Kahlert School of Computing Assistant Professor Anton Burtsev is a recipient of the 2023 Amazon Research Award for his research aimed at developing a new operating system, Atmosphere, that utilizes advances in programming languages and formal verification for constructing a formally verified operating system kernel. The $50K grant is one of 28 selected in the Automated Reasoning category.
“A grant from Amazon illustrates the potential of Prof. Burtsev’s research for large-scale, practical impact on the challenges faced by industry,” said Prof. Mary Hall, Director of the Kahlert School of Computing.
The exclusive authority of an operating system kernel makes it an attractive target for security attacks. Given the reliance on the large trusted computing base of the kernel, the entire system is at risk without the secure foundation provided by a kernel, even if application logic is verified. With the $50K grant from Amazon, Prof. Burtsev will address the challenge of developing an operating system, called Atmosphere, that is provably secure and reliable. Today, lacking security guarantees, industry-standard kernels make nearly every current computer system on the planet vulnerable to attacks that attempt to exploit these problems.
Modern operating system kernels are inherently complex. A typical kernel must adhere to multiple allocation, synchronization, access control, and object lifetime conventions. As a result, the code for the kernel is routinely affected by the introduction of bugs and vulnerabilities. The root causes of these vulnerabilities include logical and design errors related to low-level reasoning about intricate details of object lifetimes and synchronization, integer and buffer overflows, improper memory remapping, improper handling of uninitialized and freed data, missing pointer and permission checks, division by zero, infinite loops, and data races.
To address these challenges, Atmosphere leverages recent advances in the field of automated formal verification. Atmosphere will be developed in a safe language, Rust, that provides the foundation for lightweight, fine-grained isolation of traditionally monolithic kernel subsystems. Lightweight isolation enables new compartmentalized kernel organization that creates the foundation for modular verification. The system is structured as a collection of isolated subsystems that do not share state. The simplification of the verification of programming languages in Atmosphere is centered around the idea of restricted ownership discipline implemented by Rust. To that end, Atmosphere leverages a recent verification toolchain, Verus, that implements Dafny-like verification for Rust.
The ability to develop verified code at a speed that is comparable to traditional non-verified development enables a new level of trust in the software we use on a daily basis. “It took 20 person-years to develop the first fully-verified microkernel, seL4. We hope, however, that advances in automated verification would allow us to build a similar system in only a fraction of the time,” Prof. Burtsev said.