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.
Chapter PDF
Similar content being viewed by others
References
Marshall, D.: Microsoft Hyper-V gets its first security patch. Infoworld (February 2010), http://www.infoworld.com/d/virtualization/microsoft-hyper-v-gets-its-first-security-patch-106
Vulnerability report: MS11-047 – Vulnerability in Microsoft Hyper-V could cause denial of service (June 2011), http://www.sophos.com/support/knowledgebase/article/113734.html
Clarke, E., Grumberg, O., Long, D.: Model Checking. MIT Press (1999)
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V Hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 806–809. Springer, Heidelberg (2009)
Freitas, L., McDermott, J.: Formal methods for security in the Xenon hypervisor. International Journal on Software Tools for Technology Transfer 13(5), 463–489 (2011)
Webster, M., Malcolm, G.: Detection of metamorphic and virtualization-based malware using algebraic specifi cation. In: EICAR 2008 (2008)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2004)
Ball, T., Levin, V., Rajamani, S.K.: A Decade of Software Model Checking with SLAM. Communications of the ACM 54(7), 68–76 (2011)
Denning, D.: lattice model of secure information flow. Communications of the ACM 19(5), 236–243 (1976)
Shen, J., Qing, S.: A Dynamic Information Flow Model of Secure Systems. In: CCS, pp. 341–343 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
She, Y., Li, H., Zhu, H. (2013). UVHM: Model Checking Based Formal Analysis Scheme for Hypervisors. In: Mustofa, K., Neuhold, E.J., Tjoa, A.M., Weippl, E., You, I. (eds) Information and Communication Technology. ICT-EurAsia 2013. Lecture Notes in Computer Science, vol 7804. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36818-9_31
Download citation
DOI: https://doi.org/10.1007/978-3-642-36818-9_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36817-2
Online ISBN: 978-3-642-36818-9
eBook Packages: Computer ScienceComputer Science (R0)