本文档介绍了由芝加哥大学的祝杰（Jie Zhu）和裴可欣（Kexin Pei）、马里兰大学的沈持昊（Chihao Shen）和陈毅征（Yizheng Chen）、约翰斯·霍普金斯大学的李梓扬（Ziyang Li）以及西北大学的于佳豪（Jiahao Yu）共同完成的研究成果。该研究以论文形式发表，标题为“Locus: Agentic Predicate Synthesis for Directed Fuzzing”，计划于2026年4月12日至18日在巴西里约热内卢举行的IEEE/ACM第48届软件工程国际会议（ICSE ‘26）上正式发布。
研究背景与目标 定向灰盒模糊测试（Directed Grey-box Fuzzing, DGF）是一种旨在生成能够触发特定目标程序状态（例如漏洞点）输入的软件测试技术。它在调试系统崩溃、验证已报告缺陷以及生成漏洞利用证明等方面具有广泛应用。然而，定向模糊测试面临的根本挑战在于：目标状态通常深藏在复杂的程序逻辑中，而由海量可能输入构成的搜索空间极其庞大。现有的方法主要依赖分支距离或专家手动编写的约束来引导搜索。但这些方法存在明显局限：分支距离往往过于粗糙，无法精确刻画向目标状态推进的语义进度；而手动编写的约束通常针对特定类型的漏洞，难以泛化到多样化的目标状态和程序上。
随着大型语言模型（LLMs）展现出强大的代码理解和推理能力，研究者开始探索利用LLM辅助模糊测试，例如直接生成测试输入或构建输入生成器。然而，这些方法要求LLM从目标状态一路反向推理到程序输入，这一过程不仅需要处理极长的上下文和复杂的分析链，容易导致LLM“幻觉”产生错误，而且生成的输入或约束的正确性也难以验证，错误的引导反而可能阻碍模糊测试进程。
基于上述背景，该研究团队的目标是提出一个能够自动生成语义明确且可验证的“谓词”（predicates），以高效引导定向模糊测试的新框架。其核心洞察是：通过合成能够捕获模糊测试进展的谓词，作为通往目标状态的、具有语义意义的中间里程碑。当这些谓词被插入到待测试的程序中时，它们可以提前终止那些不太可能到达目标状态的执行路径，同时为模糊器提供额外的覆盖度反馈，从而大幅提升搜索效率。
研究方法论与工作流程 Locus框架的核心是一个智能体（Agentic）的谓词合成-验证工作流。其输入是待测程序P和一个描述目标状态的金丝雀（Canary）条件Ψ，输出则是一个插入了谓词集合Φ的程序P‘。整个过程分为合成与验证两大阶段，并遵循迭代求精的流程。
首先，谓词合成阶段由一个LLM驱动的智能体完成。该智能体被赋予了一套专门的工具集，用于在代码库中进行导航和推理，包括：代码搜索、文件列表、函数调用图遍历、符号引用查找等。特别是图遍历工具，使得智能体能够理解程序的控制流和数据依赖关系，这对于跨函数的语义推理至关重要。合成过程并非一蹴而就，而是采用迭代式的“定位-生成-精炼”策略。具体步骤如下： 1. 初始分析与定位：智能体首先分析金丝雀条件Ψ，推理导致该漏洞的根本原因，并近似生成一系列与触发条件相关的输入特征（如数据结构、类型、属性）。基于这些特征，智能体选择一个候选函数作为初始谓词的插入位置。 2. 谓词生成：在选定的函数上下文中，智能体利用其代码理解和从工具获取的信息，生成一个具体的谓词条件（例如，一个if语句的条件）。这个谓词旨在捕捉到达目标状态的一个必要前提。 3. 迭代精炼：初始谓词虽然语义正确，但可能位于程序执行路径的较深位置，提前终止的效果有限。因此，Locus会启动精炼循环。智能体尝试将当前谓词的语义向上游传播，寻找一个更靠近程序入口的、但仍能表达相同约束的新程序点。例如，在图1（c）的案例中，谓词从png_set_plte函数（接近漏洞点）被成功精炼到了png_read_info函数中解析循环的内部，从而能更早地筛除非相关输入。
其次，谓词验证阶段至关重要，它确保了合成的谓词不会错误地拒绝那些本可以到达目标状态的合法输入，从而保证插桩后的程序P’相对于原程序P是“模糊测试可容许的”。验证分为两步： 1. 语法验证：将生成的谓词插入到候选程序点，调用项目的编译系统进行构建。如果编译失败，则将编译错误信息反馈给合成智能体进行修复。 2. 语义验证：这是确保谓词正确性的核心。Locus采用符号执行（使用KLEE引擎）来形式化地检查生成的谓词φ是否是金丝雀条件Ψ的一个“松弛”。验证的核心定理是：如果存在一条执行路径，它违反谓词φ（即φ为假）但却能满足金丝雀Ψ（即Ψ为真），那么这个谓词就不是一个有效的松弛，因为它错误地过滤了有效路径。Locus通过符号执行探索从¬φ到Ψ的路径来寻找这样的反例。为了提高验证效率，研究还采用了基于控制流图的轻量级可达性分析，对无关路径进行剪枝，聚焦于关键路径的探索。
只有通过了语法和语义双重验证的谓词，才会被最终采纳并用于插桩。这个智能体与验证器协作的闭环设计，巧妙地将LLM强大的代码推理能力与程序分析工具的形式化保证结合起来，既利用了LLM的创造性，又通过严格验证约束了其输出空间，纠正了可能出现的错误。
主要实验结果 研究团队在Magma模糊测试基准上对Locus进行了全面评估。Magma基准包含了来自八个广泛使用的开源库（如libpng, libtiff, OpenSSL等）的31个真实世界漏洞，覆盖了多种漏洞类型。他们选择了八款先进的模糊器作为基线，包括四款定向模糊器（AFLGo, SelectFuzz, BEACON, TITAN）和四款覆盖引导模糊器（AFL, AFL++, MOpt, FOX）。
RQ1（有效性）：评估的核心指标是暴露时间（Time To Exposure， TTE），即模糊器首次触发目标金丝雀所需的时间。实验结果表明，Locus对所有被测模糊器都带来了显著的加速效果。平均而言，集成了Locus的定向模糊器获得了70.3倍的TTE加速，其中对SelectFuzz的加速比最高达到214.2倍。对于覆盖引导模糊器，平均加速比也达到了13倍，其中对高度优化的AFL++加速了15.3倍。更重要的是，在24小时的固定时间窗口内，AFLGo和AFL等模糊器在Locus的帮助下，分别多发现了5个和4个原本无法触发的漏洞。
RQ2（成本与性能）：研究者测量了部署Locus的预处理开销（包括代码索引、谓词合成与验证）和LLM推理的token成本。结果显示，Locus的平均预处理时间（约几百到一千秒）远低于某些需要进行复杂静态分析的定向模糊器（如AFLGo在处理大型项目时可能耗时数小时）。在token成本方面，平均每个漏洞样本的谓词生成消耗约45.7万token，按市价估算成本极低（约0.72美元），表明该方法是经济可行的。
RQ3（消融研究）：通过消融实验验证了Locus各个设计组件的必要性。实验对比了：仅使用初始合成谓词（Base）、增加精炼但不验证（Refine）、以及完整流程（Valid）三种设置。结果清晰地表明，没有验证的精炼虽然有时能提升性能，但更可能生成错误的谓词，导致模糊器性能下降甚至超时（无法找到漏洞）。而完整的验证流程则保证了性能的稳定提升。研究还测试了不同的LLM（如DeepSeek R1, Gemini Flash 2.0），发现Locus的框架具有良好的通用性，不同架构的LLM都能带来显著改进。
RQ4（安全影响）：为了评估Locus在真实漏洞检测场景下的能力，研究者将其应用于多个已充分测试过的软件项目（如VLC, libarchive, tcpreplay）。他们通过静态分析警报或历史补丁来生成目标金丝雀，并启动模糊测试活动。最终，Locus成功帮助发现了9个先前未知的未修补漏洞，包括内存泄漏、释放后使用、空指针解引用和越界访问等。所有漏洞均已负责任地报告给维护者，其中3个漏洞已获得确认并有了待定的修复补丁。
结论与价值 本研究提出的Locus框架，通过引入一个基于LLM智能体的、可验证的谓词合成工作流，为定向模糊测试领域提供了一种新颖且高效的通用增强方案。其核心贡献在于：1）将LLM的代码推理能力有效地应用于引导模糊测试，但通过将输出约束在谓词级别并引入形式化验证，规避了LLM直接生成输入或复杂代码时常见的幻觉和不可靠问题；2）提出的谓词作为语义里程碑，能够提供比传统分支距离更精细的引导，并能通过早期终止无效执行来加速搜索；3）框架设计与具体模糊器实现无关，可以轻松集成到现有的各类定向或覆盖引导模糊器中，作为一次性的、离线的程序插桩预处理步骤。
这项研究的科学价值在于，它成功地桥接了基于学习的智能代码合成与经典的程序分析验证技术，为如何安全、可靠地利用大模型解决程序分析中的难题提供了一个范例。其应用价值则非常直接且显著：能够大幅提升软件安全测试中漏洞复现和发现的效率，降低对专家手动编写引导规则的依赖，并已在实践中证明了其发现新漏洞的能力。
研究亮点 1. 创新性的问题重构：不同于现有LLM用于模糊测试的研究，Locus不要求LLM直接推理从漏洞到输入的完整复杂链条，而是让其专注于生成程序内部的可验证中间状态（谓词），这大大降低了任务的复杂性并提高了可控性。 2. 智能体与验证器协同的架构：该设计是研究的核心亮点。智能体负责探索和创造性合成，而验证器（编译器、符号执行）则提供严格的形式化保证，确保输出的正确性。这种协同机制有效地缓解了LLM的不可靠性问题。 3. 显著的实践效果：在标准基准和真实世界软件上的评估结果极具说服力。平均数十倍的加速比和发现多个新漏洞的成果，强有力地证明了该方法的有效性和实用性。 4. 良好的泛化性：实验表明，Locus不仅适用于多种类型的模糊器，也能兼容不同的LLM，并且初步探索显示其框架可扩展至Python、Go等其他编程语言的模糊测试场景，展现了其作为通用解决方案的潜力。
其他有价值内容 论文中通过一个详细的案例（libpng中的CVE-2013-6954漏洞）生动阐释了Locus的工作过程及其相对于传统方法（分支距离引导）和纯LLM生成输入方法（输入约束生成）的优势。案例显示，在复杂的解析逻辑下，多个分支在控制流图上与漏洞点距离相同，传统方法无法区分；而Locus通过语义推理，成功合成出检查PNG文件是否包含必需PLTE块的谓词，并将之精炼到解析循环内部，从而实现了精确的早期过滤。此外，研究还展示了Locus甚至可以根据安全补丁自动生成比人工标注更精确的金丝雀条件，这扩展了其应用场景，不依赖于预先存在的、手工定义的目标状态。