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

操作系统（OS）内核构成了所有系统软件的基础-它们对当今计算主机的弹性、安全性和可扩展性有着最大的影响。 一个单一的内核错误可以很容易地破坏整个系统的完整性和保护。PI正在将认证软件的新进展应用于新内核结构的设计和开发，这些内核结构概括和统一了微内核、递归虚拟机和虚拟机管理程序中的传统操作系统抽象。 通过用定制的安全策略替换传统的“红线”（内核和用户代码之间），PI展示了如何支持不同的隔离和内核扩展机制（例如，类型安全语言、软件故障隔离或地址空间保护）。PI还为认证内核编程和一组特定于领域的类C语言变体构建了一个新的框架。他们应用它们来认证不同抽象层的不同组件（从调度程序、虚拟内存管理器、文件系统到信息流控制），然后将所有组件连接在一起，构建端到端认证的操作系统内核。在该项目下构建的认证内核将提供安全和特定于应用程序的可扩展性，可证明的安全属性和信息流控制，以及硬件或应用程序故障的问责制和恢复。它们将有助于提高世界关键基础设施中许多关键组件的可靠性和安全性，并推动人类了解在可靠的核心之上构建值得信赖的系统的可能性。

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.