PDF《逻辑的密 的密》

计算机工程 2012, 38(3) 121-123 DOI: 10.

3969/j.issn.1000- 3428.2012.03.041 ISSN: 1000-3428 CN: 31-1289/TP Previous Articles Next Articles 本期目录 | 下期目录 | 过刊浏览 | 高级检索 [打印本页] [关闭] 安全技 安全技 安全技 安全技术 术术术扩扩扩扩展功能 展功能 展功能 展功能 本文信息 Supporting info PDF(272KB) [HTML] 下载 参考文献[PDF] 参考文献 服务与反馈 把本文推荐给朋友 加入我的书架 加入引用管理器 引用本文 Email Alert 文章反馈 浏览反馈信息 本文关键词相关文章 Hoare逻辑 密码软件 形式化验证 程序规范 RC4算法 本文作者相关文章 郝耀辉 郭渊博 罗婷 燕菊维 PubMed Article by Hao, Y. H. Article by Guo, Y. B. Article by Luo, T. Article by Yan, J. W. 基于 基于 基于 基于Hoare逻辑 逻辑 逻辑 逻辑的密 的密 的密 的密码软 码软 码软 码软件形式化 件形式化 件形式化 件形式化验证 验证 验证 验证系 系系系统 统统统郝郝郝郝耀 耀耀耀辉 辉辉辉,郭 ,郭 ,郭 ,郭渊 渊渊渊博, 博, 博, 博,罗罗罗罗婷婷婷婷,燕菊 ,燕菊 ,燕菊 ,燕菊维 维维维(解放军信息工程大学电子技术学院,郑州 450004) 摘要 摘要 摘要 摘要: 在Hoare逻辑理论和ACSL语法规范的基础上,设计一种针对密码软件的形式化验证系统,由程序规范、 验证推理规则、可靠性策略、验证推理等模块组成.以OpenSSL中RC4算法的软件实现为例,对其功能正确性、 保险性和信息流安全性进行验证,结果表明,该系统具有较高的自动化水平,可在一定程度上降低形式化验证方 法的复杂度. 关键词 关键词 关键词 关键词: Hoare逻辑 密码软件 形式化验证 程序规范 RC4算法 Formal Verification System of Cryptographic Software Based on Hoare Logic HAO Yao-hui, GUO Yuan-bo, LUO Ting, YAN Ju-wei (Institute of Electronic Technology, PLA Information Engineering University, Zhengzhou 450004, China) 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. Keywords: Hoare logic cryptographic software formal verification program specification RC4 algorithm 收稿日期 收稿日期 收稿日期 收稿日期 2011-05-17 修回日期 修回日期 修回日期 修回日期 网网网网络 络络络版 版版版发 发发发布日期 布日期 布日期 布日期 2012-02-05 DOI: 10.3969/j.issn.1000-3428.2012.03.041 基金 基金 基金 基金项 项项项目 目目目: 国家"863"计划基金资助项目"基于规范的容忍入侵中间件关键技术与平台"(2007AA01Z405);

河南省科技创 新杰出青年计划基金资助项目(104100510025) 通通通通讯 讯讯讯作者 作者 作者 作者: 作者 作者 作者 作者简 简简简介 介介介: 郝耀辉(1978-),女,讲师、硕士,主研方向:信息安全,密码学,数据库技术;

郭渊博,副教授、 博士;

罗婷,硕士研究生;

燕菊维,助教、硕士 通通通通讯 讯讯讯作者 作者 作者 作者E-mail: hao_yaohui@126.com 参参参参考文 考文 考文 考文献 献献献: : : : [2] 杨静. 用Hoare 逻辑验证程序的一般方法及实例[J].通讯和计算机.2007, 4(2):79-81 [3] Baudin P, Cuoq P, Jean-Christophe F, et al. ACSL: ANSI/ISO C Specification Language Version 1.5[EB/OL]. [2011-02-21]. http:// frama-c.com/download/acsl.pdf. [4] Almeida J B, Barbosa M, Pinto J S, et al. Deductive Verification of Cryptographic Software [J].Innovations in Systems and Software Engineering.2010, 6(3):203-218 [5] 李兆鹏, 陈意云, 葛琳, 等. 一种汇编程序的形式验证框 架[J].计算机研究与发展.2008, 45(5):825-