基于ACSL的密码软件形式化验证方法  

An ACSL-based Formal Verification of Cryptographic Software

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

机构地区：[1]中国人民解放军信息工程大学电子技术学院

出　　处：《信息安全与通信保密》2011年第7期76-78,81,共4页Information Security and Communications Privacy

摘　　要：在分析通用软件形式化验证方法的基础上,这里设计提出了一种专门针对密码软件安全性的形式化验证方法。该方法采用ACSL(ANSI/ISO C Specification Language)语言对密码软件的安全性进行形式化描述,并采用自动证明与辅助证明相结合的方法,能够对软件的实现是否满足了对安全性至关重要的一些密码学特性进行有效验证。还以一个开源openssl实现中RC4算法的软件实现部分为例,给出了对其保险性进行验证的过程与步骤,结果表明了该方法的有效性。This article first analyzes the formal verification for universal software,and then proposes an approach for formal verification of cryptographic software security. The approach first adopts ACSL（ANSI/ISO C Specification Language） to formally specify the security of cryptographic software,and then verifies the specifications with the method integrating automatic proof tools and interactive proof assistance. The paper,with the formal verification of RC4 arithmetic in openssl as an example explains this approach. The result shows that this approach could effectively verify properties of cryptographic software in a certain level of automation,and thus reduces the complexity of formal verification in certain degree.

关 键 词：ACSL 码软件 安全性 定理证明 形式化验证 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]