基于Coq的软件安全性验证研究与实现-电子与通信工程专业论文.docxVIP

万方数据 万方数据 摘要 随着软件开发技术的不断发展和演变，软件的发展已日趋于精细化和智能化。 但是，软件安全问题仍是困扰软件开发人员的关键问题。人们对软件安全的要求 逐步提高，高可信软件越来越受到亲睐。如何保证软件系统的安全，已经成为一 个迫切需要解决的问题。使用传统的软件测试方法对软件进行测试时，所测试软 件总是存在错误或漏洞，无法保证软件的绝对安全性。近年来，用形式化方法在 软件开发过程中进行严格推理是提高软件安全性的有效途径。在众多的形式化方 法中，从构造程序形式证明的角度来支持代码安全性的研究引起了广泛关注。 本文针对数组越界、空指针引用和缓冲区溢出三类威胁软件安全的不规范操 作，提出了一种基于 Coq 的验证上述三类操作的形式化方法和证明系统。首先编 写三类安全问题的程序实例，并采用形式化方法进行标注；其次运用 Frama-C 和 Why 工具对标注程序进行解析，生成需要证明的定理；最后基于 Coq 集成开发环 境证明定理，实现安全问题的验证。结果表明，本文提出的方法有效验证了软件 安全中的三类问题，为形式化方法在软件安全性验证方面的应用奠定了基础。 关键词：软件安全性 形式化方法 交互式定理证明 Coq Abstract With the continuous development and evolution of software development technology, the development of software has become increasingly refinement and intelligent. But, software security is a key issue which remains plagued by software developers. As a result, the requirement for software with soundness and safety becomes more and more urgent. The problem of software safety once becomes the most important aspect. But, traditional software testing methods cannot guarantee the absolute security of the software, since software always exist errors or bugs which have been tested. To resolve this, developing high-assurance software based on formal methods is an essential approach. Among various formal methods，proof-carrying- code-based approach has attracted widespread attention. In this paper, 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 the three issues, a formal method and proof system based on Coq is proposed. Firstly, the program instances related to the aforementioned non-standard operations are written and marked by formal methods. Following this, the Frama-C and Why tools are employed to analyze the marked programs and thus generate the theorems to be proved. Based on this, the theorems are proved under the Coq integrated developed environment to achieve the verification of security problems. Simulati