基于Hoare逻辑的密码软件形式化验证系统  

Formal Verification System of Cryptographic Software Based on Hoare Logic

作　　者：郝耀辉[1] 郭渊博[1] 罗婷[1] 燕菊维[1] 

机构地区：[1]解放军信息工程大学电子技术学院,郑州450004

出　　处：《计算机工程》2012年第3期121-123,共3页Computer Engineering

基　　金：国家"863"计划基金资助项目"基于规范的容忍入侵中间件关键技术与平台"(2007AA01Z405);河南省科技创新杰出青年计划基金资助项目(104100510025)

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

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

分 类 号：TP319[自动化与计算机技术—计算机软件与理论]