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

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

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.