FMitF: Track I: A Secure and Verifiable Commodity Hypervisor

Hypervisors are widely deployed by cloud- computing providers to support virtual machines (VMs), but their growing complexity poses a security risk as large codebases contain many vulnerabilities. A compromised hypervisor risks the data and privacy of all its VMs -- an undesirable outcome for both cloud providers and users. In today's data-driven world, data confidentiality and integrity are of crucial importance. This project will design, implement, verify, and evaluate a fundamentally new approach to hypervisor design that provides a small, verified trusted computing base (TCB) for commodity hypervisors to protect the confidentiality and integrity of VMs running in the cloud. The project's novelties are a new hypervisor architecture and formal-verification framework. The project's impacts are providing a foundation for future innovations in the verification of systems software, especially for cloud-computing infrastructure, and verifying open-source virtualization technologies in Linux to drive research innovation in a way that can be adopted in commercial systems.

This project designs a novel hypervisor architecture that partitions the hypervisor into a trusted core that performs basic virtualization, and an untrusted host that performs other hypervisor functionality and can be integrated with a host operating system. The investigators examine features of traditional hypervisors and identify only secure boot and basic CPU and memory virtualization as necessary for the core, resulting in a significantly simpler and verifiable hypervisor core. This project adopts a novel formal-verification framework named certified abstraction layers (CAL) to reason about the correctness (that is, the implementation meets its specification) and security (that is, the specification guarantees VM confidentiality and integrity) of the hypervisor core with an untrusted host. This project retrofits and verifies the Linux Kernel Virtual Machine (KVM) hypervisor, demonstrating the ability of these verification techniques to work in practice with commodity hypervisor software.

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.