一种形式化的可信平台模块应用编程接口安全性分析方法

一种形式化的可信平台模块应用编程接口安全性分析方法 A Formal Security Analysis Method of Application Programming Interfaces for Trusted Platform Module 杨飏 YANG Yang1 1 first-author 张焕国 ZHANG Huanguo1 1 2 3 张帆 ZHANG Fan1 1 徐士伟 XU Shiwei1 1 武汉大学计算机学院 武汉大学计算机学院 School of Computer,Wuhan University School of Computer,Wuhan University 武汉大学软件工程国家重点实验室 武汉大学软件工程国家重点实验室 State Key Laboratory of Software Engineering,Wuhan University State Key Laboratory of Software Engineering,Wuhan University 空天信息安全与可信计算教育部重点实验室 空天信息安全与可信计算教育部重点实验室 Key Laboratory of Aerospace Information Security and Trust Computing ofMinistry of Education Key Laboratory of Aerospace Information Security and Trust Computing ofMinistry of Education 针对可信平台模块（TPM）应用编程接口（API）规范设计的安全性未得到有效验证,本文提出了一种形式化的安全性分析方法.具体内容包括:采用形式化模型定义应用编程接口、攻击者能力与安全目标;借助自动证明机实现了一种基于归结准则和定理证明的推理方法,在该方法中还集成了可执行状态判决机制,在一定程度上缓解了状态空间爆炸的问题.实验结果表明,可信平台模块密钥迁移功能的设计存在一定安全缺陷. Trusted Platform Module （TPM） which is the root of trusted computing provides the cryptographic functions through the Application Programming Interface （API）. However the API is defined as un-formal description in TCG’s specification and the security policies are not discussed and guaranteed by TCG. We propose a formal model to describe the APIs system based on specification. In order to automatically verify the security policies,a formal deduction model based on resolution principle and theorem proving is presented,and a mechanism of executability determination is also integrated in the method to alleviate state space explosion problem to some extent. The proposed theory and method are then applied in the Key Migration module of TPM APIs and several design faults are disclosed. 可信平台模块 安全性分析 应用编程接口 一阶逻辑 trusted platform module security analysis application programming interface first-order logic 10.14188/j.1671-8836.2010.04.020 TP309 国家高技术研究发展计划（863）项目（2007AA01Z411） 2010-04-01 2021-04-01 4 56