• 《符号执行研究综述》论文阅读


    读一下《符号执行研究综述》论文~
    符号执行是重要的程序分析方法,为程序测试提供高覆盖率的测试用例,以触发深层的程序错误。

    定义

    符号执行作为一种重要的形式化方法和软件分析技术,采用抽象符号代替程序变量,程序计算的输出被表示为输入符号值的函数,根据程序的语义,遍历程序的执行空间。

    历史

    • 1975,King首次提出符号执行的思想,应用于程序分析。
    • 经历过短暂的研究高潮后,符号执行的研究就陷入了低谷。
    • 十几年间,传统符号执行——>动态符号执行——>选择性符号执行
    • 动态符号执行:(1)混合测试;(2)执行生成测试
    • 符号执行的优势:尽可能少的测试用例集达到高测试覆盖率,从而挖掘出复杂软件程序的深层错误。
    • 符号执行的限制:路径爆炸问题、约束求解困难集内存建模。

    各类符号执行介绍

    经典符合执行

    • 经典符号执行的核心思想是通过使用符号值来代替具体值作为程序输入,并用符号表达式来表示与符号值相关的程序变量的值。
    • 经典符号执行并不真实地执行,而是基于解析程序,通过符号值模拟执行。
    • 经典符合执行是一种静态符号执行。
    • 经典符号执行原理上是可对程序路径进行全覆盖的,可针对每一路径都生成符合该路径的测试用例。

    动态符号执行

    • 动态符号执行结合使用了具体执行符号执行,综合了具体执行和经典符号执行的优点,并出现了混合执行(concolic execution)执行生成测试两种符号执行技术。
    • 混合执行由 Godefroid和 Sen等在2005年提出,Sen阐述了其原理,并总结了近十年改进与发展。
    • 执行生成测试是由 Cadar等于2006年提出的,并在EXE和 KLEE工具中得到了实现。

    混合测试

    混合执行思想:具体输入执行程序,程序运行中,通过程序插桩手段收集路径约束条件,按顺序搜索程序路径,利用约束求解器求解上一执行中收集到的约束集,从而得到下一次执行的测试用例;在下一次执行结束后,按一定的策略选择其中某一分支判断点进行约束取反,得到新的约束集,再用约束求解器对其进行求解,得到下一执行的测试用例.如此反复,避免执行重复路径,以尽可能少的测试集达到高测试覆盖。

    执行生成测试

    • 执行生成测试的混合是在一次程序执行中,对符号变量无关的代码段使用具体执行;而对符号变量相关的代码段进行符号执行,使用符号执行引导测试过程,为每条路径生成一个测试用例,进行一次执行。
    • 执行生成测试的核心思想是通过程序代码自动地生成潜在的高度复杂的测试用例,在用符号输入执行程序的过程中,在分支处将false路径的状态信息记录下来,判断为true的分支继续执行。
    • 与混合测试相比,执行生成测试的优势是能更加系统且高效地得到所有的路径信息以及对应的测试用例,避免重复性搜索过程;
    • 其缺点是内存空间耗费较大,一种解决思路是可以使用多线程的方式代替分支存储,实现对多个分支的同时搜索和测试用例的生成。

    选择性符号执行

    选择性符号执行在指定区域内的符号化搜索,就是完全的符号执行,在该区域之外均使用具体执行完成。

    主要挑战和解决方法

    路径爆炸

    路径爆炸问题是制约符号执行在现实程序分析中应用的主要因素。
    缓解路径爆炸问题的思路主要有以下几种:

    • 采用启发式搜索方法对程序路径空间进行搜索。
    • 冗余路径剪枝。
    • 利用现有的回归测试集确定执行 的 优 先 顺 序。
    • 基于约束的符号执行。

    约束求解

    约束求解是符号执行的基础,符号执行在程序分析上的效率很大程度上取决于约束求解的效率;而约束求解主要依赖于可满足性模理论SMT。
    约束求解突出 的 优 化 思 想:

    • 无关约束消除。
    • 缓存求解策略。
    • 懒约束求解策略。

    主流符号执行工具

    • EXE & KLEE。针对源代码的符号执行分析工具,均出自斯坦福大学的研究团队。
      KLEE 能生成高覆盖率的测试集,在用户级程序中能达到90%的覆盖率,而且在复杂软件中,可以通过交叉检查挖掘到更深层的程序错误。
    • DART,CUTE和jCUTE。
    • angr。二进制分析工具。

    结论

    • 符号执行的发展方向之一是解决:路径空间启发式搜索、约束求解、并行处理问题、内存建模和执行环境仿真等问题。
    • 另一发展方向是与 Fuzzing技术相结合,以提高程序脆弱性检测的能力。
  • 相关阅读:
    STM32定时器笔记
    B+树结构与索引<一> _ 结构与索引
    windows上给oracle打补丁注意事项
    如何求候选码、属性集的闭包
    【Linux升级之路】6_进程间通信
    配置 身份验证 的 Squid代理服务器
    成员变量(实例变量)、局部变量以及静态变量(类变量)的区别与属性,final的使用
    小红书母婴行业文案怎么写,创作方向有哪些?
    【红外DDE算法】HE算法在红外图像可视化上的应用(附源码)
    Android Jetpack学习系列——WorkManager
  • 原文地址:https://blog.csdn.net/qq_43347746/article/details/127453693