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

商用操作系统（OS）内核构成了当今计算基础设施的支柱。尽管它们很重要，但这些商品操作系统内核是复杂的，高度并发的，并且所需要的只是代码中的一个薄弱环节，使系统容易受到黑客的攻击。其中许多漏洞几乎不可能通过传统测试检测到。即使一个商业操作系统内核可以被写得99%正确，黑客仍然可以潜入那个特定的1%设置，系统将不会像预期的那样运行。该项目正在设计，实现和评估微验证，一种新的方法来验证大型，商品，多处理器操作系统内核在任何情况下都是安全的，而无需证明系统的每个部分的正确性。这种方法正被用于Linux内核，用于当今的许多计算基础设施。该项目为构建可信赖的系统软件和使未来的计算基础设施更加安全的未来创新奠定了基础。微验证将现有的商品操作系统内核改造为一个小型的可信核心和一组更大的不可信服务，这样就可以通过单独推理核心来验证整个操作系统内核的信息流安全性。该项目正在开发安全保护层，通过将核心分解为可组合的分层规范的层次结构，使验证易于处理。然后，可以递增地验证核心实现以细化其高级分层规范，使得可以在核心的顶层规范上证明安全保证，跨层保留安全保证，并且对改进的OS内核的整个实现保持安全保证。改造和验证正在Linux内核上进行，其验证以前被认为是棘手的，表明微验证技术能够验证现有的大规模商品操作系统内核。该奖项反映了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.