【论文阅读】Locus: Agentic Predicate Synthesis for Directed Fuzzing

Canary 金丝雀探针#

Canary 是指在代码中显式插入的、用于检查是否触发了特定漏洞或到达了特定状态的谓词/断言语句（Assertion）。当相应的 canary 条件满足时，认为这些状态已被达到。

用于有向模糊测试的 canary 来源于各种途径，包括静态分析警报、手动识别的漏洞位置或运行时清理器。例如，地址清理器也可以近似地视为检查内存安全违规的 canary，例如插入 canary(index > maxbound) 来检测越界访问。

现有定向模糊测试的三种通用策略#

现有定向模糊测试（Directed Grey-box Fuzzing, DGF）在指导测试用例到达金丝雀（Canary，即目标漏洞状态）时，主要采用以下三种通用策略：

1. 距离引导调度策略（Distance-guided scheduling）

• 原理：基于控制流图（Control Flow Graph, CFG），近似计算当前测试种子（Seeds）覆盖的代码区域到目标金丝雀（Canary）节点之间的”图距离”。
• 执行方式：
  • 种子优先级调度：优先给那些能进一步缩短到 Canary 距离的种子分配更多变异资源和执行时间（如 AFLGo, Hawkeye）。
  • 早期终止（Early Termination）：对于分析后发现极不可能到达 Canary 的执行路径，直接截断或提前终止执行，避免浪费 CPU 时间（如 Beacon, SelectFuzz）。

2. 领域特化的进度/状态抽象表示（Specialized progress-capturing state representations）

• 原理：针对特定类型的软件漏洞，人工设计领域专用的状态 abstraction，来追踪程序是否正在沿着触发漏洞所需的前置状态链条推进。
• 例子：例如对于”释放后重用”（Use-After-Free, UAF）漏洞，专门设计状态机来监控从”内存分配（Allocate）→ 内存释放（Free）→ 重新指针解引用（Use）“的特定时序和数据流事件（如 CAFL）。

3. 基于 LLM 的测试驱动/输入生成器合成（LLM-assisted harness generation）

• 原理：利用大语言模型（LLM）理解代码和语法规范的能力，直接生成具备语法感知的输入生成器（Fuzzing Harness）。
• 执行方式：尝试将到达 Canary 所需的各种前置条件，直接转化为在输入层（Input Level）的语法约束（如 InputBlaster, HGFuzzer），从一开始就限定 Fuzzer 只生成符合特定结构的输入，从而缩小搜索空间。

论文在提出这三种通用策略的同时，也指出了它们各自的瓶颈，从而引出了 Locus 的核心思想：

动机示例 Motivating Example#

论文使用 libpng（一个广泛用于解析 PNG 文件的 C 库）中的一个真实漏洞 CVE-2013-6954，来演示 Locus 如何补充现有方法。

案例背景：CVE-2013-6954 (libpng)

• 漏洞原理：libpng 是 C 语言中广泛使用的 PNG 图像解析库。该漏洞属于堆缓冲区溢出（Buffer Overflow），触发条件是 PNG 文件包含一个调色板数据块（PLTE 块），且调色板的尺寸超过了预设的最大限制（即 Canary 条件：num > PNG_MAX_PALETTE_LENGTH）。
• 程序结构：PNG 文件由一系列结构化的数据块（Chunks）组成。libpng 的核心解析逻辑是在主函数 png_read_info 中运行一个循环，轮询处理各个数据块（如文件头 IHDR、调色板 PLTE、图像数据 IDAT 等）。

参见下图：

作者分析了现有的定向模糊测试策略遇到此类漏洞时的局限性：

① 传统”距离引导调度”的困境（图 1a）

• 控制流图（CFG）等距盲区：在 png_read_info 的解析循环中，处理不同数据块的分支（PLTE、color 等）在语法结构上是并行的。
• 问题：如图 1a 所示，灰色高亮节点在 CFG 上到目标 Canary 节点（黄色）的距离完全相同。但事实上，只有经过 PLTE 分支（绿色箭头路径）才能触发漏洞。传统 Fuzzer（如 AFLGo）无法识别哪个并行分支才是关键路径，只能做保守的粗粒度剪枝（虚线箭头），导致在无关路径（黑色实线）上浪费大量的测试时间。

