HybridHP:一种轻型的内核完整性监控方案及其形式化验证

摘要：

虽然传统的虚拟化监控方法可以在一定程度上保障操作系统安全.然而,虚拟监控器VMM中管理域Domain0的存在以及操作系统级的切换所带来的性能损失是很多具有大型应用的操作系统所不能接受的.注重硬件虚拟化技术的监控能力而摒弃其不必要的虚拟化能力,提出了一个新型的通用的虚拟化监控框架HybridHP,并实现其原型.HybridHP将管理域和虚拟机监控机制两者整合到被监控操作系统的地址空间,具有很好的获取被监控系统操作语义的能力.利用Isabelle/HOL形式化辅助证明工具验证HybridHP的隔离性、安全性和监控能力.最后对HybridHP进行了攻击实验和性能评估,结果显示HybridHP提供了和传统的虚拟化监控方案相同的安全保障,并具有很好的系统性能.

关键词：硬件虚拟化、内核完整性、安全监控、安全攻击、Isabelle形式化验证

所属期刊栏目：35

分类号：TP309(计算技术、计算机技术)

资助基金：国家"八六三"高技术研究发展计划项目基金2007AA01Z409;江苏省科技支撑计划自然科学基金BE2008124;江苏省"六大人才高峰"高层次人才项目2011-DZXX-035

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

页数：共13页

页码：1462-1474