Reading Papers - Directed Fuzzing
# Directed Grey-Box Fuzzing
# CCS'17 - AFLGo
# SEC'21 - CAFL, CDGF
# Directed White-Box Fuzzing
# ICSE'22 - LTL Fuzzer
LTL Fuzzer 利用时序逻辑自动机来强化 directed fuzzing ,以期能处理复杂的时序属性。
Taxonomy : mutation-based / directed / white-box fuzzing
Tag : guided fuzzing
现有的 directed fuzzing 的测试目标仅限于一些易于观测的目标,例如到达某个程序点、违反简单的不变式(崩溃或 use-after-free)、观测一组简单的事件序列,等等,而不能像 model checker 或者 runtime verifier 那样处理复杂的时序属性。
对于给定的顺序程序和需要验证的时序属性 ,LTL Fuzzer 构造一个接受 的 Buchi 自动机 来指导 fuzzing ,尝试生成违反 的 counterexamples 。
LTL Fuzzer 的工作流程如下:
将非形式化的 specification 或 assertion 人工转换为 LTL 属性。
人工考虑每个原子命题 在程序中的哪些位置 会受到影响,记为一系列的二元组 ,其中 为触发条件。
根据二元组序列对被测程序进行插桩,以便于在运行时刻监测 的满足性。
找到违反 的输入是困难的,因为这可能要求一系列的事件按照某种特定的顺序触发,并且这样的输入可能具有无限长的 trace 。
LTL Fuzzer 尝试生成输入以按照特定顺序触发事件序列:
Power Scheduling :预先构建过程间控制流图,并为在 CFG 上更接近目标的 input seed 赋予更高的优先级。此处的实现继承了 AFLGo 的算法。
Input Prefix Saving :依次以 为目标进行探索,并在探索后续目标时基于先前已发现的输入前缀进行探索。
LTL Fuzzer 为能在 Buchi 自动机 上取得更多进展的输入赋予更高的优先级,例如执行了更多的状态转换或是更接近测试目标。
LTL Fuzzer 对不同的属性用不同的方式来处理无限长的 trace :
对于 safety property ,一次违反就意味着永久违反,因而易于处理。
对于 liveness property ,判定 infinitely often 访问状态机的终结状态是不可能的,简单以观测到固定次数的循环又是不准确的。LTL Fuzzer 仅考虑 trace 中与 中原子命题相关的事件,并观测是否存在循环。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01