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

作     者：陈昊 罗蕾 李允 陈丽蓉 CHEN Hao;LUO Lei;LI Yun;CHEN Li-rong

作者机构：电子科技大学计算机科学与工程学院成都611731 

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

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2019年第46卷第3期

页      码：170-179页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.11896/j.issn.1002-137X.2019.03.026

馆 藏 号：203607427...