基于模型检测的可信软件栈测试

摘要：

基于模型检测理论,提出了一种可信软件栈的测试方法,使用计算树逻辑对可信软件栈的函数调用进行抽象描述,通过验证可信软件栈函数的接口和函数调用是否符合规范,从而确定平台中可信软件栈的正确性.测试结果表明,一些可信计算平台产品中的软件栈不完全符合可信计算组织(TCG)的规范要求.

关键词：可信计算平台、可信软件栈、模型检测、计算树逻辑、一致性测试

所属期刊栏目：56

分类号：TP309(计算技术、计算机技术)

资助基金：国家高技术研究发展计划863项目2007AA01Z411;2008AA01Z404;国家自然科学基金资助项目60673071;60743003;90718005;空天信息安全与可信计算教育部重点实验室开放基金资助项目AISTC2008Q01;AISTC2008Q02

在线出版日期：2010-09-17（万方平台首次上网日期，不代表论文的发表时间）

页码：129-132