② 基于”LLM 生成 Harness / 输入生成器”的困境（图 1b）

• 输入层约束表达力不足：PNG 文件的压缩数据（如 IDAT 块）结构复杂，LLM 很难直接在入口层（Harness 层面）构造精准的输入语法约束。LLM 生成的代码往往只能做到通用校验（如 png_sig_cmp 仅检查是否为合法 PNG）。
• 容易误导与产生幻觉：LLM 生成的 Harness 可能强行将输入限定在无关类型上（如生成 png_write_frame_head 约束，把测试限定在 APNG 动态图片格式），导致完全无法到达 Canary 目标。
• 代码冗余开销：为了在入口校验这些属性，生成器不得不重复编写解析逻辑（如计算 CRC 表），增加了每次执行的开销。

③ 专家手动设计状态抽象的困境

• 需要安全专家深刻理解 libpng 的内部逻辑才能写出有效规则，人力成本极高，且无法泛化到其他程序和漏洞。

Locus 如何解决？（三步演进与精炼，图 1c）

Locus 的思想是：不局限于输入入口，允许在程序任意中间位置合成带有早期退出（EXIT()）的进度谓词（Predicates）。

在处理该漏洞时，Locus 通过 Synthesizer-Validator Agent 循环 经历了 3 步迭代：

步骤 1：生成初始谓词（标记 ❶）

• 合成位置：Canary 函数的直接调用者 png_write_png 中。

• 生成谓词：if (png->color != PALETTE) EXIT();

  漏洞（CVE-2013-6954）发生在处理调色板数据的函数 png_set_PLTE 中（调色板数据长度超出最大限制导致缓冲区溢出）。如果输入的 PNG 图片根本不是调色板模式（比如是一张普通的 RGB 真彩色图片），那它绝对不可能执行到目标 Canary 语句去触发漏洞。通过加上这句话，一旦 Fuzzer 喂进来一张非调色板图片，程序就会立马退出，不再继续往下执行后续昂贵的解压、渲染逻辑，从而帮 Fuzzer 节约时间。

• 评价：语义上是正确的（没有 PALETTE 就无法触发目标 Canary），并且通过了符号执行的弛豫验证。但因为紧接着原代码中就有类似的检查（if (color_type & MASK_PALETTE)），所以插入在这里对 Fuzzer 的加速作用微乎其微。

步骤 2：第一次位置上提/精炼（标记 ❷）

原因：为了让程序更早地退出，Locus 的 Agent 启动了位置上提（Refinement，精炼）机制。found_plte 就是在往程序入口推进的过程中被 Agent 创造出来的。Agent 发现 png_read_info 里面有一个 for (;;) 循环，专门用来逐个读取 PNG 的数据块（Chunk，比如 IHDR 块、PLTE 块、IDAT 块等）。合成标记变量：Agent 意识到可以在循环前定义一个局部变量 int found_plte = 0;——循环中如果读到了 PLTE 块（chunk_name == png_PLTE），就把标记设为 found_plte = 1;。循环结束后检查：if (!found_plte) EXIT();（如果整个循环跑完都没遇到过 PLTE 块，说明这图没救了，直接退出）。

• 合成位置：通过遍历调用图向上追踪，推导至更靠近入口的函数 png_read_info 中，放在解析循环刚好结束的地方。
• 生成谓词：插入辅助变量并在循环后检查 if (!found_plte) EXIT();
• 评价：使得没有解析到 PLTE 块的输入在循环结束时就能直接提前终止（Early Exit），不必继续执行后续昂贵的渲染和写入逻辑。

步骤 3：第二次深度语义精炼（标记 ❸）

• 深度语义推理：Locus 的 Agent 进一步分析 PNG 协议规范发现：PNG 规范规定可选的 PLTE（调色板）块必须出现在 IDAT（图像数据）块之前。
• 合成位置与谓词：Locus 直接将谓词推进至解析 IDAT 块的分支内部：

1
if (chunk_name == png_IDAT) {
2
    if (!found_plte) EXIT(); // 到了 IDAT 还没发现 PLTE，说明后面不可能有了，直接退出！
3
}

• 效果：一旦解析流接触到 IDAT 块而此前未标记过 PLTE，程序立马提前终止。

最终效果与启示

