您的位置：山东大学 -> 科技期刊社 -> 《山东大学学报（理学版）》

山东大学学报（理学版） ›› 2014, Vol. 49 ›› Issue (09): 1-8.doi: 10.6040/j.issn.1671-9352.2.2014.408

• 论文 •    下一篇

基于扩展LS2的VMM动态度量形式化分析

纪祥敏1,2,3, 赵波1,3, 向騻1,3, 夏忠林1,3   

  1. 1. 武汉大学计算机学院, 湖北 武汉 430072;
    2. 福建农林大学计算机与信息学院, 福建 福州 350002;
    3. 武汉大学空天信息安全与可信计算教育部重点实验室, 湖北 武汉 430072
  • 收稿日期:2014-06-24 修回日期:2014-08-27 出版日期:2014-09-20 发布日期:2014-09-30
  • 通讯作者: 赵波（1972-），男，教授，博士，研究方向为信息系统安全、嵌入式系统.E-mail：zhaobo@whu.edu.cn E-mail:zhaobo@whu.edu.cn
  • 作者简介:纪祥敏（1971-），男，讲师，博士研究生，研究方向为信息系统安全、可信计算.E-mail：jixm168@126.com
  • 基金资助:
    国家“九七三”重点基础研究发展计划项目（2014CB340600）；国家自然科学基金重点项目（61332019）；国家自然科学基金资助项目（61173138，61272452）；湖北省重点新产品新工艺研究开发项目（2012BAA03004）

Formally analyzing VMM dynamic measurement based on extended LS2

JI Xiang-min1,2,3, ZHAO Bo1,3, XIANG Shuang1,3, XIA Zhong-lin1,3   

  1. 1. Computer School, Wuhan University, Wuhan 430072, Hubei, China;
    2. College of Computer and Information Sciences, Fujian Agriculture and Forestry University, Fuzhou 350002, Fujian, China;
    3. Key Laboratory of Aerospace Information Security and Trusted Computing, Ministry of Education, Wuhan University, Wuhan 430072, Hubei, China
  • Received:2014-06-24 Revised:2014-08-27 Online:2014-09-20 Published:2014-09-30

PDF (PC)

662

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

关键词: 虚拟机监控器, 动态度量, 安全系统逻辑

Abstract: Dynamic measurement for Virtual Machine Monitor (VMM) is a vital means to guarantee virtualized environments 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, whereby 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 practical application effect, and that the extended LS2 is effective to provide security theoretical support for virtualized environments security.

Key words: virtual machine monitor, dynamic measurement, logic of secure systems

中图分类号: 

  • TP309
