基于逻辑的程序验证方法在高可信软件开发上的应用

论文摘要

随着软件规模的越来越大，软件的安全越来越引起软件开发人员的关注，而现有的编程语言以及软件开发方法所能提供的安全保证是脆弱和不可靠的，例如通过标准的软件工程方法和大量的测试减少软件漏洞的发生，但是即使经过高强度测试的软件，也不能保证它没有漏洞，另外一方面，对一个漏洞的修复也往往会引起新的漏洞。可以说，现有的软件工程方法对软件安全的提高已经越来越微弱。而基于语言的程序验证方法能为软件安全提供可靠的保证。 基于语言的程序验证方法通过对程序设计语言添加静态的类型以及规范结构，使得用这种语言写出的良形式程序是安全的。现有的关于认证代码技术以及类型系统方面的研究已经能够验证低级语言和高级语言程序的多种安全属性。例如，当前的大部分程序设计语言都有一个类型系统，它一般用于检查程序的一些简单语义错误，可靠的类型系统可以以较低的代价保证程序的一些基本安全属性。安全的高级语言和通用中间层语言的类型系统的研究已经对安全计算做了有意义的贡献，但是用这些语言写就的安全程序还需经过多步的未经编译和优化才能在最终的硬件上运行，这使得最终运行的代码是未经验证的。基于这个原因，很多工作转向研究低级代码的验证，特别是研究从类型化高级语言代码产生可验证低级代码的认证编译器。但是由于类型的弱表达能力，使得类型系统只能保证代码一些最基本的安全属性，对用户指明的一些安全属性，比如算法正确性，信息流安全等基本不能触及。也正由于这个原因，对于现实的底层软件如启动引导程序，操作系统内核，用户态运行时函数库等，都没有相应的经过验证版本发布出来，而这些底层软件的安全性对整个计算系统的安全性来说是至关重要的。但是，类型系统对栈式函数调用的模块化验证有比较好的支持。另一方面，Hoare逻辑具有很强的表达能力，因为相对于类型的弱表达能力，逻辑谓词能够表达更丰富的程序属性，但是Hoare逻辑对栈式函数调用的支持比较弱。基于此，本文的研究目标是以逻辑谓词代替类型作为规范标注程序，结合类型系统和Hoare逻辑两方面的优点，设计可以模块化地构造程序满足规范的证明的框架，并使用它进行安全代码的开发。 本文提出一个基于逻辑的使用汇编语言的高可信软件开发方法，并运用此方法开发出经过严格安全验证的运行时库和操作系统组件。此方法源于Hoare逻辑的程序推理以及耶鲁大学的认证汇编编程(CAP)，它首先需要定义一个推理需要的目标机器和一组静态推理规则，并且证明推理规则的可靠性(安全性)。本文的贡献有如下几个方面： ·设计并使用Coq实现一个现实的x86平台上的认证汇编语言RCAL86，并证明

论文目录

• 摘要
• Abstract
• 第一章 背景介绍
• 1.1 基本概念
• 1.1.1 程序的安全属性
• 1.1.2 信任计算基
• 1.1.3 规范语言的表达能力
• 1.2 Curry-Howard同构
• 1.3 Hoare逻辑
• 1.4 类型系统
• 1.4.1 类型化高级语言
• 1.4.2 类型化汇编语言
• 1.5 传统的携带证明的代码
• 1.5.1 基于语义的基础携带证明的代码FPCC
• 1.5.2 基于语法的FPCC
• 1.6 本文的内容
• 第二章 程序规范语言GALLINA和定理证明工具Coq
• 2.1 项语法
• 2.2 GALLINA的命令语言Vernacular
• 2.3 使用Coq描述程序规范
• 2.4 Coq的交互式定理证明
• 2.5 本节小结
• 第三章 一个简单的支持函数调用返回的认证汇编语言RCAL86
• 3.1 引言
• 3.2 RCAL86的设计目标
• 3.3 目标机器和操作语义
• 3.3.1 RCAL86的抽象存储模型
• 3.3.2 RCAL86的操作语义
• 3.4 静态语义
• 3.4.1 RCAL86程序良型性推理规则
• 3.4.2 静态推理规则的可靠性定理
• 3.5 RCAL86下的程序安全性证明
• 3.5.1 分离逻辑
• 3.5.2 分离逻辑的Coq模块
• 3.5.3 Buddy空闲页分配算法
• 3.5.4 程序规范标注
• 3.5.5 安全证明开发
• 3.6 本章小结
• 第四章 一个MIPS认证汇编语言SCAP下的安全代码开发
• 4.1 SCAP的语法和目标机器模型
• 4.1.1 语法
• 4.1.2 操作语义
• 4.1.3 操作语义的Coq表示
• 4.2 SCAP的静态推理规则
• 4.2.1 规范结构
• 4.2.2 推理规则
• 4.2.3 可靠性定理
• 4.3 SCAP下认证的动态存储分配函数库的开发
• 4.3.1 动态存储分配算法
• 4.3.2 程序规范标注
• 4.3.3 安全证明开发
• 4.4 本章小结
• 第五章 机器字位级别抽象的扩展
• 5.1 支持位运算的抽象机器模型
• 5.1.1 机器字的位矢量表示
• 5.1.2 抽象机器模型
• 5.2 位运算的形式化推理
• 5.3 位级别抽象的Coq实现
• 5.4 在SCAP中增加位运算的支持
• 5.5 本章小结
• 第六章 结论
• 6.1 基于逻辑的高可信软件开发方式分析
• 6.1.1 开发效率
• 6.1.2 软件维护
• 6.1.3 对传统软件开发模式的指导意义
• 6.2 相关研究
• 6.2.1 Hoare逻辑和分离逻辑
• 6.2.2 认证汇编编程CAP
• 6.2.3 携带证明的代码PCC
• 6.2.4 类型化汇编语言TAL
• 6.3 未来工作
• 参考文献
• 附录
• 致谢
• 攻读学位期间的主要研究工作和论文发表情况