基于模型检测的可信软件栈测试 (2010年)

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