JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE) ›› 2014, Vol. 49 ›› Issue (09): 1-8.doi: 10.6040/j.issn.1671-9352.2.2014.408

    Next Articles

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

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

CLC Number: 

  • 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] ZHAO Dan-dan, CHEN Xing-shu, JIN Xin. A study on security enhancement technology for KVM Hypervisor [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2017, 52(3): 38-43.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
Copyright 2018 © Editorial office of JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE)
Supported by Beijing Magtech Co.Ltd