SaTC: CORE: Medium: Microverification of Information-Flow Security for the Linux Operating System Kernel

商用操作系统(OS)内核构成了当今计算基础设施的主干。尽管它们很重要，但这些商用操作系统内核是复杂的、高度并发的，所有需要做的就是代码中的一个薄弱环节--让系统容易受到黑客的攻击。其中许多漏洞几乎不可能通过传统测试检测出来。即使一个商用的操作系统内核可以写出99%的正确率，黑客仍然可以潜入到那个特定的1%的设置中，在那里系统将不会像预期的那样运行。这个项目正在设计、实现和评估微验证，这是一种新的方法，可以验证一个大型的、商用的、多处理器的操作系统内核在任何情况下都是安全的，而不需要证明系统的每个部分的正确性。这种方法正在与Linux内核一起使用，该内核在当今的许多计算基础设施中使用。该项目为未来在构建可信系统软件和使未来的计算基础设施更加安全方面的创新奠定了基础。微观验证将现有的商用操作系统内核改造成一个小的可信内核和更大的一组不可信服务，从而可以仅通过对内核的推理来验证整个操作系统内核的信息流安全。该项目正在开发安全保护层，通过将核心分解为可组合的、分层的规范层次结构，使验证变得容易处理。然后，可以递增地验证核心实现以细化其高级分层规范，使得安全保证可以在核心的顶层规范上得到证明，跨层保留，并适用于改进后的OS内核的整个实现。正在对Linux内核进行改造和验证，其验证之前被认为是棘手的，表明微验证技术能够验证现有的大规模商用OS内核。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Commodity operating system (OS) kernels form the backbone of today's computing infrastructure. Despite their importance, these commodity OS kernels are complicated, highly concurrent, and all it takes is a single weak link in the code—one to leave a system vulnerable to hackers. Many of these vulnerabilities are virtually impossible to detect via traditional testing. Even if a commodity OS kernel can be written 99% correctly, a hacker can still sneak into that particular 1% set-up where the system will not behave as expected. This project is designing, implementing, and evaluating microverification, a new approach to verify that a large, commodity, multiprocessor OS kernel is secure under all circumstances without the need to prove the correctness of every part of the system. This approach is being used with the Linux kernel, used in much of today’s computing infrastructure. The project provides a foundation for future innovations in building trustworthy system software and making tomorrow’s computing infrastructure more secure.Microverification retrofits an existing commodity OS kernel into a small, trusted core and a larger set of untrusted services, such that it is possible to verify the information-flow security of the entire OS kernel by reasoning about the core alone. This project is developing security-preserving layers to make verification tractable by decomposing the core into a hierarchy of composable, layered specifications. The core implementation can then be incrementally verified to refine its high-level layered specification, such that security guarantees can be proven over the core's top layer specification, preserved across layers, and hold for the entire implementation of the retrofitted OS kernel. Retrofitting and verification are being done on the Linux Kernel, whose verification was previously considered intractable, demonstrating that microverification techniques are capable of verifying existing large-scale commodity OS kernels.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.