CAJ | 학술논문

虚拟机监控器（virtual machine monitor，VMM）动态度量是保障虚拟化环境安全的重要手段，但是目前VMM动态度量正确性缺乏理论分析。基于VMM动态度量流程，确立了动态度量正确性目标，明确了定义动态度量应满足的重要属性，从操作语法、语义及推理规则方面扩展安全系统逻辑（logic of secure systems，LS2），据此推导动态度量程序的不变性，验证VMM动态完整性度量应满足的正确性。结论分析表明，应用本文扩展的LS2方法分析得出的动态度量结论与该技术实际应用效果一致，说明扩展的LS2方法有效，可为虚拟化环境安全提供理论参考。
허의궤감공기（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.