https://scholars.lib.ntu.edu.tw/handle/123456789/607457
標題: | A secure and formally verified linux KVM hypervisor | 作者: | Shih-Wei LI Li X Gu R Nieh J Zhuang Hui J. |
關鍵字: | Linux;Multiprocessing systems;Specifications;Theorem proving;Hiding informations;Hypervisors;Information flows;Multi-processor hardware;New approaches;Security proofs;Security properties;Security risks;Virtual machine | 公開日期: | 2021 | 卷: | 2021-May | 起(迄)頁: | 1782-1799 | 來源出版物: | Proceedings - IEEE Symposium on Security and Privacy | 摘要: | 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. ? 2021 IEEE. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85114457811&doi=10.1109%2fSP40001.2021.00049&partnerID=40&md5=38e0bf8b829aec3bc3e621990bc7b277 https://scholars.lib.ntu.edu.tw/handle/123456789/607457 |
ISSN: | 10816011 | DOI: | 10.1109/SP40001.2021.00049 |
顯示於: | 資訊工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。