作者：谯婷婷 王乐 王芳 葛艳软件安全性形式化方法coq数组越界空指针应用缓冲区溢出
摘要：针对数组越界、空指针应用和缓冲区溢出三类威胁软件安全的不规范操作，提出了一种基于Coq验证上述三类操作的形式化方法。首先编写三类安全问题的程序实例，并采用形式化方法进行标注；其次运用Frama-C和Why工具对标注程序进行解析，生成需要证明的定理；最后基于Coq集成开发环境证明定理，实现安全问题的验证。结果表明，该方法有效验证了软件安全中的三类问题，为形式化方法在软件安全性验证方面的应用奠定了基础。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
