出具证明编译器中证明生成的研究

论文摘要

随着计算机科学技术的飞速发展,计算机软件的规模日益庞大,调试和维护越来越困难。而另一方面,软件的安全形势严峻,对未受信源提供的代码的安全执行问题逐渐凸现出来。在这种背景下,关系国计民生的关键领域、行业,对高可信软件的需求不断增大。在各种构建高可信软件的技术中,形式化程序验证通过形式化程序的性质并给出形式化证明来保证软件的安全性,能够从理论上保证程序运行时不会违反安全规范。作为验证编译器的一个重要分支,出具证明编译器结合了现代编译技术和程序验证方法,在生成汇编代码的同时,根据程序员对源程序的标注生成相应的程序性质的证明。代码消费方只需要使用可信任的证明检查器去静态地检查所生成的证明,就能间接地检查程序的安全性,从而将编译器排除在被信任计算基础之外。在出具证明编译器的理论框架中,自动定理证明技术发挥着关键作用。没有自动定理证明器的支持,程序性质的证明全部需要程序员手工完成,工作量巨大。我们在实验室前期出具证明编译器项目PLCC的基础上,设计并实现了一个出具证明编译器CComp,其主要特点是使用了Hoare风格的程序验证方法,应用分离逻辑来表达验证条件,特别是关于指针的验证条件,同时引入了现代的自动定理证明技术自动地证明验证条件,借鉴了基于栈的验证汇编编程框架的形式化定义来构建后端的目标程序验证框架。其内嵌的自动定理证明器,主要支持线性整数理论和分离逻辑,并能生成可由辅助定理证明工具Coq检查的证明。在本文中,我们首先介绍了项目的研究背景和现状,然后简单介绍了我们设计的出具证明编译器CComp,包括源语言、断言语言、源级验证框架和目标级验证框架。在源级验证框架下,本文着重介绍了基于Simplex算法和Boundand Branch方法设计和实现的线性整数定理证明器,以及本人提出的用于保存、管理证明信息和生成证明项的证明库机制,描述了部分关键算法,如实数可满足性检查过程、证明库中证明信息的保存过程、证明生成的主算法等。最后,本文给出了两个简单的测试。结果表明,我们的线性整数定理证明器完全可以自动地证明出具证明编译器CComp生成的关于线性整数程序的验证条件,并且其生成的证明优于Coq中证明策略Omega生成的证明。本文的主要贡献如下:1.基于Simplex算法和Bound and Branch方法,设计并实现了一个支持线性整数命题求解的自动定理证明器,用于证明CComp中线性整数的验证条件。2.提出了自己的一套证明项构造的方法,用于自动定理证明器生成Coq可检查证明项。该方法能自动地根据构造证明项的需要去选取已有的零散的证明信息,将它们组合形成一个基本上不含冗余的证明项。其生成的证明项与Coq自带的证明策略生成的证明项相比更加简单。本工作的意义在于,通过对线性整数定理证明器中机器可检查证明的生成问题的探索,提出了一套用于构造证明项的新方法,积累了在论域专用逻辑的自动定理证明技术方面的研究经验,为将来达到自动程序验证、构建高可信软件打下了一定的理论和技术基础。

论文目录

• 摘要
• ABSTRACT
• 目录
• 表格
• 插图
• 第1章 绪论
• 1.1 研究背景
• 1.1.1 高可信软件
• 1.1.2 程序验证
• 1.1.3 验证编译器
• 1.1.4 自动定理证明器
• 1.1.5 Coq
• 1.2 研究现状
• 1.2.1 程序验证的相关研究
• 1.2.2 自动定理证明技术的相关研究
• 1.3 本文概述
• 1.3.1 研究工作
• 1.3.2 本文贡献
• 1.3.3 章节安排
• 第2章 出具证明编译器CComp
• 2.1 源程序
• 2.1.1 Clike 语言简介
• 2.1.2 断言语言
• 2.1.3 源程序示例
• 2.2 源级验证系统
• 2.2.1 自动定理证明器
• 2.3 目标级验证系统
• 2.4 本章小结
• 第3章 线性整数定理证明器
• 3.1 线性整数命题分解
• 3.2 线性整数表达式规范化
• 3.3 基于Simplex 算法的决策过程
• 3.4 线性整数表达式处理
• 3.5 证明的生成
• 3.6 本章小结
• 第4章 证明的管理和构造
• 4.1 Coq 的证明项
• 4.2 表示证明项的数据结构
• 4.3 证明库和证明信息的保存
• 4.4 证明项的生成
• 4.5 本章小结
• 第5章 实验评测
• 5.1 我们的线性整数定理证明器与Omega 的比较
• 5.2 出具证明编译器CComp 中线性整数定理证明器的测试
• 5.3 实验结果总结
• 第6章 结束语
• 6.1 论文工作总结
• 6.2 进一步的工作
• 参考文献
• 附录 验证条件的数据结构定义
• 致谢
• 在读期间发表的学术论文与取得的研究成果