基于 Coq 的软件安全性验证
1 谯婷婷 ， 王 2 乐 ， 王
*Байду номын сангаас
3 芳， 葛
艳
1
（ 1． 中国航空工业集团 西安飞行自动控制研究所， 西安 710065 ；
2． 西安电子科技大学 通信工程学院， 西安 710071 ；
3． 中国航空工业集团 第 631 研究所， 西安 710068 ） ( * 通信作者电子邮箱 wangle_xidian@ 126． com)
*
Abstract: The security risks of software are usually caused by three kinds of nonstandard 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 nonstandard operations were written and marked by formal methods． Following this， the FramaC 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． Key words: software security; formal method; Coq; array bound; null pointer reference; buffer overflow
摘 要： 针对数组越界、 空指针应用和缓冲区溢出三类威胁软件安全的不规范操作， 提出了一种基于 Coq 验证上述 。 ， C 和 Why 三类操作的形式化方法 首先编写三类 安 全 问题 的程 序 实 例 并 采 用 形式化 方 法 进行 标 注; 其 次 运 用 Frama工具对标注程序进行解析， 生成需要证明的定理; 最后基于 Coq 集成开发环境证明定理， 实现安全问题的 验 证。结 果表 明， 该方法有效验证了软件安全中的三类问题， 为形式化方法在软件安全性验证方面的应用奠定了基础。 关键词： 软件安全性; 形式化方法; Coq; 数组越界; 空指针应用; 缓冲区溢出 中图分类号： TP311 文献标志码： A
0
引言
随着软件在尖端领域的应用以及互联网技术的发展， 人 们对软件的依赖性越来越大， 软件已成为人们生活中的必需 品， 软件系统的任何一个环节工作失败或是遭受攻击都会带 来难以预料的灾难性后果， 给人们的生产和生活带来巨大的 甚至造成不可恢复的创伤， 因此软件安全的重要性与日 灾难， ［1 ］ 俱增。软件安全 是指软件程序中不会出现不规范的操作， 这类不规范操作通常包括缓冲区溢出 、 数组越界、 空指针引 用。违反软件安全的行为通常会引起系统级的保密安全问 题， 因此如何有效地保护软件安全是一个亟待解决的问题 。 传统的开发软件方法采用软件测试来确定程序是否满足应用 的需求， 而实际上软件测试仅能检查程序在某些具体点上的 执行行为， 无法保证整个系统行为的正确性 。 这也就是“软 。 件测试只能说明 bugs 的存在， 而不能说明它们的不存在 ” 采用这一方式开发的安全关键软件系统， 它的安全性和可靠 性只能靠长时间的测试来支持， 通过长期使用发现和更正错 ， 误的方式逐渐“改善 ” 缺乏本质上的安全保障 。 因此， 运用 ［2 ］ 形式化方法 对软件进行严格推理是提高软件安全性的有 效途径。形式化方法是一种以严格的数学公式和理论描述程 序语义， 并提供基于语义检查和推理程序的方法 。 该方法多
Journal of Computer Applications 计算机应用，2012，32( S2) : 96 － 100 文章编号： 1001 － 9081 （ 2012 ） S2 － 0096 － 05
ISSN 1001-9081 CODEN JYIIDU
2012-12-31 http: / / www． joca． cn
Verification of software security based on Coq
QIAO Tingting1 ， WANG Le2 ， WANG Fang3 ， GE Yan1
( 1 ． Xi an Flight Automation Control Research Institute， Aviation Industry Corporation of China， Xi an Shaanxi 710065 ， China; 2 ． School of Telecommunications Engineering， Xidian University， Xi an Shaanxi 710071 ， China; 3 ． Xi an 631 Research Institute， Aviation Industry Corporation of China， Xi an Shaanxi 710068 ， China)