white box fuzzing一般使用符号执行，天生使用符号执行从根本上限制了他们的扩展能力，并且执行速度一般非常慢(24小时以上)，而grey box fuzzing技术并不是直接抛弃拒绝无法达到的路径，而是根据每个seed的score(能够到达目标地址的可能性，通过判定距离目标位置的远近，或者机器学习的方法)，给出seed优先权。但是由于不对地址做预先筛选，大部分执行路径是无法到达target site的。
本文给出的Beacon的创新点在于，通过廉价的静态分析，我们可以计算直接导致目标路径不可行的程序变量值的合理近似值，从而根据此就可以修剪超过80%的不可行路径(包含无法到达以及到达时数据条件不满足两种情况)。
Directed Grey-Box Fuzzing with Provable Path Pruning
文章标题是”具有可证明路径剪枝”的DGF。
问题和创新点
white box fuzzing一般使用符号执行，天生使用符号执行从根本上限制了他们的扩展能力，并且执行速度一般非常慢(24小时以上)，而grey box fuzzing技术并不是直接抛弃拒绝无法达到的路径，而是根据每个seed的score(能够到达目标地址的可能性，通过判定距离目标位置的远近，或者机器学习的方法)，给出seed优先权。但是由于不对地址做预先筛选，大部分执行路径是无法到达target site的。
本文给出的Beacon的创新点在于，通过廉价的静态分析，我们可以计算直接导致目标路径不可行的程序变量值的合理近似值，从而根据此就可以修剪超过80%的不可行路径(包含无法到达以及到达时数据条件不满足两种情况)。
为了确保一个进程状态的有效性，引入一个新的静态分析方式，来达到精确性和有效性
- relationship preservation
保持变量之间的数据流关系，从而保持精度
- bounded disjunction
防止析取过多导致推理的浪费
因此总的来说，这种fuzzer就是通过首先引入一种轻量级静态分析技术判断数据流条件，对所有不可能的路径进行剪枝，从而减少fuzzer的开销
技术细节
上述推理器首先把中间程序状态计算为最弱先决条件（也称为必要先决条件）的近似值，这在静态分析中得到了广泛的研究 。举个例子
对于上图中，我们如果想要计算从13行到18行的最近距离，需要满足从14行到18行的所有条件合取的结果。这个合取结果就称为最弱先决条件。不满足这个条件的输入可以被安全的舍弃。
然而，此时我们仍需考虑静态处理中的一些问题。静态分析一般是速度和准确性不能共存的，并且对于路径求解，一般的静态分析会直接在CFG汇合处合并条件(会产生问题例如a<10并且a>20被合并为a<10 || a>20的错误)或者直接舍弃必要结果，这些对于fuzz都是不可接受的。
BEACON
首先，BEACON对代码做一个可达分析，并且把显然不能到达目标的路径删除。
其次BEACON如何解决上面两个问题？
首先，关系保持。在变量之间关系保持能够带来更加准确的前提条件，这样可以减少更多分支。这要求我们记录下买一个变量的位置作为他们的标识。
其次，有界析取。例如将($-\infty$，5)∪(25, $+\infin$)做一个上下界限制。
作者采用的instrument的方法是通过添加assert语句的instrument来减少分支执行。
后向区间分析
这一部分的目的是确保被剪枝的路径确实不能到达目标block。我们需要接受目标地址块和初始条件作为参数。举个例子
对于上面这张图，如果设置目标($\phi$)为第18行的w>10，并且假设第18行的条件为正确(可达)我们向前追溯，直到第9行，则有以下两种分支。但是求解以下分支需要的SMT比较复杂。
作者为了解决这个问题，设计了一个线性域
例如对于上面的条件，写出如下的线性域。注意两者取交集的表示方式。
优化
- 合并分支
当到达l的路径个数比threshold小的时候，就保持原来的条件不变，否则就要对条件进行合并。合并的原则是对于合并后对精确性影响最小的两个条件。下图是精度丢失的例子。
其实合并的过程就是取并集，而精度丢失也就是并集中多增加的元素。
- 预条件instrument
这个优化是为了解决我们关注的变量过多的问题。作者的思想是如果变量B由变量A决定，那么就不关注变量B。具体来说，算法为
- 将程序转换为SSA模式这个后续还要看一下，因为SSA模式确保一个变量在写之前不会被定义。(可能通过这种方法可以确保变量定义位置)
- 如果确保变量B由变量A决定，那么就不关注变量B。
总结
总结一下BEACON带来的优化思想，是输入生成(input generation)和种子优化(seed prioritization)。具体来说，包含了1.去除不必要的分支来减少随机性带来的开销，并验证这种分支优化是合理的。2.对输入条件做总结(使用映射到线性域的方式)，优化推理过程
源码分析
这里顺便记录一下从image启动container的方法
- docker run -dit yguoaz/beacon /bin/bash (从image启动docker)
- docker exec -it d0f4b4974782 /bin/bash (这里的数字是containerID)
好吧，这个工程文件也没有提供源码