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.

六十年前，第一个计算机操作系统是作为一个相对简单的软件层开发的，旨在提供硬件的多路复用并确保用户的基本隔离。如今，操作系统为几乎每个消费者和企业设备提供了一个行业标准的执行环境，从家庭娱乐系统到医疗设备以及可扩展的云基础架构。我们相信这些系统不仅在面对成千上万的开发人员和大规模的重新设计工作时正确运行，还可以承受针对性的安全攻击，并为各种现代应用提供有效的执行环境。不幸的是，六十年前做出的设计决策的影响阻碍了现代系统的可靠性，安全性和性能。 拟议的研究将探索一个新的操作系统组织非政府组织，该组织结合了提高操作系统内核安全性和可靠性的新颖方法。非政府组织旨在为减轻现代操作系统中的错误和安全漏洞造成的巨大经济损害提供基础。通过更改内核的遗产架构，非政府组织为安全可靠的系统建立了实用的基础，以消除许多类型的软件故障，有针对性的安全攻击，恶意软件僵尸网络和相关活动。非政府组织将是开源的，直接使更广泛的社区受益。这项工作的主要贡献是一种干净的操作系统体系结构，旨在探索低空隔离，语言安全性以及对安全系统内核的安全性，可靠性和性能的正式验证的好处。非政府组织将利用旨在支持隔离和控制流程的新型硬件机制，以开发新的隔离机制，从而使操作系统组件的低空，细粒度隔离。这将允许将微动化的原理推向极端，即，由于绩效原因，在历史上保持整体岩石的跨系统隔离。然后，非政府组织将隔离与新颖的形式验证技术相结合，以实现对内在共享的内核子系统的模块化验证，即提供硬件资源的多重多路复用。非政府组织利用零跨越的安全编程语言（例如Rust）的进步，即无需垃圾收集的语言，以在低级系统代码中启用传统上令人难以置信的高级编程语言技术。模块化操作系统组织和实际验证工具的最新进展的结合，这些工具利用基于线性类型的语言验证自动化，可实现NGOS内核的可扩展验证。最后，对于超越现代验证的子系统的子系统，非政府组织利用高级编程语言抽象来使通过基于语言的轻量，基于语言的交易从短暂的故障恢复透明。该奖项反映了NSF的法定任务，并通过该基金会的知识绩效和广泛的影响来评估NSF的法定任务，并被认为是值得的。