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

操作系统既庞大——有数千万行代码——又非常重要——它们管理资源并为运行社会的应用程序提供服务。像所有的软件一样，操作系统也有缺陷。不幸的是，这些基础系统中的漏洞可能会带来灾难性的后果，从大规模数据泄露到恶意代理完全接管机器。研究人员团队开发了新的工具，可用于在部署系统之前发现并消除此类错误，因为这些错误可能会损害性能、可靠性和安全性。该项目的新颖之处是基础技术、语言和算法，这些技术、语言和算法使软件开发人员能够描述错误模式，这些模式允许自动化工具在数百万行代码中扩展和发现错误。该项目的影响将是提高现实世界操作系统的健壮性、可靠性和安全性。现有的漏洞查找方法要么是精确的，要么是适用于大型系统的，但不能两者兼得。这个项目将可伸缩性和精度与一个关键的洞察力相协调：系统特定的可扩展性将允许开发人员扩展核心算法，以一种扩展到大型代码库的方式来检查对其特定系统重要的属性和模式。为此，研究人员开发了新的基于符号执行的方法，这些方法是可扩展的、精确的和可伸缩的，从而允许开发人员轻松地定制扩展，专注于可能的错误模式，同时允许他们迅速忽略数百万行不相关的代码。速度、精度和可伸缩性反过来使开发人员能够直接将项目的工具集成到他们的软件开发周期中，从而在部署之前消除错误。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.