Logo

Header

Header

Ronghui Gu

Columbia University

A Secure and Formally Verified Linux KVM Hypervisor

Commodity hypervisors are widely deployed to support virtual machines (VMs) on multiprocessor hardware. Their growing complexity poses a security risk. To enable formal verification over such a large codebase, we introduce microverification, a new approach that decomposes a commodity hypervisor into a small core and a set of untrusted services so that we can prove the security properties of the entire hypervisor by verifying the core alone. To verify the multi-processor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we introduce data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data while retaining KVM’s functionality and performance. Our work is the first machine-checked security proof for a commodity multiprocessor hypervisor.

Photo
Ronghui Gu is the inaugural Tang Family Assistant Professor of Computer Science at Columbia University and a Cybersecurity Affiliated member of Columbia's Data Science Institute. He is the primary designer and developer of CertiKOS, the first verified concurrent OS kernel, and SeKVM, the first verified commodity hypervisor--major milestones toward building safe and secure systems software. Gu also co-founded CertiK, a blockchain security startup that has collectively served more than 300 enterprise clients and secured more than $8 billion worth of assets in cryptocurrency. For his work in systems verification, Gu received: an SOSP Best Paper Award, a CACM Research Highlight, and a Yale Distinguished Dissertation Award. He obtained his Ph.D. degree from Yale University in 2016 and bachelor's degree from Tsinghua University in 2011.
 
Homepage: https://www.cs.columbia.edu/~rgu/