TC: Medium: Making OS Kernels Crash-Proof by Design and Certification

Yale University, New Haven CT

Investigators

Abstract

Operating System (OS) kernels form the bedrock of all system software---they can have the greatest impact on the resilience, security, and extensibility of today's computing hosts. A single kernel bug can easily wreck the entire system's integrity and protection. The PIs are applying new advances in certified software to the design and development of novel kernel structures that generalize and unify traditional OS abstractions in microkernels, recursive virtual machines, and hypervisors. By replacing the traditional "red line" (between the kernel and user code) with customized safety policies, the PIs show how to support different isolation and kernel extension mechanisms (e.g., type-safe languages, software-fault isolation, or address space protection) in a single framework. The PIs are also building a new framework for certified kernel programming and a set of domain-specific variants of C-like languages. They are applying them to certify different components at different abstraction layers (ranging from scheduler, virtual memory manager, file system, to information flow control), and then linking everything together to build end-to-end certified OS kernels. Certified kernels built under this project will offer safe and application-specific extensibility, provable security properties with information flow control, and accountability and recovery from hardware or application failures. They will help improve the reliability and security of many key components in the world's critical infrastructure, and advance human knowledge on what is possible in building trustworthy systems on top of a reliable core.