基于Coq的软件安全性验证

摘要

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