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

FMITF：协作研究：第一轨：查找并消除操作系统中的错误

• 批准号: 1918573
• 负责人: Deian Stefan
• 金额: $ 50万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-01 至 2023-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918573&HistoricalAwards=false
• 关键词: FMitF; Collaborative; Research; Track; Finding

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.

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

项目成果

Flux: Liquid Types for Rust

助焊剂：用于防锈的液体类型

• DOI: 10.1145/3591283
• 发表时间: 2023-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Lehmann, Nico;Geller, Adam T.;Vazou, Niki;Jhala, Ranjit
• 通讯作者: Jhala, Ranjit

Доверя́й, но проверя́й: SFI safety for native-compiled Wasm

ÐÐ⁄веÑÑÌÐ1, нÐ⁄ п

• DOI: 10.14722/ndss.2021.24078
• 发表时间: 2021-02
• 期刊: Network and Distributed Systems Security (NDSS
• 作者: Johnson, Evan;Thien, David;Alhessi, Yousef;Narayan, Shravan;Brown, Fraser;Lerner, Sorin;McMullen, Tyler;Savage, Stefan;Stefan, Deian
• 通讯作者: Stefan, Deian

Swivel: Hardening WebAssembly against Spectre

Swivel：针对 Spectre 强化 WebAssembly

• 发表时间: 2021-03
• 期刊: USENIX Security Symposium.
• 作者: Narayan, Shravan;Disselkoen, Craig;Moghimi, Daniel;Cauligi, Sunjay;Johnson, Evan;Gang, Zhao;Vahldiek;Sahita, Ravi;Shacham, Hovav;Tullsen, Dean;et al
• 通讯作者: et al

Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code

Sys：用于在良好（浏览器）代码中查找良好错误的静态/符号工具

• DOI: 10.1145/3411496.3421226
• 发表时间: 2024-09-14
• 期刊: Proceedings of the 7th ACM Workshop on Moving Target Defense
• 作者: Fraser Brown;D. Stefan;D. Engler
• 通讯作者: D. Engler

Solver-Aided Constant-Time Hardware Verification

求解器辅助的恒定时间硬件验证

• DOI: 10.1145/3460120.3484810
• 发表时间: 2021-11-12
• 期刊: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
• 作者: K. V. Gleissenthall;Rami Gökhan Kici;D. Stefan;Ranjit Jhala
• 通讯作者: Ranjit Jhala