SP22 BEACON ：Directed Grey-Box Fuzzing with Provable Path Pruning

源码：https://hub.docker.com/r/yguoaz/beacon.
作者：huangheqing 香港科技大学网络安全实验室
历史作品：Pangolin: Incremental Hybrid Fuzzing via Polyhedral Path Abstraction S&P’20

背景：

定向模糊测试旨在测试程序的特定部分。定向模糊测试的实用性在于尽早拒绝不可达的执行路径。

问题：

现有的定向模糊器都存在不可行路径爆炸问题（infeasible-path-explosion）

研究现状：

•定向白盒模糊测试使用的符号执行从根本上限制了它们的扩展能力。定向白盒模糊测试被证明不能在24小时内重现漏洞。
•定向灰盒模糊测试一般不考虑拒绝不可达路径。AFLGo中提到的24小时实验中95%以上的输入无法到达给定的程序点。

挑战

中间程序状态是作为最弱前提条件(也称为必要前提条件)的近似来计算的，静态分析的挑战在于：很难同时是精确和高效的。现有的研究经常在精确度和速度之间做出折衷。

复杂条件求解开销大：14和17行条件（z<2y,v == y-x）相对复杂，通常涉及到一个昂贵的约束求解器。
精度的问题：一方面，由于不可靠的结果可能会让我们错误地修剪可以到达目标的路径，所以我们不能在我们的场景中使用这些方法。另一方面，来自不同分支的合并条件可能会导致精度损失。
基本想法：
•使用一个轻量级静态分析器来计算合理的中间程序状态（以一阶逻辑条件的形式），作为执行达到目标的前提条件。任何违反这些中间条件的执行都应立即终止。
需要解决的挑战
•如何有效地推理前提条件中的路径条件?
•如何在设计合理的分析的同时避免合并路径带来的严重精度损失?

BEACON

•输入：程序源代码（编译为llvm
bitcode）、fuzzing目标代码
•不可达分析：为了简化静态分析和修剪明显不可行的路径，首先对过程间控制流图（ICFG）进行图可达性分析，修剪无法到达目标代码的基本块。使用了一个有效而合理的指针分析来解析函数指针
•逆向区间分析：剔除更多不可行的路径(比如那些条件不满足的路径)

逆向区间分析

使用区间域推理：
常用的数值抽象域包括区间域、八边形域、多面体域等，可以帮助推断程序中出现的变量的可能值。在这项工作中，我们选择区间域，因为它几乎是最小的域，使用区间域表示的前提条件可以在运行时进行有效检查，只需要比较变量和常量(即区间的边界)。因此，它不会对初始执行造成太多的运行时开销。
导致感知不精确：
（1）区间抽象是粗糙的，产生不精确的结果。
（2）反向路径的合并也可能导致不精确的结果
解决方法：
•关系保留relationship preservation. 保留了程序变量之间的关系，从而保持了精度
•保持v==y-x的关系，根据v,x的条件，推断出y。还可以进一步推断出14行的z。

•有界分离bounded disjunction 限制分离的数量，以避免昂贵的逻辑推理和穷举路径合并造成的精度损失。
为了控制精度损失，同时加快速度，我们对分析结果保持有界分离，只有当路径数量超过阈值τ时才合并结果。

评估

评估结果表明，BEACON比现有的定向灰盒fuzzer平均快11.50倍，并能提高传统覆盖制导模糊器AFL、AFL++和Mopt的重现特定bug的速度，分别提高了6.31倍、11.86倍和10.92倍。更有趣的是，在用于测试漏洞补丁时，BEACON发现了14个现有CVE 识别漏洞的不完整修复和 8个新错误。

不足及未来方向

•加速静态分析：在实践中，我们可以通过利用静态分析社区提出的其他技术（例如增量分析）来进一步加速静态分析。
•混合模糊：混合模糊的方法与BEACON正交，并且可以与BEACON集成以获得更好的性能
•大规模程序：本文还没有证明
BEACON 能够帮助依赖符号执行的模糊器。然而，由于可扩展性问题是符号执行的主要问题，如何有效地处理实验中选择的大规模程序可能成为另一个挑战。