可信平台模块(Trusted Platform Module,TPM)是可信计算平台的核心和基础,可信平台模块的功能测试和验证是保证可信平台模块的实现正确性以及规范一致性的重要手段,但是目前尚不存在一种有效严格的可信平台模块测试和功能验证方法,同时可信计算组织给出的TPM规范是描述性的,不利于产品的开发和测试.文中在分析可信平台模块目前存在的一些问题的基础上,以TPM密码子系统为例给出了该子系统的形式化规格说明,并且基于该规格说明,给出了扩展有限状态机模型,最后,将该有限状态机模型应用于测试用例的自动生成,并通过实验验证了形式化测试的有效性.
Trusted platform module is the core component of trusted computing platform, the functional testing and validation is an important method to ensure the correctness and specification compliance of the trusted platform module, but until now, there is no valid formal testing and validation method, meanwhile the specification which is given by trusted computing group is descriptive, it is not convenient for product development and testing. The paper firstly analyzes the problem of the trusted platform module, and then gives the Z specification of TPM's cryptography system, based on this formal specification, gives the extended finite state machine model. Finally, the authors use the EFSM model for generating the test case and analyze the testing results.