学位论文 > 优秀研究生学位论文题录展示

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

作　者: 杨思敏
导　师: 陈意云
学　校: 中国科学技术大学
专　业: 计算机软件与理论
关键词: 证明生成 自动定理证明 线性整数定理证明 出具证明编译器 程序验证 高可信软件
分类号: TP314
类　型: 硕士论文
年　份: 2010年
下　载: 40次
引　用: 1次
阅　读: 论文下载
 

内容摘要


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

全文目录


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

相似论文

  1. 有限元法在略阳电厂边坡稳定性分析中的应用与研究,TU43
  2. 基于Hoare逻辑的软件形式化验证技术研究,TP311.52
  3. 一种出具证明编译器中汇编级断言和证明的生成方法,TP314
  4. Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用,TP311.11
  5. 验证带有线程动态创建和退出多线程程序,TP311.53
  6. Web服务编排语言的分析与测试,TP393.09
  7. 一个程序验证工具的设计和实现,TP311.53
  8. 一种新的基于扩展规则的知识编译方法,TP182
  9. Java语言的类和多态性的公理语义,TP312
  10. 交互式并行定理证明环境的构建,TP181
  11. VeriJava中静态验证器的设计与实现,TP312.1
  12. 数字信号处理器MD16验证研究,TN79
  13. 基于网格计算的定理自动证明研究,TP393.01
  14. Java语言的异常处理机制的公理语义,TP312
  15. 基于计算机辅助证明的安全性保证方法研究,TP309
  16. 程序验证关键技术研究,TP311.11
  17. 低级并行代码中几种同步机制的验证,TP332
  18. 面向程序验证的循环不变式自动构造技术研究,TP311.11
  19. 基于软件事务内存的并行程序验证,TP311.5
  20. 基于计算机代数的程序验证,TP311.1

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 编译程序、解释程序
© 2012 www.xueweilunwen.com