随着软件开发技术的不断发展和演变，软件的发展已日趋于精细化和智能化。但是，软件安全问题仍是困扰软件开发人员的关键问题。人们对软件安全的要求逐步提高，高可信软件越来越受到亲睐。如何保证软件系统的安全，已经成为一个迫切需要解决的问题。使用传统的软件测试方法对软件进行测试时，所测试软件总是存在错误或漏洞，无法保证软件的绝对安全性。近年来，用形式化方法在软件开发过程中进行严格推理是提高软件安全性的有效途径。在众多的形式化方法中，从构造程序形式证明的角度来支持代码安全性的研究引起了广泛关注。本文针对数组越界、空指针引用和缓冲区溢出三类威胁软件安全的不规范操作，提出了一种基于Coq的验证上述三类操作的形式化方法和证明系统。首先编写三类安全问题的程序实例，并采用形式化方法进行标注；其次运用Frama-C和Why工具对标注程序进行解析，生成需要证明的定理；最后基于Coq集成开发环境证明定理，实现安全问题的验证。结果表明，本文提出的方法有效验证了软件安全中的三类问题，为形式化方法在软件安全性验证方面的应用奠定了基础。