模块化构造软件系统安全性证明的研究
| 中文摘要 | 第1-7页 |
| 英文摘要 | 第7-15页 |
| 第一章 绪论 | 第15-35页 |
| ·研究背景 | 第15-19页 |
| ·程序与安全 | 第15-16页 |
| ·形式化的程序验证 | 第16-17页 |
| ·信任计算基础 | 第17-18页 |
| ·Curry-Howard同构原理 | 第18-19页 |
| ·携带证明的代码(PCC) | 第19-21页 |
| ·PCC相关的研究 | 第21-31页 |
| ·Touch Stone PCC框架 | 第22-24页 |
| ·基于语义模型的基础PCC框架 | 第24-26页 |
| ·类型化的基础PCC框架 | 第26-28页 |
| ·采用逻辑验证的基础PCC框架 | 第28-29页 |
| ·存在的问题 | 第29-31页 |
| ·本文概述 | 第31-35页 |
| ·研究工作 | 第31-33页 |
| ·主要创新与贡献 | 第33页 |
| ·章节安排 | 第33-35页 |
| 第二章 一个简单的基础PCC框架 | 第35-59页 |
| ·框架概述 | 第35-38页 |
| ·归纳构造演算 | 第38-40页 |
| ·抽象机器模型与汇编程序 | 第40-44页 |
| ·安全策略 | 第44-45页 |
| ·程序验证推理系统 | 第45-54页 |
| ·程序规范 | 第45-46页 |
| ·推理规则 | 第46-48页 |
| ·验证推理系统的可靠性与不变式 | 第48-54页 |
| ·安全性证明与PCC包的构造 | 第54-55页 |
| ·实现 | 第55-59页 |
| 第三章 支持模块化验证的基础PCC框架 | 第59-81页 |
| ·模块定义 | 第60-61页 |
| ·框架概述 | 第61-62页 |
| ·支持验证系统嵌入的推理系统(OCAP) | 第62-74页 |
| ·OCAP规范定义 | 第62-64页 |
| ·OCAP推理规则 | 第64-69页 |
| ·OCAP的可靠性证明 | 第69-74页 |
| ·在OCAP中嵌入CAP | 第74-78页 |
| ·模块链接 | 第78-79页 |
| ·实现 | 第79-81页 |
| 第四章 支持栈式推理的验证系统(SCAP) | 第81-101页 |
| ·SCAP验证推理系统 | 第82-88页 |
| ·规范结构 | 第82-83页 |
| ·推理规则 | 第83-88页 |
| ·SCAP验证条件产生器 | 第88-91页 |
| ·验证条件产生函数 | 第88-90页 |
| ·验证条件产生函数的可靠性 | 第90-91页 |
| ·分离逻辑 | 第91-93页 |
| ·一个动态内存分配模块newpair | 第93-95页 |
| ·在OCAP中嵌入SCAP | 第95-97页 |
| ·实现 | 第97-101页 |
| 第五章 类型化的验证系统(TALP) | 第101-125页 |
| ·TALP类型系统 | 第102-109页 |
| ·TALP类型系统 | 第103-104页 |
| ·TALP定型规则 | 第104-109页 |
| ·TALP类型检查器 | 第109-115页 |
| ·定型规则检查函数 | 第109-110页 |
| ·合一算法 | 第110-114页 |
| ·类型检查器及其可靠性证明 | 第114-115页 |
| ·一个调用内存分配的模块main | 第115-117页 |
| ·在OCAP中嵌入TALP | 第117-118页 |
| ·链接main模块与newpair模块 | 第118-121页 |
| ·main模块 | 第119页 |
| ·newpair模块 | 第119页 |
| ·链接并产生安全性证明 | 第119-121页 |
| ·实现 | 第121-125页 |
| 第六章 结束语 | 第125-129页 |
| ·论文工作总结 | 第125-126页 |
| ·未来的研究方向 | 第126-129页 |
| 参考文献 | 第129-137页 |
| 致谢 | 第137-139页 |
| 攻读学位期间发表的学术论文 | 第139页 |
