| 摘要 | 第1-5页 |
| Abstract | 第5-11页 |
| 第一章 背景介绍 | 第11-27页 |
| ·基本概念 | 第11-13页 |
| ·程序的安全属性 | 第11-12页 |
| ·信任计算基 | 第12页 |
| ·规范语言的表达能力 | 第12-13页 |
| ·Curry-Howard同构 | 第13-14页 |
| ·Hoare逻辑 | 第14-15页 |
| ·类型系统 | 第15-20页 |
| ·类型化高级语言 | 第16-18页 |
| ·类型化汇编语言 | 第18-20页 |
| ·传统的携带证明的代码 | 第20-24页 |
| ·基于语义的基础携带证明的代码FPCC | 第22-23页 |
| ·基于语法的FPCC | 第23-24页 |
| ·本文的内容 | 第24-27页 |
| 第二章 程序规范语言GALLINA和定理证明工具Coq | 第27-35页 |
| ·项语法 | 第27-29页 |
| ·GALLINA的命令语言Vernacular | 第29-31页 |
| ·使用Coq描述程序规范 | 第31-32页 |
| ·Coq的交互式定理证明 | 第32-34页 |
| ·本节小结 | 第34-35页 |
| 第三章 一个简单的支持函数调用返回的认证汇编语言RCAL86 | 第35-59页 |
| ·引言 | 第35-37页 |
| ·RCAL86的设计目标 | 第37-38页 |
| ·目标机器和操作语义 | 第38-41页 |
| ·RCAL86的抽象存储模型 | 第38页 |
| ·RCAL86的操作语义 | 第38-41页 |
| ·静态语义 | 第41-45页 |
| ·RCAL86程序良型性推理规则 | 第41-43页 |
| ·静态推理规则的可靠性定理 | 第43-45页 |
| ·RCAL86下的程序安全性证明 | 第45-58页 |
| ·分离逻辑 | 第45-47页 |
| ·分离逻辑的Coq模块 | 第47-53页 |
| ·Buddy空闲页分配算法 | 第53-55页 |
| ·程序规范标注 | 第55-56页 |
| ·安全证明开发 | 第56-58页 |
| ·本章小结 | 第58-59页 |
| 第四章 一个MIPS认证汇编语言SCAP下的安全代码开发 | 第59-83页 |
| ·SCAP的语法和目标机器模型 | 第60-65页 |
| ·语法 | 第60-61页 |
| ·操作语义 | 第61-63页 |
| ·操作语义的Coq表示 | 第63-65页 |
| ·SCAP的静态推理规则 | 第65-72页 |
| ·规范结构 | 第66-67页 |
| ·推理规则 | 第67-70页 |
| ·可靠性定理 | 第70-72页 |
| ·SCAP下认证的动态存储分配函数库的开发 | 第72-81页 |
| ·动态存储分配算法 | 第72-74页 |
| ·程序规范标注 | 第74-79页 |
| ·安全证明开发 | 第79-81页 |
| ·本章小结 | 第81-83页 |
| 第五章 机器字位级别抽象的扩展 | 第83-93页 |
| ·支持位运算的抽象机器模型 | 第83-88页 |
| ·机器字的位矢量表示 | 第83-87页 |
| ·抽象机器模型 | 第87-88页 |
| ·位运算的形式化推理 | 第88-90页 |
| ·位级别抽象的Coq实现 | 第90-92页 |
| ·在SCAP中增加位运算的支持 | 第92页 |
| ·本章小结 | 第92-93页 |
| 第六章 结论 | 第93-101页 |
| ·基于逻辑的高可信软件开发方式分析 | 第93-96页 |
| ·开发效率 | 第93-95页 |
| ·软件维护 | 第95页 |
| ·对传统软件开发模式的指导意义 | 第95-96页 |
| ·相关研究 | 第96-98页 |
| ·Hoare逻辑和分离逻辑 | 第96-97页 |
| ·认证汇编编程CAP | 第97页 |
| ·携带证明的代码PCC | 第97-98页 |
| ·类型化汇编语言TAL | 第98页 |
| ·未来工作 | 第98-101页 |
| 参考文献 | 第101-109页 |
| 附录 | 第109-111页 |
| 致谢 | 第111-113页 |
| 攻读学位期间的主要研究工作和论文发表情况 | 第113-114页 |
