Abstract: Based on Hoare logic and ANSI/ISO C Specification Language(ACSL) specification, this paper presents a formal verification system for cryptographic software, which is composed of program specification, inference rules, reliability strategy and verification module. It takes the software realization of RC4 algorithm in OpenSSL as an example, the functional correctness, safety properties and information flow security are tested and verified. Results show that this system can reduce the complexity of formal verification method and has a high level of automation.

Key words: Hoare logic, cryptographic software, formal verification, program specification, RC4 algorithm

摘要： 在Hoare逻辑理论和ACSL语法规范的基础上，设计一种针对密码软件的形式化验证系统，由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL中RC4算法的软件实现为例，对其功能正确性、保险性和信息流安全性进行验证，结果表明，该系统具有较高的自动化水平，可在一定程度上降低形式化验证方法的复杂度。

关键词: Hoare逻辑, 密码软件, 形式化验证, 程序规范, RC4算法

CLC Number: 

• TP319