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

摘要：

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

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

所属期刊栏目：38

分类号：TP319(计算技术、计算机技术)

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

在线出版日期：2012-06-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：121-123