| 摘要 | 第5-6页 |
| abstract | 第6-7页 |
| 第1章 绪论 | 第10-17页 |
| 1.1 研究背景和意义 | 第10-12页 |
| 1.1.1 研究背景 | 第10页 |
| 1.1.2 研究意义 | 第10-12页 |
| 1.2 安全缺陷与漏洞的概念 | 第12页 |
| 1.2.1 安全缺陷 | 第12页 |
| 1.2.2 漏洞 | 第12页 |
| 1.3 国内外研究现状 | 第12-15页 |
| 1.3.1 开源软件漏洞检测方面的研究 | 第12-14页 |
| 1.3.2 模型检测的发展历程 | 第14-15页 |
| 1.4 论文研究内容以及组织结构 | 第15-17页 |
| 第2章 模型检测理论及技术研究 | 第17-28页 |
| 2.1 模型检测技术基本概念 | 第17-22页 |
| 2.1.1 基础概念 | 第17-18页 |
| 2.1.2 Kripke结构 | 第18-20页 |
| 2.1.3 时序逻辑 | 第20-22页 |
| 2.2 模型检测经典算法 | 第22-26页 |
| 2.2.1 CTL模型检测算法 | 第22-24页 |
| 2.2.2 LTL模型检测算法 | 第24页 |
| 2.2.3 符号化模型检测算法 | 第24-26页 |
| 2.2.4 其他算法 | 第26页 |
| 2.3 模型检测常用工具 | 第26-27页 |
| 2.4 本章小结 | 第27-28页 |
| 第3章 模型检测在开源软件漏洞检测中的应用研究 | 第28-37页 |
| 3.1 针对源代码的模型检测技术研究 | 第28-29页 |
| 3.2 条件模型检测在源代码漏洞检测上的应用方法 | 第29-35页 |
| 3.2.1 条件模型检测概念 | 第29-32页 |
| 3.2.2 条件模型检测理论基础 | 第32-34页 |
| 3.2.3 条件模型检测建模过程 | 第34-35页 |
| 3.3 条件模型检测的实施原理 | 第35-36页 |
| 3.4 本章小结 | 第36-37页 |
| 第4章 CPAChecker模型检测工具的深入分析 | 第37-47页 |
| 4.1 CPAChecker介绍及其功能 | 第37-39页 |
| 4.1.1 CPAChecker的出现 | 第37-38页 |
| 4.1.2 CPAChecker的功能 | 第38-39页 |
| 4.2 CPAChecker体系结构 | 第39-43页 |
| 4.2.1 CPAChecker逻辑结构 | 第40-41页 |
| 4.2.2 CPAChecker目录结构 | 第41-43页 |
| 4.3 CPAChecker主要算法分析 | 第43-46页 |
| 4.4 本章小结 | 第46-47页 |
| 第5章 条件模型检测在开源软件漏洞检测上的应用 | 第47-60页 |
| 5.1 条件模型检测应用准备阶段 | 第47-52页 |
| 5.1.1 检测对象的选择 | 第47-48页 |
| 5.1.2 开源软件Tomcat的介绍 | 第48-49页 |
| 5.1.3 Tomcat编译过程 | 第49-52页 |
| 5.2 详细检测过程及结果分析 | 第52-59页 |
| 5.2.1 建模过程 | 第52-55页 |
| 5.2.2 设置规范 | 第55页 |
| 5.2.3 执行条件模型检测 | 第55-58页 |
| 5.2.4 实施情况总结 | 第58-59页 |
| 5.3 本章小结 | 第59-60页 |
| 结论 | 第60-61页 |
| 参考文献 | 第61-65页 |
| 致谢 | 第65页 |