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

• 作者: 燕菊维 罗婷 郝耀辉 郭渊博
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: Hoare逻辑 密码软件 形式化验证 程序规范 RC4算法
• 年，卷（期）: 2012,（3）
• 所属期刊栏目: 安全技术
• 页码范围: 121-123
• 分类号: TP319
• 字数: 3312字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2012.03.041

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郝耀辉	解放军信息工程大学电子技术学院	11	49	4.0	6.0
2	郭渊博	解放军信息工程大学电子技术学院	76	462	13.0	17.0
3	燕菊维	解放军信息工程大学电子技术学院	3	12	3.0	3.0
4	罗婷	解放军信息工程大学电子技术学院	1	3	1.0	1.0