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

HybridHP: A Verified Lightweight Approach to Provide LifetimeKernel Integrity Surveillance

作　　者：钱振江[1,2,3] 刘苇[1,2] 黄皓[1,2] 

机构地区：[1]南京大学软件新技术国家重点实验室,南京210046 [2]南京大学计算机科学与技术系,南京210046 [3]常熟理工学院计算机科学与工程学院,江苏常熟215500

出　　处：《计算机学报》2012年第7期1462-1474,共13页Chinese Journal of Computers

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

摘　　要：虽然传统的虚拟化监控方法可以在一定程度上保障操作系统安全.然而,虚拟监控器VMM中管理域Domain0的存在以及操作系统级的切换所带来的性能损失是很多具有大型应用的操作系统所不能接受的.注重硬件虚拟化技术的监控能力而摒弃其不必要的虚拟化能力,提出了一个新型的通用的虚拟化监控框架HybridHP,并实现其原型.HybridHP将管理域和虚拟机监控机制两者整合到被监控操作系统的地址空间,具有很好的获取被监控系统操作语义的能力.利用Isabelle/HOL形式化辅助证明工具验证HybridHP的隔离性、安全性和监控能力.最后对HybridHP进行了攻击实验和性能评估,结果显示HybridHP提供了和传统的虚拟化监控方案相同的安全保障,并具有很好的系统性能.Although traditional virtualization monitoring can help ensure security,the existence of management domain（such as Domain0） and performance loss caused by OS-level switches make these approaches unsuitable for many OSs with large applications.In this paper,focusing on monitoring capability of the hardware virtualization technology without the unnecessary virtualization functionality,we propose HybridHP,a new general-purpose framework of virtualization monitoring,and implement the prototype.HybridHP merges the management domain and virtual machine monitoring functionality into the monitored system,and has strong ability to obtain operational semantics of the monitored system.We use the formal theorem prover Isabelle/HOL to verify isolation,security and monitoring capability of HybridHP.With the systemic experiments and performance evaluation for HybridHP,we show that HybridHP provides at least the same security guarantees as what can be achieved by the traditional virtualization monitoring approaches,and has well system performance.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]