CAREER: NgOS: Towards Better Operating Systems: Fast, Secure, and Reliable

60年前，第一批计算机操作系统被开发为一个相对简单的软件层，旨在提供硬件的多路复用并确保用户的基本隔离。如今，操作系统为从家庭娱乐系统到医疗设备和可扩展云基础设施的几乎每一台消费者和企业设备提供了行业标准的执行环境。我们相信这些系统不仅能在面对数以千计的开发承诺和大规模的重新设计工作时正确运行，而且还能经受住有针对性的安全攻击，并为各种现代应用程序提供高效的执行环境。不幸的是，六十年前做出的设计决策的影响阻碍了现代系统的可靠性、安全性和性能。拟议的研究将探索一个新的操作系统组织--非政府组织，该组织采用新的方法来提高操作系统内核的安全性和可靠性。非政府组织旨在为减轻现代操作系统中的编程错误和安全漏洞造成的巨大经济损害奠定基础。通过改变内核的遗留架构，非政府组织为安全可靠的系统建立了实用的基础，以消除各种软件故障、有针对性的安全攻击、恶意软件僵尸网络和相关活动。这项工作的主要贡献是一种全新的操作系统体系结构，旨在探索低开销隔离、语言安全以及对操作系统内核的安全性、可靠性和性能进行正式验证的好处。非政府组织将利用旨在支持隔离和控制流完整性的新型硬件机制来开发新的隔离机制，以实现操作系统组件的低开销、细粒度隔离。这将允许将微核化的原则推向极端，即实现跨子系统的隔离，这些子系统由于性能原因而历来保持单一。然后，非政府组织将隔离与新的正式核查技术相结合，以实现对内在共享的核心子系统的模块化核查，即提供硬件资源的多路复用。非政府组织利用Rust等零开销安全编程语言的进步，即在没有垃圾收集的情况下实现安全的语言，以使低级系统代码中传统上令人望而却步的高级编程语言技术成为可能。模块化的操作系统组织和实用核查工具的最新进展相结合，利用基于线性类型的语言核查的自动化，使非政府组织的核心得以可扩展核查。最后，对于现代验证范围之外的子系统，非政府组织利用高级编程语言抽象，通过轻量级、基于语言的事务实现从暂时性故障中透明地恢复。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Six decades ago, the first computer operating systems were developed as a relatively simple software layer aimed at providing multiplexing of hardware and ensuring basic isolation of users. Today, operating systems provide an industry-standard execution environment for nearly every consumer and enterprise device ranging from home entertainment systems to medical devices and scalable cloud infrastructure. We trust these systems not only to run correctly when faced with thousands of development commits and massive re-engineering efforts but also to withstand targeted security attacks and provide an efficient execution environment for a broad variety of modern applications. Unfortunately, the impact of design decisions that were made six decades ago hinder the reliability, security, and performance of modern systems. The proposed research will explore a new operating system organization, NgOS, that incorporates novel approaches for improving security and reliability of operating system kernels. NgOS is aimed at providing a foundation for mitigating the vast economic damage that is enabled by programming errors and security vulnerabilities in modern operating systems. By changing the legacy architecture of the kernel, NgOS builds a practical foundation for secure and reliable systems that eliminates many kinds of software faults, targeted security attacks, malware botnets, and related activities. NgOS will be open source, directly benefiting the broader community.The main contribution of this work is a clean-slate operating system architecture designed to explore the benefits of low-overhead isolation, language safety, and formal verification for security, reliability, and performance of the operating system kernel. NgOS will leverage novel hardware mechanisms aimed at support for isolation and control flow integrity to develop new isolation mechanisms that enable low-overhead, fine-grained isolation of operating system components. This will allow pushing the principles of microkernelization to the extreme, i.e., enabling isolation across subsystems that historically remained monolithic due to performance reasons. NgOS then combines isolation with novel formal verification techniques to enable modular verification of the kernel subsystems that are inherently shared, i.e., provide multiplexing of hardware resources. NgOS leverages advances in zero-overhead safe programming languages like Rust, i.e., languages that implement safety without garbage collection, to enable traditionally prohibitive high-level programming language techniques in low-level systems code. A combination of modular operating system organization and recent advances in practical verification tools that leverage automation of verification for languages based on linear types enable scalable verification of NgOS's kernel. Finally, for subsystems that are beyond the reach of modern verification, NgOS leverages high-level programming language abstractions to enable transparent recovery from transient faults through lightweight, language-based transactions.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.