摘要
虚拟机监控器(virtual machine monitor,VMM)动态度量是保障虚拟化环境安全的重要手段,但是目前VMM动态度量正确性缺乏理论分析。基于VMM动态度量流程,确立了动态度量正确性目标,明确了定义动态度量应满足的重要属性,从操作语法、语义及推理规则方面扩展安全系统逻辑(logic of secure systems,LS2),据此推导动态度量程序的不变性,验证VMM动态完整性度量应满足的正确性。结论分析表明,应用本文扩展的LS2方法分析得出的动态度量结论与该技术实际应用效果一致,说明扩展的LS2方法有效,可为虚拟化环境安全提供理论参考。
Dynamic measurement for Virtual Machine Monitor （VMM）is a vital means to guarantee virtualized envi-ronments security,but there is currently little theoretical analysis on the correctness of VMM dynamic measurement. Therefore,based on VMM dynamic measurement process,the correctness goal of dynamic measurement is established in this work,which also gave a clear definition of several important properties to be met during dynamic measurement. Meanwhile,Logic of Secure Systems （LS2 ）is extended by the operating syntax,semantics and reasoning rules,where-by reasoning several procedure invariances,and then formally verifying the correctness of VMM dynamic integrity measurement.The analysis shows that model and analysis conclusions drawn from the extended LS2 coincide with prac-tical application effect,and that the extended LS2 is effective to provide security theoretical support for virtualized envi-ronments security.
出处
《山东大学学报（理学版）》
CAS
CSCD
北大核心
2014年第9期1-8,23,共9页
Journal of Shandong University(Natural Science)
基金
国家"九七三"重点基础研究发展计划项目(2014CB340600)
国家自然科学基金重点项目(61332019)
国家自然科学基金资助项目(61173138
61272452)
湖北省重点新产品新工艺研究开发项目(2012BAA03004)
关键词
虚拟机监控器
动态度量
安全系统逻辑
virtual machine monitor
dynamic measurement
logic of secure systems
