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

TC：中：通过设计和认证使操作系统内核防崩溃

基本信息

批准号：
1065451
负责人：
Zhong Shao
金额：
$ 111.63万
依托单位：
Yale University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2011
资助国家：
美国
起止时间：
2011-08-01 至 2016-07-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1065451&HistoricalAwards=false
关键词：
TC Medium Making OS Kernels

项目摘要

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.

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