中文译名:信标: 具有可证明路径剪枝的定向灰盒模糊测试
作者:Huang Heqing
单位:香港科技大学
国家: #中国
年份: #2022年
来源: #SP
关键字: #定向fuzzing
代码地址: https://hub.docker.com/r/yguoaz/beacon
笔记建立时间: 2023-05-09 17:27
摘要
- 当前的定向 fuzzer 不够高效,因为它们符号化或者具体的执行了很多不会到达 target code 到的 path,浪费了很多计算资源
- beacon——通过一种可证明的方式在路径之海中引导灰盒模糊测试
- 轻量级的静态分析——用于计算到达目标的先决条件——用于修剪无法到达 target 的路径
引言
- 传统模糊测试应用于
- 检测漏洞路径
- 生成潜在漏洞的 poc
- 崩溃复现
- 追踪信息流
- 定向 fuzzing 现状
- 定向白盒模糊器依靠符号执行,通过求解路径约束来确定可达性,旨在为生成能够到达目标的输入提供理论保证。因此,它们对符号执行的固有使用从根本上限制了它们的扩展能力。
- 定向灰盒模糊器通常不考虑拒绝不可达路径。它们依靠从执行反馈中收集的启发式方法,根据到达目标代码的可能性对种子进行优先排序。他们要么使用轻量级的元启发式,例如,到目标的距离,要么使用机器学习技术来预测可达性,但不能保证这种优先级会导致拒绝任何不可行的路径。因此,在 AFLGo 中提到的24小时实验中,95%以上的输入无法到达给定的程序点。
- 定向 fuzzing 的关键在于尽可能早的剔除不能到达 target 的执行路径
- BEACON
- 耗费低的静态分析计算程序变量的合理近似值,这些值用于决定某条路径是否可以到达 target
- 为了使得静态分析精确又高效,采用了两种新的优化方法:关系保持和有界析取
- 基于此对模糊测试中要执行的路径进行修剪(作者称可以达到 80%以上的修剪)
- 在路径遇到控制流图上不能到达目标的指令时,直接对路径进行剪枝
- 可到达目标但路径条件不满足的路径进行剪枝
- 耗费低的静态分析计算程序变量的合理近似值,这些值用于决定某条路径是否可以到达 target
- 提高:
- BEACON 平均可以早期拒绝82.94%的路径
- 与传统的定向模糊器相比,速度提高了11.50倍
- 对于 AFL、afl++和 Mopt 等 fuzzers, BEACON 可以分别加速6.31倍、11.86倍和10.92倍来重现目标 bug
- BEACON 发现了14个不完整的修复和8个新 bug
概述
- 输入为程序源代码和模糊测试目标
- 首先进行可达性分析,剔除无法到达任何目标的路径
- 进行反向区间分析
- 因为选择了区间域作为先决条件的抽象,损失了精确度,所以采用以下两种优化方法
- 关系保持——保留计算式类的约束条件
- 边界提取——设定阈值,超过阈值才合并路径
- 有选择性的插桩
- 在 BEACON 中,我们检测两种语句: 变量定义语句和分支语句
- 插桩用于修剪路径
方法
预备工作
作者给出了一个语言简化表示的语法
转换规则
Backward Interval Analysis
以图二为例,用该算法进行分析,从 18 行开始向上反向分析,初始的后置条件是 true,当分析到第 9 行时,碰到了第一个分支, 此时的先验条件分裂为两条,分别是:
在实际分析中可能会分裂为许多条,进行求解非常复杂,同时还需要在 18 行进行合并,还会丢失一定的精度。
为了提高效率,我们建议使用区间抽象来支持路径条件的轻量级推理和反向路径的合理过度逼近。(算法 7-18 行)
经过合并后的 pc 1 和 pc 2 如下图:
综上,我们可以看到后向间隔分析负责得到一个合理逼近的 target 的先验条件
Optimizations for Maintaining Precision
Relationship Preservation
- 我们设计了如图5所示的推断规则来执行间隔抽象。
- 与传统的区间分析不同,我们的分析不仅跟踪变量的区间,还跟踪路径条件中出现的表达式。
使用这些规则来分析 pc 2,与传统的分析的区别如下图所示
可以看到分析结果要比传统的区间分析精度更高。
Bounded Disjunctions
- 当路径数量小于阈值的时候,不进行合并,保留了精度
- 当路径大于阈值的时候,就需要合并,合并就意味着要丢失精度,
- 上图的 AB 合并,就会损失中间部分的精度,下面 AB 合并不会有精度损失
- 依照上述公式进行计算损失,哪个合并损失少,就合并哪两个路径
- 例子
Precondition Instrumentation
- 我们首先将程序转换为 SSA 形式[42],并且只考虑变量定义作为插装的候选程序位置。这是正确的,因为 SSA 表单保证变量在定义之后不会被写入。
- 当变量 v1的值仅依赖于另一个变量 v2时,不应该检测 v1。这些信息可以通过定义数据流分析来计算[43]。例如,在图2中,v 仅依赖于 u 而不是 x 或 z。
评价
实现
- 基于LLVM实现执行先决条件分析、检查先决条件的检测和其他与覆盖率相关的检测,输出可执行的二进制文件
- 使用AFLGo作为模糊测试引擎
Compared to the State of the Art
- 和AFLGo比较
- BEACON分别在Binutils、Ming和Lrzip中检测到3个、9个和2个不完整的补丁,以及8个额外的bug,而AFLGo只检测到6个不完整的补丁。
- 对于那些可在AFLGo中重现的漏洞,BEACON需要较少的覆盖率 (平均91.2%)
- 在某些场景下,特别是在AFLGo无法重现漏洞的情况下,BEACON可以实现更高的覆盖率。
- 和Hawkeye比较
- BEACON对所有漏洞的再现均优于AFLGo和Hawkeye,且p值均小于0.05。特别是对于CVE-2016-4491和CVE-20166131, BEACON相比Hawkeye可以实现3.6倍和5.7倍的加速。
- 和AFL, AFL++, and Mopt比较
- 与原始工具相比,AFL+BEACON AFL++ BEACON和Mopt+BEACON分别可以实现6.31倍、11.86倍和10.92倍的加速。
路径切片的影响与前提条件检查
在重现漏洞方面,BEACON比BEACON*要快得多 (1.1倍到18.4倍),因为它平均比BEACON多修剪29.1%的路径。在某些情况下 (例如,CVE-2017-8397), BEACON *甚至无法在120小时内重现漏洞。这一结果证明了前置条件分析的重要性和必要性,使我们的性能得到了显著的提高。
关系保持与有界析取的影响
在重现漏洞时,BEACON比BEACON-rp和BEACON-bd分别快得多 (1.05倍到4.9倍,1.05倍到5.34倍)。这一结果证明了这两种策略的重要性和必要性,因为它们都有助于前提条件分析的精度,它们的组合可以使我们在模糊测试中获得更高的精度并修剪更多的路径。
当绑定阈值从5增加到50时,执行过滤率从0.9%略微提高到3.2%。然而,时间成本急剧增加,甚至耗尽了服务器内存。因此,BEACON使用5作为阈值,以获得效率和有效性的最佳点。
插桩开销
其中显示了每个程序的执行次数 (Nexec)、原始时间成本 (Torig)和插装后的时间成本 (TBeacon)。我们观察到,BEACON引入了高达9.8%的运行时开销,平均为5.7%。我们认为这样低的开销在实践中是可以接受的,并且之前的评估表明BEACON比现有的模糊器要快得多。
相关工作
定向白盒fuzzing
- Klee[49],以生成可利用的输入,用于漏洞复现
- 然而,路径爆炸问题和众所周知的昂贵约束求解使得它们难以扩展到现实世界的程序中。
- 现有的工作试图利用对漏洞的先验知识,使符号执行专注于相关的程序状态。一个方向是优先考虑程序路径,以供符号执行探索。例如,Hercules[50]使用了一个不健全的函数摘要来确定可达路径的优先级。其他人要么依赖bug报告[51]、关键系统调用[10],要么依赖补丁中的变化[52]来识别潜在的bug踪迹。然而,这些工作通常需要手工专业知识来确保这些先验知识的质量,这可能导致不同程序的不同表现。另一个方向是加速符号执行本身,以便更快地接近目标。例如,现有的作品通过快照机制象征性地[53]或具体地[54]保留执行状态,以避免冗余的路径探索。Chopper[55]采用在线静态分析来提供状态合并策略,同时最小化动态分析路径的数量。DiSE[56]识别分支条件之间的关系,并逐步解决它们。
覆盖引导fuzzing
- 可以通过动态污染分析来优化输入生成。其基本思想是改变相关的输入偏移量以满足未覆盖的分支条件。
- Angora[57]采用字节级污染跟踪来发现目标条件的相关输入字节,然后应用基于梯度下降的搜索策略。
- 为了使基于梯度下降的搜索更加合理,Neuzz[58]提出使用神经网络平滑搜索过程。
- 还有一些技术涉及轻量级程序分析和转换,以提高突变的有效性。Fairfuzz[59]识别了不需要改变值的输入偏移量,因此,最小化输入搜索空间提高了突变的效率。Mopt[13]提出了一种新的突变算子调度策略来调整不同程序的突变策略。
- 将模糊器与集合/符号执行相结合,即混合模糊,用于解决复杂和严格的路径约束。
- Driller[60]提出解决那些未发现的路径进行模糊化,而不是用集合执行来探索所有路径。然而,如何有效地将协同执行与模糊测试相结合一直是人们关注的问题。
- QSYM[61]解决了基种子的部分路径约束,并对满足实际条件的验证输入利用了突变。
- Intriguer[62]进一步用动态污染分析取代符号仿真,这减少了建模大量类移动指令的开销。
- Pangolin[63]建议将约束保留为抽象,并重用它来指导进一步的输入生成。