Skip to Main content Skip to Navigation
New interface
Conference papers

UVHM: Model Checking Based Formal Analysis Scheme for Hypervisors

Abstract : Hypervisors act a central role in virtualization for cloud computing. However, current security solutions, such as installing IDS model on hypervisors to detect known and unknown attacks, can not be applied well to the virtualized environments. Whats more, people have not raised enough concern about vulnerabilities of hypervisors themselves. Existing works mainly focusing on hypervisors’ code analysis can only verify the correctness, rather than security, or only be suitable for open-source hypervisors. In this paper, we design a binary analysis tool using formal methods to discover vulnerabilities of hypervisors. In the scheme, Z notation, VDM, B, Object-Z or CSP formalism can be utilized as suitable modeling and specification languages. Our proposal sequently follows the process of disassembly, modeling, specification, and verification. Finally, the effectiveness of the method is demonstrated by detecting the vulnerability of Xen-3.3.0 in which a bug is added.
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, March 1, 2017 - 11:04:58 AM
Last modification on : Wednesday, December 15, 2021 - 12:42:02 PM
Long-term archiving on: : Tuesday, May 30, 2017 - 2:29:46 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Yuchao She, Hui Li, Hui Zhu. UVHM: Model Checking Based Formal Analysis Scheme for Hypervisors. 1st International Conference on Information and Communication Technology (ICT-EurAsia), Mar 2013, Yogyakarta, Indonesia. pp.300-305, ⟨10.1007/978-3-642-36818-9_31⟩. ⟨hal-01480185⟩



Record views


Files downloads