编译过程安全性基础研究
| 摘要 | 第1-7页 |
| ABSTRACT | 第7-9页 |
| 目录 | 第9-13页 |
| 图表目录 | 第13-15页 |
| 表格目录 | 第15-16页 |
| 第1章 绪论 | 第16-29页 |
| ·安全软件开发 | 第16-17页 |
| ·编译器的构造及其安全验证问题 | 第17-22页 |
| ·编译器的工作流程 | 第18-22页 |
| ·编译器实现方法 | 第22页 |
| ·编译安全验证问题的提出 | 第22页 |
| ·程序的安全属性建模以及分析 | 第22-24页 |
| ·程序属性描述 | 第23页 |
| ·程序属性分析 | 第23-24页 |
| ·编译过程验证技术 | 第24-26页 |
| ·编译正确性的概念 | 第24-25页 |
| ·编译安全性验证 | 第25页 |
| ·编译优化验证 | 第25-26页 |
| ·论文工作与组织 | 第26-29页 |
| 第2章 编译验证技术 | 第29-52页 |
| ·引言 | 第29-30页 |
| ·编译验证的理论基础 | 第30-31页 |
| ·程序语义学 | 第30-31页 |
| ·语义等价性定义及其证明方法 | 第31页 |
| ·编译验证研究内容与背景分析 | 第31-33页 |
| ·编译验证的方法分类 | 第31-32页 |
| ·编译验证研究背景分析 | 第32-33页 |
| ·程序属性描述方法研究 | 第33-51页 |
| ·基于类型精化的内存安全属性描述研究 | 第33-40页 |
| ·信息流安全属性表示研究 | 第40-51页 |
| ·小结 | 第51-52页 |
| 第3章 编译正确性验证研究 | 第52-73页 |
| ·引言 | 第52页 |
| ·语法解析算法的正确性验证研究 | 第52-54页 |
| ·语法解析算法的实现方法概述 | 第52页 |
| ·Parser正确性验证方案 | 第52-53页 |
| ·验证实例分析 | 第53-54页 |
| ·实验分析 | 第54页 |
| ·代码生成算法的正确性验证方法研究 | 第54-57页 |
| ·代码生成算法原理简介 | 第54-55页 |
| ·验证方法 | 第55-56页 |
| ·实验分析 | 第56-57页 |
| ·基于属性文法的编译优化验证研究 | 第57-61页 |
| ·编译优化实现概述 | 第57-59页 |
| ·属性文法简介 | 第59页 |
| ·针对CFG的属性文法拓展 | 第59-60页 |
| ·基于LCFG的属性描述生成 | 第60-61页 |
| ·实验 | 第61页 |
| ·基于SSA的寄存器分配算法研究 | 第61-70页 |
| ·SSA语法和语义 | 第62-64页 |
| ·寄存器分配算法简介 | 第64页 |
| ·基于SSA表示的寄存器分配方案 | 第64-66页 |
| ·寄存器分配算法的形式化描述 | 第66-68页 |
| ·寄存器分配算法实现的正确性验证 | 第68-70页 |
| ·基于SSA的代码生成方法的讨论 | 第70页 |
| ·实验 | 第70-72页 |
| ·小结 | 第72-73页 |
| 第4章 基于程序分析的编译验证框架设计 | 第73-83页 |
| ·引言 | 第73页 |
| ·SUIF编译框架简介 | 第73-74页 |
| ·验证框架的设计 | 第74-78页 |
| ·总体结构 | 第74-75页 |
| ·重要模块说明 | 第75-78页 |
| ·自定义的程序检查模式描述语言CPDL | 第78-79页 |
| ·描述语言语法 | 第78页 |
| ·自定义分析的实例分析 | 第78-79页 |
| ·分析模块采用的基本分析算法 | 第79-80页 |
| ·编译验证框架的工作流程 | 第80-81页 |
| ·源程序属性检查 | 第80-81页 |
| ·编译变换的过程的正确性检查 | 第81页 |
| ·本章小结 | 第81-83页 |
| 第5章 程序安全属性分析方法研究 | 第83-96页 |
| ·引言 | 第83页 |
| ·TC与MC的混合式属性分析方法 | 第83-87页 |
| ·单一分析方法的缺点 | 第84页 |
| ·MC算法原理 | 第84-86页 |
| ·TCMC算法 | 第86页 |
| ·TCMC算法的反例的意义 | 第86-87页 |
| ·基于TCMC算法的内存安全性分析 | 第87页 |
| ·基于TCMC算法的内存泄漏检测方案 | 第87-93页 |
| ·内存泄漏概述 | 第87-88页 |
| ·内存泄漏检测算法 | 第88-90页 |
| ·实例分析 | 第90-93页 |
| ·基于TCMC算法的信息流安全分析方案 | 第93-94页 |
| ·信息流安全标注方法 | 第93页 |
| ·安全类型的传播 | 第93页 |
| ·实例分析 | 第93-94页 |
| ·实验 | 第94-95页 |
| ·本章小结 | 第95-96页 |
| 第6章 二进制代码分析框架研究 | 第96-108页 |
| ·引言 | 第96页 |
| ·机器代码分析 | 第96-106页 |
| ·可重定向的二进制代码分析工具设计 | 第96-98页 |
| ·机器语言语义描述MSSL | 第98-101页 |
| ·机器无关的RTL中间语言 | 第101页 |
| ·控制流信息的恢复 | 第101-105页 |
| ·SSA变换 | 第105页 |
| ·类型分析 | 第105-106页 |
| ·二进制分析工具在编译验证框架中的应用 | 第106页 |
| ·讨论 | 第106页 |
| ·小结 | 第106-108页 |
| 第7章 实验分析 | 第108-112页 |
| ·基本实验数据 | 第108-110页 |
| ·编译安全性分析 | 第110-111页 |
| ·小结 | 第111-112页 |
| 第8章 结束语 | 第112-115页 |
| 参考文献 | 第115-124页 |
| 攻读学位期间发表的学术论文目录 | 第124-125页 |
| 作者在读博士期间从事的科研项目 | 第125-126页 |
| 致谢 | 第126页 |
