安全虚拟机监视器的形式化验证研究

doi:10.11896/j.issn.1002-137X.2019.03.026

摘要/Abstract

摘要： 虚拟化技术为安全关键系统提供了分区隔离等重要特性,虚拟机监视器(Virtual Machine Monitor,VMM)作为其核心组件,对客户系统的安全运行及虚拟机间威胁和故障的屏蔽起着决定性作用。文中从最小特权原则出发,将VMM的设计按是否与安全直接相关划分为内核扩展与用户进程,并采用分层精化的方法对内核扩展中的各关键模块展开了形式化建模与验证,继而以此为基础,证明了虚拟机实现的功能正确性。实验评估表明,原型系统的综合性能负载与主流虚拟化方案接近,安全划分的设计方法与形式化验证在提升VMM安全性的同时,并未对其产生明显负载,可较好地满足应用领域的需求。

关键词: 安全隔离, 功能正确性, 形式化验证, 虚拟化技术, 虚拟机监视器

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: Formal verification, Functional correctness, Security isolation, Virtual machine monitor, Virtualization technology

中图分类号:

TP316.2

陈昊,罗蕾,李允,陈丽蓉. 安全虚拟机监视器的形式化验证研究[J]. 计算机科学, 2019, 46(3): 170-179. https://doi.org/10.11896/j.issn.1002-137X.2019.03.026

CHEN Hao, LUO Lei, LI Yun, CHEN Li-rong. Study on Formal Verification of Secure Virtual Machine Monitor[J]. Computer Science, 2019, 46(3): 170-179. https://doi.org/10.11896/j.issn.1002-137X.2019.03.026

参考文献

[1]SMITH J,NAIR R.Virtual machines:versatile platforms for
systems 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.Combining
Mechanized 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.A
Case 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 memory
management 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.

相关文章 15

[1]	蹇奇芮, 陈泽茂, 武晓康. 面向无人机通信的认证和密钥协商协议 Authentication and Key Agreement Protocol for UAV Communication 计算机科学, 2022, 49(8): 306-313. https://doi.org/10.11896/jsjkx.220200098
[2]	杨萍, 王生原. CompCert编译器目标代码生成机制分析 Analysis of Target Code Generation Mechanism of CompCert Compiler 计算机科学, 2020, 47(9): 17-23. https://doi.org/10.11896/jsjkx.200400018
[3]	李凌, 李璜华, 王生原. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design 计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173
[4]	范永乾, 陈钢, 崔敏. 基于COQ的有限域GF(2ⁿ)的形式化研究 Formalization of Finite Field GF(2ⁿ) Based on COQ 计算机科学, 2020, 47(12): 311-318. https://doi.org/10.11896/jsjkx.190900197
[5]	马振威,陈钢. 基于Coq记录的矩阵形式化方法 Matrix Formalization Based on Coq Record 计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022
[6]	唐红梅,郑刚. 基于KVM的虚拟桌面基础架构设计与优化 Design and Optimization on Virtual Desktop Infrastructure Based on KVM 计算机科学, 2017, 44(Z6): 560-562. https://doi.org/10.11896/j.issn.1002-137X.2017.6A.125
[7]	李艳春,李晓娟,关永,王瑞,张杰,魏洪兴. 基于xMAS模型的SpaceWire信誉逻辑的形式化验证 xMAS-based Formal Verification of SpaceWire Credit Logic 计算机科学, 2016, 43(2): 113-117. https://doi.org/10.11896/j.issn.1002-137X.2016.02.026
[8]	杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰. 函数矩阵及其微积分的高阶逻辑形式化 Higher-order Logic Formalization of Function Matrix and its Calculus 计算机科学, 2016, 43(11): 24-29. https://doi.org/10.11896/j.issn.1002-137X.2016.11.005
[9]	陈丽蓉,李允,罗蕾. 嵌入式操作系统的形式化验证研究 Research on Formal Verification of Embedded Operating System 计算机科学, 2015, 42(8): 203-214.
[10]	肖芳雄,许波,夏国恩,李国祥,闵华清. 面向组合式软件功能正确性和非功能满足性的统一建模方法 Unified Modeling Method of Functional and Non-functional Aspects for Composite Software 计算机科学, 2015, 42(12): 162-166.
[11]	刘洋,杨斐,石刚,闫鑫,王生原,董渊. 可信编译器构造的翻译确认方法简述 Brief Overview of Translation Validation Method in Trusted Compiler Construction 计算机科学, 2014, 41(Z6): 334-338.
[12]	周宽久,任龙涛,王小龙,勇嘉伟,侯刚. 基于层次化时间STM软件设计的形式化验证 Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix 计算机科学, 2014, 41(8): 42-46. https://doi.org/10.11896/j.issn.1002-137X.2014.08.008
[13]	李倩,郁文生. 空间生命支持系统中VCCR子系统的安全性验证 Safety Verification for VCCR Subsystem of Space Life Support System 计算机科学, 2014, 41(6): 193-198. https://doi.org/10.11896/j.issn.1002-137X.2014.06.038
[14]	李敏,罗惠琼,唐春玲,王强. Web交互模型的形式化验证研究 Research on Formal Verification of Web Interaction Model 计算机科学, 2014, 41(2): 219-221.
[15]	黄聪会,陈靖,龚水清,陈明华. 64位Windows ABI虚拟化方法研究 Research of Method for Virtualizing 64-bit Windows Application Binary Interface 计算机科学, 2014, 41(1): 39-42.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed