基于扩展LS2的VMM动态度量形式化分析
作为云计算的关键技术，虚拟化在安全隔离方面具有极大优势。然而，当前虚拟化平台自身面临着前所未有的安全挑战和威胁。处于核心层的虚拟机监控器(Virtual Machine Monitor, VMM)完整性保护问题函需研究解决。可信度量是确保VMM完整性的重要方法之一。但是，目前采用的静态可信根度量(Static Root of Trust for Measurement, SRTM)技术只是在平台启动时才进行一次完整性度量，难以满足VMM多次完整性度量需求，并已证明不安全。这种情况下，Intel和AMD推出的动态可信度量技术应运而生，已经成为研究焦点之一。动态完整性度量的关键是如何保证度量过程的正确性和唯一性。但是目前缺乏针对VMM动态完整性度量正确性的形式化分析。动态度量技术领先与理论，缺乏理论层次的深入研究分析，难以从虚拟机监控器( Virtual Machine Monitor.VMM)动态完整性度量是目前保障虚拟化环境安全的重要的手段,但是在针对VMM动态度量正确性、安全性以及稳定性等安全指标方面缺乏理论分析.为此,本文基于VMM动态完度量流程,确立动态度量正确性目标,明确定义动态度量应满足的重要属性,从操作语法、语义及推理规则方面扩展了安全系统逻辑（Logic of Secure Svstems,LS2),据此推导动态度量程序的不变性,验证VMM动态完整性度量应满足的正确性与唯一性.结果分析表明,应用本文扩展的LS2方法分析得出的动态度量结论与该技术实际应用效果一致,说明扩展的LS2方法有效,可为虚拟化环境安全提供理论参考.
云计算 虚拟机 监控器 动态度量 安全性能
国内会议
湖北恩施
中文
1-7
2014-09-13（万方平台首次上网日期，不代表论文的发表时间）