A Secure and Formally Verified Linux KVM Hypervisor
A Secure and Formally Verified Linux KVM Hypervisor
复制标题
DOI：
10.1109/sp40001.2021.00049
复制
发表时间：
2021-05
期刊：
影响因子：
--
通讯作者：
Shih-wei Li;Xupeng Li;Ronghui Gu;Jason Nieh;J. Hui
中科院分区：
文献类型：
--
作者：
Shih-wei Li;Xupeng Li;Ronghui Gu;Jason Nieh;J. Hui
商品管理器被广泛部署以支持多处理器硬件的虚拟机（VM）。以及一组不信任的服务，以便我们可以单独验证核心来证明整个管理程序的安全性属性，以验证多处理器Hypervisor Core，我们介绍了安全性的层次，以模块化证明而无需隐藏信息泄漏在实现的规范中，通过核心实现的所有层来完善了顶层规范，以验证需要动态变化信息流的商品管理功能。使用Microverification，我们使用COQ对Linux KVM管理程序进行了适度的修改。商品多处理器管理程序的证明。
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 security properties of the entire hypervisor by verifying the core alone. To verify the multiprocessor 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.