计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2012年
3期
121-123
,共3页
郝耀辉%郭渊博%罗婷%燕菊维
郝耀輝%郭淵博%囉婷%燕菊維
학요휘%곽연박%라정%연국유
Hoare逻辑%密码软件%形式化验证%程序规范%RC4算法
Hoare邏輯%密碼軟件%形式化驗證%程序規範%RC4算法
Hoare라집%밀마연건%형식화험증%정서규범%RC4산법
在Hoare逻辑理论和ACSL语法规范的基础上,设计一种针对密码软件的形式化验证系统,由程序规范、验证推理规则、可靠性策略、验证推理等模块组成.以OpenSSL中RC4算法的软件实现为例,对其功能正确性、保险性和信息流安全性进行验证,结果表明,该系统具有较高的自动化水平,可在一定程度上降低形式化验证方法的复杂度.
在Hoare邏輯理論和ACSL語法規範的基礎上,設計一種針對密碼軟件的形式化驗證繫統,由程序規範、驗證推理規則、可靠性策略、驗證推理等模塊組成.以OpenSSL中RC4算法的軟件實現為例,對其功能正確性、保險性和信息流安全性進行驗證,結果錶明,該繫統具有較高的自動化水平,可在一定程度上降低形式化驗證方法的複雜度.
재Hoare라집이론화ACSL어법규범적기출상,설계일충침대밀마연건적형식화험증계통,유정서규범、험증추리규칙、가고성책략、험증추리등모괴조성.이OpenSSL중RC4산법적연건실현위례,대기공능정학성、보험성화신식류안전성진행험증,결과표명,해계통구유교고적자동화수평,가재일정정도상강저형식화험증방법적복잡도.
