基于选择性符号执行的补丁验证
| 摘要 | 第3-4页 |
| ABSTRACT | 第4页 |
| 目录 | 第6-9页 |
| 表格索引 | 第9-10页 |
| 插图索引 | 第10-11页 |
| 主要符号对照表 | 第11-12页 |
| 第一章 绪论 | 第12-20页 |
| 1.1 研究背景 | 第12-15页 |
| 1.1.1 课题的研究意义 | 第12-14页 |
| 1.1.2 国内外研究现状 | 第14-15页 |
| 1.2 研究内容 | 第15-18页 |
| 1.2.1 课题的研究目标 | 第15-16页 |
| 1.2.2 本文的工作 | 第16-18页 |
| 1.3 本文的内容组织 | 第18-20页 |
| 第二章 选择性符号执行技术 | 第20-32页 |
| 2.1 符号执行 | 第20-24页 |
| 2.1.1 基本概念 | 第20-21页 |
| 2.1.2 符号执行工具 | 第21-23页 |
| 2.1.3 工作流程 | 第23-24页 |
| 2.2 KLEE 简介 | 第24-25页 |
| 2.2.1 LLVM 分析框架 | 第24-25页 |
| 2.2.2 KLEE 系统 | 第25页 |
| 2.3 术语简介 | 第25-27页 |
| 2.4 一个典型例子 | 第27页 |
| 2.5 SERAPH 的工作流 | 第27-30页 |
| 2.6 本章小结 | 第30-32页 |
| 第三章 rbscope 的生成 | 第32-48页 |
| 3.1 生成 rbscope 的流程 | 第32-34页 |
| 3.2 关注点配置 | 第34-37页 |
| 3.2.1 入口函数配置 | 第34-35页 |
| 3.2.2 复杂补丁处理 | 第35-37页 |
| 3.3 指向分析 | 第37-38页 |
| 3.3.1 基本概念 | 第37-38页 |
| 3.3.2 Andersen 算法 | 第38页 |
| 3.4 调用图的建立 | 第38-40页 |
| 3.4.1 基本概念 | 第38-39页 |
| 3.4.2 调用图的实现 | 第39-40页 |
| 3.5 基于未被调用函数的削减 | 第40页 |
| 3.6 基于可达性的削减 | 第40-41页 |
| 3.6.1 过程内分析 | 第40页 |
| 3.6.2 过程间可达性 | 第40-41页 |
| 3.6.3 基于可达性的削减 | 第41页 |
| 3.7 基于程序影响性分析的削减 | 第41-43页 |
| 3.8 本章小结 | 第43-48页 |
| 第四章 补丁验证 | 第48-54页 |
| 4.1 单程序的补丁验证 | 第48页 |
| 4.2 交叉验证 | 第48-50页 |
| 4.3 用户提供的上下文初始化 | 第50页 |
| 4.4 本章小结 | 第50-54页 |
| 第五章 实验与评估 | 第54-60页 |
| 5.1 实验流程 | 第54-55页 |
| 5.2 实验介绍 | 第55-57页 |
| 5.3 实验结果 | 第57-59页 |
| 5.4 本章小结 | 第59-60页 |
| 第六章 全文总结 | 第60-62页 |
| 附录 A 前向切片的问题 | 第62-64页 |
| 附录 B LLVM 中间代码的一些特点 | 第64-68页 |
| B.1 控制流和数据流 | 第64-66页 |
| B.2 LLVM opt 的插件机制 | 第66-68页 |
| 附录 C KLEE 的参数配置 | 第68-70页 |
| 参考文献 | 第70-74页 |
| 致谢 | 第74-76页 |
| 攻读学位期间发表的学术论文目录 | 第76-78页 |
| 攻读学位期间参与的项目 | 第78-80页 |
