可信运行控制软件形式化设计与验证

Formal design and verification of trusted running control

可信运行控制软件作为可信计算平台中提供可信度量服务的关键软件,其自身设计是否安全可信,是可信计算平台安全运行的基础。为保证该软件设计安全可信,基于形式化模型检验基本理论,提出了软件形式化设计框架,研究了抽象行为、安全属性和代码功能正确性建模验证方法,开展了可信运行控制软件形式化设计与验证。验证结果表明,采用形式化设计方法,能够有效地解决软件设计缺陷和安全漏洞,保证软件设计与实现的正确性、安全性与一致性。

Since the trusted running control software is the key software to provide trusted measurement service in trusted computing platform, the safety and reliability of the design is the basis of ensuring the safe running of the trusted computing platform. To ensure the safety and reliablility of the software, based on the theory of formal model testing, a software formal design framework is proposed. The modeling and verification methods of abstract behavior, security attributes and code function correctness are studied, and software formal design and verification of trusted running control are carried out. The verification results show that the formal design method can effectively solve the software design defects and security loopholes, and ensure the correctness, security and consistency of design and implementation.