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

A Formal Security Analysis Method of Application Programming Interfaces for Trusted Platform Module

作　　者：杨飏[1] 张焕国[1,2,3] 张帆[1] 徐士伟[1] 

机构地区：[1]武汉大学计算机学院,湖北武汉430072 [2]武汉大学软件工程国家重点实验室,湖北武汉430072 [3]空天信息安全与可信计算教育部重点实验室,湖北武汉430072

出　　处：《武汉大学学报（理学版）》2010年第4期446-450,共5页Journal of Wuhan University:Natural Science Edition

基　　金：国家高技术研究发展计划(863)项目(2007AA01Z411)

摘　　要：针对可信平台模块(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.

关 键 词：可信平台模块 安全性分析 应用编程接口 一阶逻辑 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]