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.