基于Coq的软件安全性验证  

Verification of software security based on Coq

作　　者：谯婷婷[1] 王乐[2] 王芳 葛艳[1] 

机构地区：[1]中国航空工业集团西安飞行自动控制研究所,西安710065 [2]西安电子科技大学通信工程学院,西安710071 [3]中国航空工业集团第631研究所,西安710068

出　　处：《计算机应用》2012年第A02期96-100,共5页journal of Computer Applications

基　　金：航空科学基金资助项目(20100718004)

摘　　要：针对数组越界、空指针应用和缓冲区溢出三类威胁软件安全的不规范操作,提出了一种基于Coq验证上述三类操作的形式化方法。首先编写三类安全问题的程序实例,并采用形式化方法进行标注;其次运用Frama-C和Why工具对标注程序进行解析,生成需要证明的定理;最后基于Coq集成开发环境证明定理,实现安全问题的验证。结果表明,该方法有效验证了软件安全中的三类问题,为形式化方法在软件安全性验证方面的应用奠定了基础。The security risks of software are usually caused by three kinds of non-standard operation procedures including array bounds, null point reference and buffer overflow. In order to verify these three issues, a formal method based on Coq was proposed. Firstly, the program instances related to the mentioned non-standard operations were written and marked by formal methods. Following this, the Frama-C and Why tools were employed to analyze the marked programs and thus generate the theorems to be proved. Based on this, the theorems were proved under the Coq integrated development environment to achieve the verification of security problems. Simulation results show that the proposed method effectively verifies the three kinds of security problems, which is helpful to lay a good foundation for the applications of formal methods in software verification.

关 键 词：软件安全性 形式化方法 COQ 数组越界 空指针应用 缓冲区溢出 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]