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

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.