基于符号执行的代码安全检查技术研究与实现

摘要

代码安全缺陷一直是困扰IT产业发展的一颗绊脚石，究其缘由主要是安全缺陷检查的成本高，效率低下。目前主要靠手工或者工具两种方式来应对此问题，人工的效率比较低，靠工具来检查是时下比较热门的话题，我们一般把代码安全缺陷检查工具分为两类：一类是使用传统静态分析的工具，另一种是使用动态测试的工具。符号执行是一种程序分析的技术，它主要靠收集符号的约束信息，再利用约束求解器求解来得到测试用例，理论上能够覆盖全部的路径。本论文的主要工作如下：
　　（1）针对符号执行中路径指数爆炸问题，提出基于 CFG（Control Flow Graph）的执行状态选择算法。该算法利用静态分析提取出所需的CFG，然后在此基础上结合执行状态的权值产生一种新的执行状态选择算法，可以在路径爆炸时覆盖更多的路径；
　　（2）利用无用函数分析的思想来优化动态符号执行。无用函数分析是本文提到的一种静态分析方法，分为两个阶段：第一阶段是死代码消除，第二阶段是无用函数消除，通过这两个阶段消除不必要分析的代码，以此达到优化的目的；
　　（3）提出基于数组模型的改进设计，将数组模型用树表示，便于内存安全的检测。同时，针对数组模型不能处理大小不确定类型的数据做了改进，使得改进之后的内存模型能够处理大小不确定类型的数据；
　　（4）在上述内容的基础之上实现了一个简易的动态符号执行的代码安全缺陷检查工具，该工具能够检查内存越界、二次释放、野指针访问、内存泄露、加法溢出、除零等错误；
　　（5）分别针对整个系统、无用函数分析优化以及执行状态选择算法做了实验分析，实验充分表明了本文实现的工具的有效性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 研究背景

1.2 研究的目的和意义

1.3 符号执行研究现状

1.4相关技术和研究

1.5研究内容

1.6 组织结构

第二章 符号执行概述

2.1 符号执行简介

2.2 约束求解器简介

2.3 符号执行面临的挑战

2.4 本章小结

第三章 动态符号执行的优化研究

3.1 缓解路径爆炸的优化

3.2 基于无用函数分析的优化

3.3 内存模型的改进

3.4 本章小结

第四章 系统实现

4.1 总体架构

4.2 bitcode优化模块

4.3 语义解释器模块

4.4 执行状态选择模块

4.5 内存模型模块

4.6 安全缺陷检查模块

4.7 本章小结

第五章 实验与结论

5.1 实验说明

5.2 实验环境

5.3 安全缺陷检查实验

5.4 无用函数分析实验

5.5 执行状态选择算法实验

5.6 实验总结

第六章 总结与展望

6.1 本文总结

6.2 展望

致谢

参考文献

攻读硕士期间的研究成果