• 极致加速：对于原本极其棘手的 CVE-2013-6954，仅仅凭借 Locus 在 png_read_info 中插装的这 3 行精炼后的谓词代码，就为经典定向 Fuzzer（AFLGo）带来了 8 倍（8x）的漏洞触发加速。
• 启示与总结：
  1. 证实了在中间程序点插入语义谓词比单纯在输入入口做 Harness 约束更灵活、更有效。
  2. 证明了 Agent 多轮位置上提（Refinement） 机制的必要性——越靠近入口终止，节约的时间成本越高。

谓词合成与精炼（Synthesis）#

1
Require: original program P, vulnerability canary ψ
2
Ensure: a target-conditional equivalent program P'
3

4
1: C ← CANARYREASONING(P, ψ)        ▷ 获得推理列表 (list of reasonings)
5
2: Φ ← ∅
6
3: for all c ∈ C do
7
4:     l ← LOCALIZE(c, P)            ▷ 寻找初始程序点 (find the initial program point)
8
5:     n ← 0
9
6:     repeat
10
7:         ϕ_l ← GENERATE(l, c, P)
11
8:         while ¬VALIDATE(ϕ_l, ψ, P) do ▷ 语法与语义校验 (syntax and semantic)
12
9:             ϕ_l ← GENERATE(l, ϕ, P)
13
10:        end while
14
11:        l ← LOCALIZE(ϕ, l, c, P)      ▷ 精炼上提，寻找更好的位置 (refine, find a better location)
15
12:        n ← n + 1
16
13:    until l = None ∨ n > MAXITERATIONS
17
14:    Φ ← Φ ∪ {ϕ_l}
18
15: end for
19
16: P' ← INSTRUMENT(P, Φ)            ▷ 自动化生成模糊测试容许程序 (fuzzing admissible program)

• 输入 (Require)：原始程序 $P$ 及目标漏洞金丝雀 $\psi$。
• 输出 (Ensure)：插装谓词后、与原程序在目标条件上等价的程序 $P'$。

算法 1（Algorithm 1）展示了 Locus 谓词合成的具体流程。由于一次性让 LLM 直接写出完美且靠前的中间谓词非常困难，Locus 采用了一种 “迭代定位-生成-精炼” 的工作流：

1. 初始 Canary 推理：Agent 先分析 Canary $\psi$，大致推测出可能与该漏洞相关的输入特征（如数据结构、类型、关键标志位）。
2. 粗粒度定位：Agent 先不用精确到某一行，而是先挑出一个候选函数，并在该函数内生成初始谓词（即动机示例中的步骤 ❶，位置比较靠后）。
3. 迭代精炼（Refinement）：
   • 只要初始谓词通过了后面的验证，Locus 就会启动精炼循环（Refinement）。
   • Agent 会利用调用图工具，尝试把这个谓词”向上提炼（Propagate）“到调用链中更靠近程序入口的函数里，或者推到更前置的分支中（如精炼到步骤 ❷ 和 ❸）。
   • 目的：越早的阶段把无效输入拦截（Early Termination），Fuzzer 就能省下越多宝贵的模糊测试时间。

双重验证（Validation）#

为了防止 LLM 产生幻觉或写出错误的谓词导致程序崩溃、或者错误”误杀”了漏洞触发路径，Locus 设计了严格的双重验证流水线：

1. 语法验证（Syntax Validation）：
   • 怎么做：直接把生成的谓词插到代码里，调用项目的构建系统（如 Makefile / CMake）尝试编译。
   • 反馈修复：如果报错（如符号未声明、类型不匹配），编译器报错信息会被喂给 LLM 让其自我修正（Self-reflection）。
2. 语义验证（Semantic Validation）—— 核心难点：
   • 目标：通过数学方式证明生成的谓词 $\phi$ 确实是 Canary $\psi$ 的”严格放松条件”（定理 2：如果存在某条路径使得 $\neg\phi$ 成立但 $\psi$ 依然能触发，说明谓词有误杀，验证失败）。
   • 工具：使用 KLEE 符号执行引擎来寻找这样的反例。
   • 工程优化（解决路径爆炸）：符号执行非常慢。Locus 借鉴了 Chopper 的思想，先用 SVF 静态分析框架对控制流图（CFG）进行可达性剪枝，只保留跟谓词和 Canary 相关的关键路径，把不相干的分支全部切掉，从而大幅降低符号执行的开销。