[1] 赵波,向騻,张焕国,等.虚拟机环境下并行信任关系研究与实现[J]. 电子科技大学学报, 2013, 42(1):98-104. ZHAO Bo, XIANG Shuang, ZHANG Huanguo, et al.Research on parallel trust structure in virtualization[J].Journal of University of Electronic Science and Technology of China, 2013, 42(1):98-104.
[2] RUTKOWSKA J. Security challenges in virtualized environments[C]//Proceedings of RSA Conference.[S.l.]: [s.n.], 2008:78-87.
[3] CHEN C, MANIATIS P, PERRIG A, et al. Towards verifiable resource accounting for outsourced computation[C]//Proceedings of the 9th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments. New York:ACM Press, 2013:167-178.
[4] 沈昌祥, 张焕国, 王怀民, 等. 可信计算的研究与发展[J]. 中国科学:信息科学, 2010, 40(2):139-166. SHEN Changxiang, ZHANG Huanguo, WANG Huaimin, et al. Researches on trusted computing and its developments[J]. Science China:Information Sciences, 2010, 40(2):139-166.
[5] MCCUNE J M, LI Y, QU N, et al. TrustVisor:efficient TCB reduction and attestation[C]//Proceedings of 2010 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society, 2010:143-158.
[6] 刘孜文, 冯登国. 基于可信计算的动态完整性度量架构 [J]. 电子与信息学报, 2010, 32(4):875-879. LIU Ziwen, FENG Dengguo.TPM-based dynamic integrity measurement architecture[J]. Journal of Electronics & Information Technology, 2010, 32(4):875-879.
[7] 常德显, 冯登国, 秦宇, 等. 基于扩展 LS2的可信虚拟平台信任链分析[J]. 通信学报, 2013, 34(5):31-41. CHANG Dexian, FENG Dengguo, QIN Yu, et al. Analyzing the trust chain of trusted virtualization platform based on the extended LS2[J]. Journal on Communications, 2013, 34(5):31-41.
[8] DATTA A, FRANKLIN J, GARG D, et al. A logic of secure systems and its application to trusted computing[C]//Proceedings of 30th IEEE Symposium on Security and Privacy. Piscataway: IEEE Computer Society, 2009:221-236.
[9] NIST. National vulnerability database[EB/OL].[201-02-15].http://web.nvd.nist.gov/view/vuln/search-results?query=Xen&search-type=all&cves=on.
[10] 程戈, 李聪. 可信计算环境构建机制研究进展[J]. 计算机工程与应用, 2013, 49(13):59-64. CHENG Ge, LI Cong. Research progress of trusted computing environment[J]. Computer Engineering and Applications, 2013, 49(13):59-64.
[11] DAI Weiqi, JIN Hai, ZOU Deqing, et al. TEE: a virtual DRTM based execution environment for secure cloud-end computing [C]//Proceedings of the 17th ACM Conference on Computer and Communications Security. New York: ACM Press, 2010:663-665.
[12] NANEVSKI A, MORRISETT G, BIRKEDAL L. Hoare type theory, polymorphism and separation[J]. Journal of Functional Programming, 2008, 18(5-6):865-911.
[13] ZHANG Xing, HUANG Qiang, SHEN Changxiang A formal method based on noninterference for analyzing trust chain of trusted computing platform [J]. Chinese Journal of Computers, 2010, 33(1):74-81.
[14] 冯登国,秦宇. 可信计算环境证明方法研究[J].计算机学报, 2008, 31(9):1640-1652. FENG Dengguo, QIN Yu. Research on attestation method for trust computing environment [J]. Chinese Journal of Computers, 2008, 31(9):1640-1652.
[15] CHEN Shuyi, WEN Yingyou, ZHAO Hong. Formal analysis of secure bootstrap in trusted computing [M]//Autonomic and Trusted Computing. Berlin-Heidelberg: Springer, 2007: 352-360.
[16] MILLEN J, GUTTMAN J, RAMSDELL J, et al. Analysis of a measured launch[R]. Mitre Corp Bedford MA, 2007.
[17] BURROWS M, ABADI M, NEEDHAM M R.A logic of authentication[J]. Operating Systems Review, 1989, 23(5):1-13.
[18] ABADI M, FOURNET C. Mobile values, new namesand secure communication[C]//Proceedings of the 28th Symposium on Principles of Programming Languages. New York: ACM Press, 2001: 104-115.
[19] 薛锐,冯登国. 安全协议的形式化分析技术与方法[J]. 计算机学报, 2006, 29(1): 1-20. XUE Rui, FENG Dengguo.The approaches and technologies for formalverification of security protocols[J].Chinese Journal of Computers, 2006, 29(1): 1-20.
[20] FENG Wei, QIN Yu, YU Aimin, et al. A DRTM-based method for trusted network connection[C]//Proceedings of 2011 International Joint Conference of IEEE TrustCom-11/IEEE ICESS-11/FCST-11. Los Alamitos: IEEE Computer Society, 2011: 425-435.
[1] 赵丹丹,陈兴蜀,金鑫. KVM Hypervisor安全能力增强技术研究[J]. 山东大学学报（理学版）, 2017, 52(3): 38-43.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
版权所有 © 2018 《山东大学学报(理学版)》编辑部　
地址: 山东省济南市山大南路27号山东大学中心校区（250100）　电话: +86-0531-88366917　E-mail: xblxb@sdu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发