基于逻辑的程序验证方法在高可信软件开发上的应用
发布时间：2023-02-08 10:29
随着软件规模的越来越大，软件的安全越来越引起软件开发人员的关注，而现有的编程语言以及软件开发方法所能提供的安全保证是脆弱和不可靠的，例如通过标准的软件工程方法和大量的测试减少软件漏洞的发生，但是即使经过高强度测试的软件，也不能保证它没有漏洞，另外一方面，对一个漏洞的修复也往往会引起新的漏洞。可以说，现有的软件工程方法对软件安全的提高已经越来越微弱。而基于语言的程序验证方法能为软件安全提供可靠的保证。 基于语言的程序验证方法通过对程序设计语言添加静态的类型以及规范结构，使得用这种语言写出的良形式程序是安全的。现有的关于认证代码技术以及类型系统方面的研究已经能够验证低级语言和高级语言程序的多种安全属性。例如，当前的大部分程序设计语言都有一个类型系统，它一般用于检查程序的一些简单语义错误，可靠的类型系统可以以较低的代价保证程序的一些基本安全属性。安全的高级语言和通用中间层语言的类型系统的研究已经对安全计算做了有意义的贡献，但是用这些语言写就的安全程序还需经过多步的未经编译和优化才能在最终的硬件上运行，这使得最终运行的代码是未经验证的。基于这个原因，很多工作转向研究低级代码的验证，特别...
【文章页数】：114 页
【学位级别】：博士
【文章目录】：
摘要
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 未来工作
参考文献
附录
致谢
攻读学位期间的主要研究工作和论文发表情况
本文编号：3737844
【文章页数】：114 页
【学位级别】：博士
【文章目录】：
摘要
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 未来工作
参考文献
附录
致谢
攻读学位期间的主要研究工作和论文发表情况
本文编号：3737844
本文链接：https://www.wllwen.com/shekelunwen/ljx/3737844.html