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

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

HybridHP:A Verified Lightweight Approach to Provide Lifetime Kernel Integrity Surveillance

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.