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

职业：NgOS：迈向更好的操作系统：快速、安全且可靠

• 批准号: 2239615
• 负责人: Anton Burtsev
• 金额: $ 60.33万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-08-01 至 2028-07-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2239615&HistoricalAwards=false
• 关键词: CAREER; NgOS; Towards; Better; Operating

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.

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