|
|||||
|
|
| 基于模型检测的可信软件栈测试 | |
| 引用本文： | 何凡,张焕国,严飞,杨飏,汪红,孟学军.基于模型检测的可信软件栈测试[J].武汉大学学报(理学版),2010,56(2). |
| 作者姓名： | 何凡 张焕国 严飞 杨飏 汪红 孟学军 |
| 作者单位： | 1. 武汉大学,计算机学院,湖北,武汉,430072;武汉理工大学,计算机科学与技术学院,湖北,武汉,430063 2. 武汉大学,计算机学院,湖北,武汉,430072;武汉大学,空天信息安全与可信计算教育部重点实验室,湖北,武汉,430072 3. 武汉大学,计算机学院,湖北,武汉,430072 4. 湖北省政府采购中心,湖北,武汉,430072 5. 武汉大学,网络中心,湖北,武汉,430072 |
| 基金项目： | 国家高技术研究发展计划(863)项目(2007AA01Z411,2008AA01Z404); 国家自然科学基金资助项目(60673071,60743003,90718005); 空天信息安全与可信计算教育部重点实验室开放基金资助项目(AISTC2008Q01,AISTC2008Q02) |
| 摘 要： | 基于模型检测理论,提出了一种可信软件栈的测试方法,使用计算树逻辑对可信软件栈的函数调用进行抽象描述,通过验证可信软件栈函数的接口和函数调用是否符合规范,从而确定平台中可信软件栈的正确性.测试结果表明,一些可信计算平台产品中的软件栈不完全符合可信计算组织(TCG)的规范要求. |
| 关 键 词： | 可信计算平台 可信软件栈 模型检测 计算树逻辑 一致性测试 |
Test of Trusted Software Stack Based on Model Checking |
|
| HE Fan,ZHANG Huanguo,YAN Fei,YANG Yang,WANG Hong,MENG Xuejun.Test of Trusted Software Stack Based on Model Checking[J].JOurnal of Wuhan University:Natural Science Edition,2010,56(2). | |
| Authors: | HE Fan ZHANG Huanguo YAN Fei YANG Yang WANG Hong MENG Xuejun |
| Affiliation: | HE Fan1,2,ZHANG Huanguo1,3,YAN Fei1,YANG Yang1,WANG Hong4,MENG Xuejun5(1.School of Computer,Wuhan University,Wuhan 430072,Hubei,China,2.School of Computer Science , Technology,Wuhan University of Technology,Wuhan 430063,3.Key Laboratory of Aerospace Information Security , Trusted Computing of Ministry of Education,4.Department of Government Procurement of Hubei Province,Wuhan 430071,5.Network Center,... |
| Abstract: | This paper presents a test method on TSS by model checking,and takes computation tree logics to formalize the function call of TSS,our aim is to confirm that the function call of TSS can successfully discriminate a trusted sequence from an insecure one.As a result,our test shows that the TSS on some trusted computing platforms incompletely meet the specification of trusted computing group. |
| Keywords: | trusted computing platform trusted software stack model checking computation tree logics conformance testing |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
