FMitF: Collaborative Research: Track I: Finding and Eliminating Bugs in Operating Systems

Stanford University, Stanford CA

Investigators

Abstract

Operating systems are both huge -- tens of millions of lines of code -- and hugely important -- they manage resources and provide services to the applications that run society. Like all software, operating systems contain bugs. Unfortunately, bugs in such foundational systems can have catastrophic consequences, from large-scale data leaks to complete machine takeovers by malicious agents. The team of researchers develops new tools that can be used to find and eliminate such bugs before a system is deployed, when the bugs can compromise performance, reliability, and security. The project's novelties are foundational techniques, languages, and algorithms that empower software developers to describe buggy patterns that allow automated tools to scale and find bugs in many millions of lines of code. The project's impacts will be in improving the robustness, reliability, and security of real-world operating systems. Existing approaches to bug finding either are precise or scale to large systems but not both. This project reconciles scalability and precision with a key insight: that system-specific extensibility will allow developers to extend core algorithms to check for properties and patterns that are important to their particular systems in a way that scales to large code bases. To this end, the researchers develop new symbolic-execution-based methods that are extensible, precise and scalable, thereby allowing developers to easily customize extensions to focus on likely error patterns while allowing them to swiftly ignore many millions of lines of irrelevant code. The speed, precision and scalability in turn allows developers to directly integrate the project's tools into their software-development cycle to eliminate bugs well before deployment. 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.