| 基于ACSL的密码软件形式化验证方法 |
| |
| 引用本文： | 罗婷,郭渊博,郝耀辉.基于ACSL的密码软件形式化验证方法[J].信息安全与通信保密,2011,9(7):76-78,81. |
| |
| 作者姓名： | 罗婷 郭渊博 郝耀辉 |
| |
| 作者单位： | 中国人民解放军信息工程大学电子技术学院,河南郑州,450004 |
| |
| 摘 要： | 在分析通用软件形式化验证方法的基础上,这里设计提出了一种专门针对密码软件安全性的形式化验证方法。该方法采用ACSL（ANSI/ISO C Specification Language）语言对密码软件的安全性进行形式化描述,并采用自动证明与辅助证明相结合的方法,能够对软件的实现是否满足了对安全性至关重要的一些密码学特性进行有效验证。还以一个开源openssl实现中RC4算法的软件实现部分为例,给出了对其保险性进行验证的过程与步骤,结果表明了该方法的有效性。
|
| 关 键 词： | ACSL 码软件 安全性 定理证明 形式化验证 |
An ACSL-based Formal Verification of Cryptographic Software |
| |
| LUO Ting,GUO Yuan-bo,HAO Yao-hui.An ACSL-based Formal Verification of Cryptographic Software[J].China Information Security,2011,9(7):76-78,81. |
| |
| Authors: | LUO Ting GUO Yuan-bo HAO Yao-hui |
| |
| Institution: | LUO Ting,GUO Yuan-bo,HAO Yao-hui (Institute of Electronic Technology,PLA Information Engineering College,Zhengzhou Henan 450004,China) |
| |
| Abstract: | 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. |
| |
| Keywords: | ACSL cryptographic software security theorem prove formal verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
