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

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.