FMitF: Collaborative Research: RedLeaf: Verified Operating Systems in Rust

FMITF：协作研究：RedLeaf：经过验证的 Rust 操作系统

• 批准号: 2313411
• 负责人: Anton Burtsev
• 金额: $ 35万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-02-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2313411&HistoricalAwards=false
• 关键词: FMitF; Collaborative; Research; RedLeaf; Verified

An operating system kernel provides a foundation for isolation and security in every computer system used today. Operating system kernels are trusted to provide the first line of defense for numerous mission critical systems in the face of targeted security attacks. Unfortunately, despite decades of evolution modern operating systems are faulty and vulnerable. Inheriting their core engineering technology from the first time-sharing machines, modern operating system kernels are still developed with a legacy software engineering techniques---a combination of an unsafe programming language, rudimentary concurrency primitives, and virtually no testing or verification tools. Today these systems are faulty and vulnerable. Lacking verification support, industry standard kernels make nearly every computer system on the planet vulnerable. This project will develop RedLeaf, a new operating system, and associated formal verification tools for implementing provably secure and reliable systems in the Rust programming language. RedLeaf brings together state-of-the-art results from verification, programming-language, and systems research communities in order to enable unprecedented security and reliability guarantees in low-level systems software. To achieve complete verification of the entire software stack, i.e., operating system and applications, the RedLeaf team will develop a set of new tools, a collection of techniques and engineering disciplines, and a methodology focused on rapid development of verified systems software. The RedLeaf OS will run on an embedded CPU of a medical sensor, implement a network function virtualization framework aimed at line-rate network processing, and provide a general platform for a broad range of verifiably secure systems. The operating system and associated tools will be open source, directly benefiting the broader community.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.

操作系统内核为当今使用的每个计算机系统的隔离和安全提供了基础。操作系统内核被认为可以为众多关键任务系统提供第一道防线，以应对有针对性的安全攻击。不幸的是，尽管经过了数十年的发展，现代操作系统仍然存在缺陷且脆弱。现代操作系统内核继承了第一代分时机的核心工程技术，仍然采用传统的软件工程技术开发——结合了不安全的编程语言、基本的并发原语以及几乎没有测试或验证工具。如今，这些系统存在缺陷且容易受到攻击。由于缺乏验证支持，行业标准内核使得地球上几乎每个计算机系统都容易受到攻击。该项目将开发 RedLeaf（一种新操作系统）以及相关的形式验证工具，用于使用 Rust 编程语言实现可证明安全可靠的系统。 RedLeaf 汇集了验证、编程语言和系统研究社区的最先进成果，以便在低级系统软件中实现前所未有的安全性和可靠性保证。为了实现整个软件堆栈（即操作系统和应用程序）的完整验证，RedLeaf团队将开发一套新工具、一系列技术和工程学科以及专注于快速开发经过验证的系统软件的方法。 RedLeaf操作系统将在医疗传感器的嵌入式CPU上运行，实现旨在线速网络处理的网络功能虚拟化框架，并为广泛的可验证安全系统提供通用平台。该操作系统和相关工具将是开源的，直接使更广泛的社区受益。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Extending Rust with Support for Zero Copy Communication

通过支持零复制通信来扩展 Rust

• 发表时间: 2023-10
• 期刊: Workshop on Programming Languages and Operating Systems
• 作者: Lafrance, Arthur;Detweiler, David;Li, Zhaofeng;Chen, Xiangdong;Narayanan, Vikram;Burtsev, Anton
• 通讯作者: Burtsev, Anton