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

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

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.