摘要 | 第4-5页 |
ABSTRACT | 第5-6页 |
第一章 绪论 | 第9-15页 |
1.1 研究背景和意义 | 第9-10页 |
1.2 国内外研究现状 | 第10-12页 |
1.3 论文主要研究内容 | 第12-13页 |
1.4 论文章节安排 | 第13-15页 |
第二章 相关平台及技术研究 | 第15-23页 |
2.1 GCC编译器 | 第15-17页 |
2.1.1 抽象语法树 | 第16-17页 |
2.2 基于缺陷模式的静态分析 | 第17-19页 |
2.2.1 软件的缺陷模式 | 第17-18页 |
2.2.2 静态分析技术 | 第18-19页 |
2.2.3 基于缺陷模式的静态分析技术的优缺点 | 第19页 |
2.3 符号执行技术 | 第19-21页 |
2.3.1 符号执行原理 | 第19-20页 |
2.3.2 静态符号执行 | 第20-21页 |
2.4 本章小结 | 第21-23页 |
第三章 ABAZER-SE的设计 | 第23-31页 |
3.1 研制动机 | 第23-24页 |
3.2 ABAZER-SE框架和分析流程设计 | 第24-27页 |
3.2.1 ABAZER简介 | 第24-25页 |
3.2.2 ABAZER-SE框架 | 第25-26页 |
3.2.3 ABAZER-SE符号化分析流程 | 第26-27页 |
3.3 核心算法设计 | 第27-30页 |
3.3.1 符号执行路径探索算法 | 第27-29页 |
3.3.2 语句分析算法 | 第29-30页 |
3.4 本章小结 | 第30-31页 |
第四章 ABAZER-SE的实现 | 第31-43页 |
4.1 关键数据结构 | 第31-33页 |
4.2 符号执行的语句分析 | 第33-40页 |
4.2.1 内存模型的构建及使用 | 第34-36页 |
4.2.2 指令的语义模拟 | 第36-40页 |
4.2.3 库函数建模 | 第40页 |
4.3 约束求解 | 第40-41页 |
4.4 不确定性内存地址的处理 | 第41-42页 |
4.5 本章小结 | 第42-43页 |
第五章 ABAZER-SE的实验评估 | 第43-56页 |
5.1 实验基准 | 第43-44页 |
5.2 检测的缺陷类型 | 第44-48页 |
5.2.1 时序性逻辑缺陷 | 第44-45页 |
5.2.2 零除数错误 | 第45页 |
5.2.3 数组越界 | 第45-46页 |
5.2.4 未初始化变量使用 | 第46-47页 |
5.2.5 缓冲区溢出缺陷 | 第47页 |
5.2.6 指针双重释放 | 第47-48页 |
5.3 ABAZER-SE与ABAZER实验结果对比 | 第48-51页 |
5.3.1 不可达路径裁剪 | 第48-50页 |
5.3.2 实际代码测试 | 第50-51页 |
5.4 ABAZER-SE与CPPCHECK、KLEE的比较 | 第51-55页 |
5.5 本章小结 | 第55-56页 |
第六章 总结与展望 | 第56-58页 |
6.1 论文总结 | 第56页 |
6.2 未来展望 | 第56-58页 |
参考文献 | 第58-62页 |
致谢 | 第62-63页 |
攻读学位期间发表的学术论文 | 第63页 |