计算机工程2012，Vol.38Issue(3)：121-123,3.DOI:10.3969/j.issn.1000-3428.2012.03.041
基于Hoare逻辑的密码软件形式化验证系统
Formal Verification System of Cryptographic Software Based on Hoare Logic
摘要
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.关键词
Hoare逻辑/密码软件/形式化验证/程序规范/RC4算法Key words
Hoare logic/ cryptographic software/ formal verification/ program specification: RC4 algorithm分类
信息技术与安全科学引用本文复制引用
郝耀辉,郭渊博,罗婷,燕菊维..基于Hoare逻辑的密码软件形式化验证系统[J].计算机工程,2012,38(3):121-123,3.基金项目
国家“863”计划基金资助项目“基于规范的容忍入侵中间件关键技术与平台”(2007AA01Z405) （2007AA01Z405）
河南省科技创新杰出青年计划基金资助项目(104100510025) （104100510025）
