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 OS将在医疗传感器的嵌入式CPU上运行，实现旨在旨在线路速率网络处理的网络功能虚拟化框架，并为广泛的可靠安全系统提供一般平台。操作系统和相关工具将是开源的，直接使更广泛的社区受益。该奖项反映了NSF的法定任务，并使用基金会的知识分子优点和更广泛的影响审查标准，被认为值得通过评估来获得支持。

项目成果

Extending Rust with Support for Zero Copy Communication

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

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