信息安全与通信保密
信息安全與通信保密
신식안전여통신보밀
CHINA INFORMATION SECURITY
2011年
7期
76-78,81
,共4页
ACSL%码软件%安全性%定理证明%形式化验证
ACSL%碼軟件%安全性%定理證明%形式化驗證
ACSL%마연건%안전성%정리증명%형식화험증
ACSL%cryptographic software%security%theorem prove%formal verification
在分析通用软件形式化验证方法的基础上,这里设计提出了一种专门针对密码软件安全性的形式化验证方法。该方法采用ACSL（ANSI/ISO C Specification Language）语言对密码软件的安全性进行形式化描述,并采用自动证明与辅助证明相结合的方法,能够对软件的实现是否满足了对安全性至关重要的一些密码学特性进行有效验证。还以一个开源openssl实现中RC4算法的软件实现部分为例,给出了对其保险性进行验证的过程与步骤,结果表明了该方法的有效性。
在分析通用軟件形式化驗證方法的基礎上,這裏設計提齣瞭一種專門針對密碼軟件安全性的形式化驗證方法。該方法採用ACSL（ANSI/ISO C Specification Language）語言對密碼軟件的安全性進行形式化描述,併採用自動證明與輔助證明相結閤的方法,能夠對軟件的實現是否滿足瞭對安全性至關重要的一些密碼學特性進行有效驗證。還以一箇開源openssl實現中RC4算法的軟件實現部分為例,給齣瞭對其保險性進行驗證的過程與步驟,結果錶明瞭該方法的有效性。
재분석통용연건형식화험증방법적기출상,저리설계제출료일충전문침대밀마연건안전성적형식화험증방법。해방법채용ACSL（ANSI/ISO C Specification Language）어언대밀마연건적안전성진행형식화묘술,병채용자동증명여보조증명상결합적방법,능구대연건적실현시부만족료대안전성지관중요적일사밀마학특성진행유효험증。환이일개개원openssl실현중RC4산법적연건실현부분위례,급출료대기보험성진행험증적과정여보취,결과표명료해방법적유효성。
This article first analyzes the formal verification for universal software,and then proposes an approach for formal verification of cryptographic software security. The approach first adopts ACSL（ANSI/ISO C Specification Language） to formally specify the security of cryptographic software,and then verifies the specifications with the method integrating automatic proof tools and interactive proof assistance. The paper,with the formal verification of RC4 arithmetic in openssl as an example explains this approach. The result shows that this approach could effectively verify properties of cryptographic software in a certain level of automation,and thus reduces the complexity of formal verification in certain degree.
