| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 可信平台模块的形式化分析和测试 |
| 作者 | 陈小峰 |
| 作者单位 | (中国科学院软件研究所信息安全国家重点实验室 北京 100190) (信息安全共性技术国家工程研究中心 北京 100190) |
| 发表年份 | 2009 |
| 发表月份 | 4期(646—653) |
| 文章摘要 | 摘要 可信平台模块(Trusted Platform Module,TPM)是可信计算平台的核心和基础，可信平台模块的功能测试和验证是保证可信平台模块的实现正确性以及规范一致性的重要手段，但是目前尚不存在一种有效严格的可信平台模块测试和功能验证方法，同时可信计算组织给出的TPM规范是描述性的，不利于产品的开发和测试.文中在分析可信平台模块目前存在的一些问题的基础上，以TPM密码子系统为例给出了该子系统的形式化规格说明，并且基于该规格说明，给出了扩展有限状态机模型，最后，将该有限状态机模型应用于测试用例的自动生成，并通过实验验证了形式化测试的有效性. 关键词 可信计算平台;可信平台模块;一致性测试;形式化分析 中图法分类号: TP309 DOI号: 10.3724/SP.J.1016.2009.00646 |