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

摘要：

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

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

所属期刊栏目：46

分类号：TP316.2(计算技术、计算机技术)

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

在线出版日期：2019-05-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：170-179