Computer Science ›› 2019, Vol. 46 ›› Issue (3): 170-179.doi: 10.11896/j.issn.1002-137X.2019.03.026

• Information Security • Previous Articles     Next Articles

Study on Formal Verification of Secure Virtual Machine Monitor

CHEN Hao, LUO Lei, LI Yun, CHEN Li-rong   

  1. (School of Computer Science and Engineering,University of Electronic Science and Technology of China,Chengdu 611731,China)
  • Received:2018-01-03 Revised:2018-03-20 Online:2019-03-15 Published:2019-03-22

Abstract: Virtualization equips the security-critical systems with multiple features,including partitioning and separation.As the core component,virtual machine monitor (VMM) serves as a backbone to the secure execution as well as a barrier to isolate the threats and faults of virtual machines.Following the principle of least privilege,this paper presented a method to decouple the VMM into two parts:kernel extension and user processes.Furthermore,a formal method by constructing abstraction layers is used to certify those key components of the VMM kernel extension.Then,the functional correctness property of the VMM are also proved.The experiment results show that the certified prototype achieves comparable efficiency as the mainstream virtualization solution.The decoupled design and formal verification improve the VMM security without imposing obvious performance degradation,and meet the requirement of the application fields.

Key words: Virtualization technology, Virtual machine monitor, Security isolation, Formal verification, Functional correctness

CLC Number: 

  • TP316.2
