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

作     者：郝耀辉 郭渊博 罗婷 燕菊维 HAO Yao-hui;GUO Yuan-bo;LUO Ting;YAN Ju-wei

作者机构：解放军信息工程大学电子技术学院郑州450004 

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

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2012年第38卷第3期

页      码：121-123页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1000-3428.2012.03.041

馆 藏 号：203288167...