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

Study on Formal Verification of Secure Virtual Machine Monitor

作　　者：陈昊[1] 罗蕾[1] 李允[1] 陈丽蓉[1] CHEN Hao;LUO Lei;LI Yun;CHEN Li-rong(School of Computer Science and Engineering,University of Electronic Science and Technology of China,Chengdu 611731,China)

机构地区：[1]电子科技大学计算机科学与工程学院,成都611731

出　　处：《计算机科学》2019年第3期170-179,共10页Computer Science

基　　金："十二五"核高基重大专项:汽车电子基础软件平台研发及应用产业化项目(2009ZX01038-002-003)资助

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

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

分 类 号：TP316.2[自动化与计算机技术—计算机软件与理论]