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的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。