[1] SMITH J,NAIR R.Virtual machines:versatile platforms forsystems and processes[M].San Francisco,California,USA:Elsevier,2005.
[2] SHU R,WANG P,GORSKI S A,et al.A Study of Security Isolation Techniques[J].ACM Computing Surveys,2016,49(3):1-37.
[3] CHONG S,GUTTMAN J,DATTA A,et al.Report on the NSF Workshop on Formal Methods for Security[R].College Park,MD,USA:National Science Foundation,2016.
[4] SCHMITTNER C,MA Z.Towards a Framework for Alignment Between Automotive Safety and Security Standards[C]∥Computer Safety,Reliability,and Security:SAFECOMP 2015 Workshops.Cham,Netherlands:Springer International Publishing,2015:133-143.
[5] BECKER H,CRESPO J M,GALOWICZ J,et al.CombiningMechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor[C]∥International Symposium on Formal Methods.Limassol,Cyprus:Springer,Cham,2016:69-84.
[6] MATICHUK D,MURRAY T,ANDRONICK J,et al.Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification[C]∥Proceedings of the 37th International Confe-rence on Software Engineering-Volume 1.Piscataway,NJ,USA:IEEE Press,2015:722-732.
[7] WU C,WANG Z,JIANG X.Taming hosted hypervisors with(mostly) deprivileged execution[C]∥Proceedings of the Network and Distributed System Security Symposium (NDSS).San Diego,CA,USA:Internet Society,2013:1-15.
[8] PAN W,ZHANG Y,YU M,et al.Improving Virtualization Security by Splitting Hypervisor into Smaller Components[C]∥Proceedings of the 26th Annual IFIP WG 11.3 Conference on Data and Applications Security and Privacy.Berlin,Heidelberg:Springer-Verlag,2012:298-313.
[9] SANN D,BUTTERFIELD A,HINCHEY M.Separation Ker-nel Verification:The Xtratum Case Study[C]∥Working Conference on Verified Software:Theories,Tools,and Experiments.Vienna,Austria:Springer,Cham,2014:133-149.
[10] PENNEMAN N,KUDINSKAS D,RAWSTHORNE A,et al.Formal virtualization requirements for the ARM architecture[J].Journal of Systems Architecture,2013,59(3):144-154.
[11] BARTHE G,BETARTE G,CAMPO J D,et al.Formally Verified Implementation of an Idealized Model of Virtualization[C]∥19th International Conference on Types for Proofs and Programs (TYPES 2013).Dagstuhl,Germany:Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,2014:45-63.
[12] NEMATI H,GUANCIALE R,DAM M.Trustworthy Virtuali-zation of the ARMv7 Memory Subsystem[C]∥International Conference on Current Trends in Theory and Practice of Informatics.Berlin:Springer,2015:578-589.
[13] BLANCHARD A,KOSMATOV N,LEMERRE M,et al.ACase Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C[C]∥International Workshop on Formal Methods for Industrial Critical Systems.Berlin:Springer,2015:15-30.
[14] BAUMANN C,SCHWARZ O,DAM M.Compositional Verification of Security Properties for Embedded Execution Platforms[C]∥6th International Workshop on Security Proofs for Embedded Systems(PROOFS 2017).Taipei,Taiwan,China,EPiC open access,2017:1-16.
[15] NORDHOLZ J.Design and provability of a statically configurable hypervisor[D].Berlin:Technische Universitt Berlin,2017.
[16] LEINENBACH D,SANTEN T.Verifying the Microsoft Hyper-V Hypervisor with VCC[C]∥Proceedings of the 2Nd World Congress on Formal Methods.Berlin,Heidelberg:Springer-Verlag,2009:806-809.
[17] ALKASSAR E,HILLEBRAND M A,PAUL W J,et al.Automated Verification of a Small Hypervisor[C]∥Proceedings of the Third International Conference on Verified Software:Theories,Tools,Experiments.Berlin,Heidelberg:Springer-Verlag,2010:40-54.
[18] KLEIN G,ANDRONICK J,ELPHINSTONE K,et al.Comprehensive Formal Verification of an OS Microkernel[J].ACM Transactions on Computer Systems,2014,32(1):2:1-2:70.
[19] VASUDEVAN A,CHAKI S,JIA L,et al.Design,Implementation and Verification of an eXtensible and Modular Hypervisor Framework[C]∥2013 IEEE Symposium on Security and Privacy.Berkeley,CA,USA:IEEE Press,2013:430-444.
[20] BOLIGNANO P.Formal models and verification of memorymanagement in a hypervisor[D].Breizh:Université Rennes 1,2017.
[21] BARTHE G,BETARTE G,CAMPO J D,et al.Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization[C]∥2012 IEEE 25th Computer Security Foundations Symposium.Cambridge,MA,USA:IEEE Press,2012:186-197.
[22] BOLIGNANO P,JENSEN T,SILES V.Modeling and Abstraction of Memory Management in a Hypervisor[C]∥International Conference on Fundamental Approaches to Software Engineering.Berlin,Germany:Springer,2016:214-230.
[23] KOVALEV M.TLB virtualization in the context of hypervisor verification[D].Saarbrucken:Saarland University,2013.
[24] MOGOSANU L,CARABAS M,CONDURACHE C,et al.Eva-luating Architecture-Dependent Linux Performance[C]∥2015 20th International Conference on Control Systems and Computer Science.New York:IEEE Press,2015:499-505.
[25] ABDELRAHEM O,BAHAA-ELDIN A M,TAHA A.Virtuali-zation security:A survey[C]∥2016 11th International Conferen-ce on Computer Engineering Systems (ICCES).Cairo,Egypt:IEEE Press,2016:32-40.
[26] FENG X,SHAO Z,GUO Y,et al.Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems[C]∥Proceedings of the 2Nd International Conference on Verified Software:Theories,Tools,Experiments.Berlin,Heidelberg:Springer-Verlag,2008:54-69.
[27] GU R,KOENIG J,RAMANANANDRO T,et al.Deep Specifications and Certified Abstraction Layers[C]∥Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.New York,NY,USA:ACM,2015:595-608.
[28] BERTOT Y,HUET G,CASTRAN P,et al.Interactive Theorem Proving and Program Development:Coq’Art:The Calculus of Inductive Constructions[M].Berlin,Germany:Springer Berlin Heidelberg,2013:1-472.
[29] HEISER G.The Role of Virtualization in Embedded Systems[C]∥Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems.New York,NY,USA:ACM,2008:11-16.
[30] GE Q,YAROM Y,COCK D,et al.A survey of microarchitectural timing attacks and countermeasures on contemporary hardware[J].Journal of Cryptographic Engineering,2018,8(1):1-27.
[31] KIM J H,LEE S H,JIN H W.Supporting Virtualization Stan-dard for Network Devices in RTEMS Real-time Operating System[J].ACM SIGBED Review,2016,13(1):35-40.
[32] KLEIN G.Operating system verification—An overview[J].Sadhana,2009,34(1):27-69.
[33] LEROY X,BLAZY S,KSTNER D,et al.CompCert-A Formally Verified Optimizing Compiler[C]∥ERTS 2016:Embedded Real Time Software and Systems,8th European Congress.Toulouse,France:SEE,2016.
[34] LEROY X,BLAZY S.Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations[J].Journal of Automated Reasoning,2008,41(1):1-31.
[35] STAELIN C.Lmbench:an extensible micro-benchmark suite[J].Software:Practice and Experience,2005,35(11):1079-1105.
[36] KLEINERT B,WEI S,SCHFER F,et al.Adaptive Synchronization Interface for Hardware-Software Co-Simulation Based on SystemC and QEMU[C]∥Proceedings of the 9th EAI International Conference on Simulation Tools and Techniques.ICST,Brussels,Belgium,Belgium:ICST,2016:28-36.
[37] DESHPANDE S M,AINAPURE B.An Intelligent Virtual Machine Monitoring System Using KVM for Reliable And Secure Environment in Cloud[C]∥2016 IEEE International Conference on Advances in Electronics,Communication and Computer Technology (ICAECCT).New York:IEEE Press,2016:314-319.
[38] PU J,SONG Z,TILEVICH E.Understanding the Energy,Performance,and Programming Effort Trade-Offs of Android Persistence Frameworks[C]∥2016 IEEE 24th International Symposium on Modeling,Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS).London,United Kingdom:IEEE Press,2016:433-438.
[1] LI Ling, LI Huang-hua, WANG Sheng-yuan. Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design [J]. Computer Science, 2020, 47(6): 8-15.
[2] FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318.
[3] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[4] TANG Hong-mei and ZHENG Gang. Design and Optimization on Virtual Desktop Infrastructure Based on KVM [J]. Computer Science, 2017, 44(Z6): 560-562.
[5] LI Yan-chun, LI Xiao-juan, GUAN Yong, WANG Rui, ZHANG Jie and WEI Hong-xing. xMAS-based Formal Verification of SpaceWire Credit Logic [J]. Computer Science, 2016, 43(2): 113-117.
[6] YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie. Higher-order Logic Formalization of Function Matrix and its Calculus [J]. Computer Science, 2016, 43(11): 24-29.
[7] CHEN Li-rong, LI Yun and LUO Lei. Research on Formal Verification of Embedded Operating System [J]. Computer Science, 2015, 42(8): 203-214.
[8] LI Qing-bao, ZHANG Ping and ZENG Guang-yu. Integrity Based Security Protection Method for Terminal Computer [J]. Computer Science, 2015, 42(6): 162-166.
[9] LIU Yang,YANG Fei,SHI Gang,YAN Xin,WANG Sheng-yuan and DONG Yuan. Brief Overview of Translation Validation Method in Trusted Compiler Construction [J]. Computer Science, 2014, 41(Z6): 334-338.
[10] ZHOU Kuan-jiu,REN Long-tao,WANG Xiao-long,YONG Jia-wei and HOU Gang. Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix [J]. Computer Science, 2014, 41(8): 42-46.
[11] LI Qian and YU Wen-sheng. Safety Verification for VCCR Subsystem of Space Life Support System [J]. Computer Science, 2014, 41(6): 193-198.
[12] LI Min,LUO Hui-qiong,TANG Chun-ling and WANG Qiang. Research on Formal Verification of Web Interaction Model [J]. Computer Science, 2014, 41(2): 219-221.
[13] HUANG Cong-hui,CHEN Jing,GONG Shui-qing and CHEN Ming-hua. Research of Method for Virtualizing 64-bit Windows Application Binary Interface [J]. Computer Science, 2014, 41(1): 39-42.
[14] HOU Gang,ZHOU Kuan-jiu,YONG Jia-wei,REN Long-tao and WANG Xiao-long. Survey of State Explosion Problem in Model Checking [J]. Computer Science, 2013, 40(Z6): 77-86.
[15] PAN Hai-yu,ZHANG Min and CHEN Yi-xiang. Relationships among Several Types of Kripke Structures Based on Fuzzy Logic [J]. Computer Science, 2013, 40(5): 42-44.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75 .
[2] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[3] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[4] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[5] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99 .
[6] ZHOU Yan-ping and YE Qiao-lin. L1-norm Distance Based Least Squares Twin Support Vector Machine[J]. Computer Science, 2018, 45(4): 100 -105 .
[7] LIU Bo-yi, TANG Xiang-yan and CHENG Jie-ren. Recognition Method for Corn Borer Based on Templates Matching in Muliple Growth Periods[J]. Computer Science, 2018, 45(4): 106 -111 .
[8] GENG Hai-jun, SHI Xin-gang, WANG Zhi-liang, YIN Xia and YIN Shao-ping. Energy-efficient Intra-domain Routing Algorithm Based on Directed Acyclic Graph[J]. Computer Science, 2018, 45(4): 112 -116 .
[9] CUI Qiong, LI Jian-hua, WANG Hong and NAN Ming-li. Resilience Analysis Model of Networked Command Information System Based on Node Repairability[J]. Computer Science, 2018, 45(4): 117 -121 .
[10] WANG Zhen-chao, HOU Huan-huan and LIAN Rui. Path Optimization Scheme for Restraining Degree of Disorder in CMT[J]. Computer Science, 2018, 45(4): 122 -125 .