计算机应用 ›› 2018, Vol. 38 ›› Issue (2): 337-342.DOI: 10.11772/j.issn.1001-9081.2017082168

• 网络空间安全 • 上一篇    下一篇

满足对应性属性的平台配置证明

徐明迪1, 高杨1, 高雪原1, 张帆2   

  1. 1. 武汉数字工程研究所, 武汉 430205;
    2. 武汉轻工大学 数学与计算机学院, 武汉 430023
  • 收稿日期:2017-08-21 修回日期:2017-09-17 出版日期:2018-02-10 发布日期:2018-02-10
  • 通讯作者: 张帆
  • 作者简介:徐明迪(1980-),男,湖北武汉人,副研究员,博士,CCF会员,主要研究方向:可信计算、云安全、安全形式化;高杨(1993-),女,黑龙江哈尔滨人,硕士研究生,主要研究方向:可信计算;高雪原(1991-),男,湖北襄阳人,硕士研究生,主要研究方向:可信计算;张帆(1977-),男,湖北宜昌人,副教授,博士,主要研究方向:恶意代码分析。
  • 基金资助:
    国家自然科学基金资助项目(61502438)。

Correspondence property-based platform configuration attestation

XU Mingdi1, GAO Yang1, GAO Xueyuan1, ZHANG Fan2   

  1. 1. Wuhan Digital and Engineering Institute, Wuhan Hubei 430205, China;
    2. School of Mathematics and Computer Science, Wuhan Polytechnic University, Wuhan Hubei 430023, China
  • Received:2017-08-21 Revised:2017-09-17 Online:2018-02-10 Published:2018-02-10
  • Supported by:
    This work is partially supported by the National Natural Science Foundation of China (61502438).

摘要: 针对完整性报告协议(IRP)存在局部和全局攻击的安全隐患,对StatVerif进行语法扩展,增加了与完整性度量相关的构造算子和析构算子,通过对平台配置证明(PCA)安全进行分析,发现其存在的局部攻击和全局攻击,包括通过未授权命令对平台配置寄存器和存储度量日志进行篡改。对攻击者能力进行了建模,详细说明了攻击者如何通过构造子和析构子形成知识,进而对平台配置证明进行攻击。最后,在平台配置证明不满足对应性属性的情况下,从理论上证明了攻击序列的存在,并给出了平台配置证明满足局部可靠和全局可靠的条件,通过形式化验证工具Proverif证明了命题的合理性。

关键词: 可信计算, 完整性报告协议, 平台配置证明, 对应性属性, StatVerif演算, Proverif验证

Abstract: Concerning the security problem of local and global attacks on the Integrity Report Protocol (IRP), the StatVerif syntax was extended by adding constructors and destructors associated with the integrity measurement. The security of the Platform Configuration Attestation (PCA) was analyzed and the local and global attacks were found, including tampering the platform configuration register or revising stored measurement log by running unauthorized commands. The abilities of attackers were modeled, and how attackers accumulated knowledge and tampered PCA protocol by using constructors and destructors was introduced. Finally, the existence of attacking sequence was proved theoretically when PCA does not satisfy the correspondence property; and several propositions that PCA can meet the local reliability and gloabal reliability were given, which were proved by the formal verification tool Proverif.

Key words: trusted computing, Integrity Report Protocol (IRP), Platform Configuration Attestation (PCA), correspondence property, StatVerif calculus, Proverif verification

中图分类号: