汇编指针程序安全性验证的研究
| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 第1章 绪论 | 第11-26页 |
| ·研究背景 | 第11-14页 |
| ·软件安全 | 第11-12页 |
| ·形式验证 | 第12-13页 |
| ·受信任计算基础 | 第13-14页 |
| ·相关研究分析和比较 | 第14-22页 |
| ·Hoare逻辑 | 第14-15页 |
| ·类型化汇编语言 | 第15-16页 |
| ·携带证明代码 | 第16-18页 |
| ·验证汇编编程 | 第18-19页 |
| ·应用类型系统 | 第19-20页 |
| ·分离逻辑 | 第20-21页 |
| ·指针逻辑 | 第21-22页 |
| ·存在的问题和发展方向 | 第22-23页 |
| ·本文概述 | 第23-26页 |
| ·研究工作 | 第24-25页 |
| ·特色和贡献 | 第25页 |
| ·章节安排 | 第25-26页 |
| 第2章 安全程序的设计和证明框架 | 第26-41页 |
| ·安全程序开发框架和出具证明的编译器 | 第26-31页 |
| ·传统软件开发框架 | 第26-27页 |
| ·安全软件开发框架 | 第27-31页 |
| ·源级程序设计与验证系统 | 第31-40页 |
| ·PointerC语言简介 | 第31-33页 |
| ·源级指针逻辑 | 第33-37页 |
| ·源级验证系统 | 第37-40页 |
| ·汇编级验证系统 | 第40页 |
| ·本章小结 | 第40-41页 |
| 第3章 一个x86汇编程序验证框架 | 第41-71页 |
| ·引言 | 第41-43页 |
| ·机器模型和操作语义 | 第43-48页 |
| ·汇编程序验证框架 | 第48-61页 |
| ·断言与规范语言 | 第48-50页 |
| ·合式公式 | 第50页 |
| ·推理规则 | 第50-54页 |
| ·可靠性证明 | 第54-61页 |
| ·Coq实现 | 第61-69页 |
| ·基础逻辑CiC | 第61-63页 |
| ·证明辅助工具Coq | 第63-65页 |
| ·机器模型 | 第65-67页 |
| ·推理规则和可靠性定理 | 第67-69页 |
| ·相关工作 | 第69-70页 |
| ·本章小节 | 第70-71页 |
| 第4章 用于汇编指针程序安全性验证的指针逻辑 | 第71-102页 |
| ·概述 | 第71-72页 |
| ·汇编级指针逻辑 | 第72-95页 |
| ·机器模型 | 第72-73页 |
| ·基本定义 | 第73-75页 |
| ·断言语言 | 第75-78页 |
| ·推理规则 | 第78-93页 |
| ·可靠性证明 | 第93-95页 |
| ·Coq实现 | 第95-98页 |
| ·本章小结 | 第98-102页 |
| ·相关工作 | 第98-100页 |
| ·和PointerC指针逻辑比较 | 第100-101页 |
| ·小节 | 第101-102页 |
| 第5章 汇编级验证原型系统 | 第102-108页 |
| ·原型系统构成 | 第102-105页 |
| ·汇编级验证原型系统 | 第105-106页 |
| ·实验结果 | 第106-107页 |
| ·本章小结 | 第107-108页 |
| 第6章 结束语 | 第108-111页 |
| ·论文工作总结 | 第108-110页 |
| ·进一步的工作 | 第110-111页 |
| 参考文献 | 第111-117页 |
| 致谢 | 第117-119页 |
| 在读期间发表的学术论文与取得的研究成果 | 第119-120页 |
