💻 computer science

Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery

本文提出了 SAILOR 框架，通过结合静态分析定位漏洞、大语言模型迭代合成执行桩以及符号执行与具体重放验证，实现了在大规模 C/C++ 项目中自动化发现 379 个此前未知的内存安全漏洞，其效果显著优于现有基线方法。

原作者： Md Shafiuzzaman, Achintya Desai, Wenbo Guo, Tevfik Bultan

发布于 2026-04-09

📖 1 分钟阅读☕ 轻松阅读

原作者： Md Shafiuzzaman, Achintya Desai, Wenbo Guo, Tevfik Bultan

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文介绍了一个名为 Sailor（水手）的全新系统，它的任务是自动在巨大的计算机代码库中寻找“漏洞”（就像寻找建筑物里的裂缝或电路里的短路）。

为了让你更容易理解，我们可以把寻找代码漏洞的过程想象成在一个巨大的、迷宫般的废弃工厂里寻找隐藏的炸弹。

1. 为什么以前的方法行不通？（旧方法的困境）

在 Sailor 出现之前，人们主要用三种方法找炸弹，但都有大问题：

静态分析（Static Analysis）：像拿着放大镜看图纸。
- 比喻： 你有一张工厂的图纸，用放大镜看哪里画得不对（比如“这里没画保险丝”）。
- 缺点： 图纸太复杂，放大镜看一遍会看到成千上万个“可能有问题”的地方，但其中 99% 都是误报（其实那里并没有炸弹，只是图纸画得奇怪）。这就像大海捞针，效率极低。
模糊测试（Fuzzing）：像往工厂里扔石头。
- 比喻： 你往工厂各个角落扔石头，看哪里会爆炸。
- 缺点： 如果炸弹藏在工厂最深处的一个上了锁的保险柜里，而你扔的石头根本打不开门，或者你扔的石头形状不对，你就永远触发不了爆炸。
大语言模型（LLM）：像请了一个博学的侦探。
- 比喻： 你请了一个读过很多书、很聪明的侦探（AI）来看图纸。
- 缺点： 这个侦探虽然聪明，但他没有亲眼见过工厂内部。他可能会自信满满地告诉你“这里肯定有炸弹”，但实际上那里很安全；或者他漏掉了真正的炸弹。而且，如果工厂太大（代码几百万行），侦探的脑子（上下文窗口）也装不下整个工厂的图纸。
符号执行（Symbolic Execution）：像派一个超级机器人进去模拟。
- 比喻： 这是一个能模拟所有可能情况的超级机器人。它能精确地算出：“如果输入是 A，炸弹会炸；如果输入是 B，炸弹不会炸”。
- 缺点： 这个机器人不会自己开门。它需要有人（专家）给它写一张详细的“入场指南”（Harness），告诉它从哪个门进、怎么开保险柜、怎么绕过守卫。写这张指南非常难，需要专家花大量时间手动编写，这成了最大的瓶颈。

2. Sailor 是怎么工作的？（三阶段接力赛）

Sailor 的创新之处在于，它把上述四种方法结合了起来，组成了一支完美的三人探险队，分三个阶段工作：

第一阶段：静态分析（SA）—— “地图标记员”

角色： 拿着放大镜的初级侦察兵。
任务： 它快速扫描整个工厂（代码库），虽然它分不清真假，但它能圈出所有“看起来像炸弹”的可疑地点。
Sailor 的魔法： 它不只是扔出一堆乱码，而是把每个可疑地点整理成一张**“寻宝卡片”**（Vulnerability Specification）。卡片上写着：“这里有个可疑的 memcpy 函数，可能没检查长度，请重点调查。”
作用： 把大海捞针变成了“在几个特定的盒子里找针”。

第二阶段：大语言模型（LLM）+ 符号执行（SE）—— “智能向导与超级机器人”

这是 Sailor 的核心（也是论文最厉害的地方）。

角色： 一个聪明的向导（LLM）和一个超级机器人（SE）。
任务：
1. 向导（LLM）看卡片： 向导拿到“寻宝卡片”后，开始研究工厂的局部结构。它需要写一张**“入场指南”**（Harness），告诉机器人怎么进那个特定的房间。
2. 试错与修正（迭代）： 向导写的指南第一次可能不行（比如门打不开，或者机器人撞墙了）。这时候，编译器和机器人会反馈错误信息：“门打不开，因为少了一把钥匙”或者“机器人卡住了”。
3. 向导修改指南： 向导看到反馈，立刻修改指南，再试一次。这个过程会重复很多次（就像玩游戏通关，死了读档重来），直到向导写出完美的指南。
4. 机器人执行： 一旦指南完美，超级机器人（符号执行引擎 KLEE）就进去模拟。它能计算出：“只要输入一个长度为 17 的字符串，炸弹就会爆炸！”并生成具体的**“触发密码”**（Witness Inputs）。
比喻： 以前写指南靠专家手动写，现在靠 AI 向导自己试错、自己修改，直到把机器人送进最深处。

第三阶段：具体验证（Concrete Validation）—— “真人实测”

角色： 勇敢的拆弹专家。
任务： 机器人算出的“触发密码”是理论上的。为了确认它真的能炸，我们需要在真实的工厂（未修改的代码）里，用真实的炸弹（AddressSanitizer 工具）试一次。
作用： 如果真人试了真的爆炸了，那就100% 确认找到了真炸弹。如果没炸，说明之前的 AI 向导可能被骗了（误报），直接扔掉。

3. 结果有多厉害？

研究人员在 10 个著名的开源大项目（总共 680 万行代码，相当于几百万行文字）中测试了 Sailor：

战绩： 发现了 379 个 以前没人知道的、真实存在的内存安全漏洞（比如缓冲区溢出，会导致黑客控制电脑）。
对比：
- 最强的竞争对手（一个拥有无限权限、能自由探索整个代码库的 AI 代理），只找到了 12 个 漏洞。
- 如果没有静态分析（让 AI 自己瞎找），找到的漏洞数量会暴跌 12 倍。
- 如果没有 AI 向导的反复修改，一个漏洞都找不到。
- 如果没有最后的真人实测，就无法确认哪些是真正的漏洞。

4. 总结：Sailor 为什么成功？

这就好比找宝藏：

静态分析帮你缩小了搜索范围（从整个森林缩小到几棵树）。
AI 向导帮你画出了通往树洞的地图，并且通过不断试错，把地图画得完美无缺。
符号执行机器人按照地图，精确地算出了宝藏的位置和打开方式。
真人实测最后确认宝藏是真的。

Sailor 的核心思想是： 不要指望一种技术解决所有问题。让擅长“找线索”的静态分析、擅长“写代码和推理”的 AI、擅长“精确计算”的符号执行引擎，以及擅长“验证事实”的真人测试，分工合作，互相补位。

这就是为什么 Sailor 能像一位经验丰富的“水手”，在代码的汪洋大海中，精准地找到那些隐藏最深的“暗礁”（漏洞）。

论文技术总结：利用静态分析与大语言模型引导符号执行以发现漏洞

论文标题：Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery
作者：Md Shafiuzzaman, Achintya Desai, Wenbo Guo, Tevfik Bultan (UC Santa Barbara)
核心系统：Sailor (Static Analysis Informed and LLM-Orchestrated Symbolic Execution)

1. 研究背景与问题 (Problem)

在大型 C/C++ 代码库中自动发现漏洞面临巨大挑战，现有单一技术均存在局限性：

静态分析 (Static Analysis, SA)：虽然能扫描数百万行代码并标记大量候选点，但误报率（False Positives）极高，无法确认漏洞是否真实存在。
模糊测试 (Fuzzing)：通过具体输入执行程序，但难以触及深层库内部逻辑，特别是那些需要精确构建复杂程序状态才能触发的路径。
大语言模型 (LLMs)：具备代码理解能力，但缺乏形式化正确性保证，可能自信地报告不存在的漏洞或忽略真实漏洞。
符号执行 (Symbolic Execution, SE)：能精确处理输入并生成触发漏洞的具体输入（Witness），但可扩展性极差。主要瓶颈在于测试驱动（Harness）的构建：需要人工编写驱动程序来设置符号状态、模拟环境依赖（Stubs）并指定断言。对于大型项目，手动构建 Harness 需要深厚的专业知识，限制了 SE 的规模化应用。

核心问题：如何自动化地构建符号执行所需的 Harness，从而在大型代码库中规模化地利用符号执行进行精确的漏洞发现？

2. 方法论：Sailor 系统 (Methodology)

Sailor 是一个全自动化的三阶段流水线，结合了静态分析的可扩展性、LLM 的代码推理能力、符号执行的精确路径探索以及具体执行的验证能力。

阶段一：静态分析引导的目标生成 (Static Analysis Informed Target Generation)

输入：项目源代码。
过程：
1. 使用 CodeQL 运行包含 34 个查询（13 个标准 + 21 个自定义）的内存安全查询套件。
2. 事实生成与增强：提取可疑调用、指针变量、长度变量、边界提示及构建上下文（如 include 路径）。
3. 规范生成：将每个静态分析发现转化为一个独立的漏洞规范 (Vulnerability Specification)。规范包含：
  - 候选位置 ( $\ell$ )。
  - 漏洞描述 ( $d$ )。
  - 数据流轨迹 ( $\tau$ )。
  - 入口点选择：自动推断或指定符号执行的入口函数。
  - 断言模板：根据 CWE 类型提供安全属性模板（如缓冲区边界检查）。
输出：一组独立的、包含丰富上下文的漏洞规范，供下一阶段处理。

阶段二：LLM 编排的符号执行 (LLM-Orchestrated Symbolic Execution)

这是 Sailor 的核心贡献，利用 LLM 迭代合成并优化 Harness。

输入：阶段一生成的漏洞规范。
过程：
1. 驱动合成 (Driver Synthesis)：LLM 根据规范探索源代码，生成 main() 驱动函数。它负责分配内存、将关键变量声明为符号值 (klee_make_symbolic)，并添加假设 (klee_assume) 以绕过不必要的守卫条件，确保执行流能到达目标漏洞点。
2. 存根合成 (Stub Synthesis)：生成一个自包含的代码切片。LLM 将无关的分支替换为 if(0)，循环转换为单次 if，并将外部依赖函数替换为存根（Stubs）。存根根据路径需求返回符号值或默认值。
3. 断言实例化 (Assertion Instantiation)：根据规范中的模板，在代码切片中插入断言（如 klee_assert(0) 用于可达性检查，或构造违反安全属性的约束）。
4. 迭代优化 (Iterative Refinement)：
  - 将生成的 Harness 编译为 LLVM 位码并链接。
  - 使用 KLEE 进行符号执行（300 秒超时）。
  - 反馈循环：如果编译失败或 KLEE 未到达目标，系统提取错误信息（如类型缺失、守卫条件过强）并反馈给 LLM，LLM 据此修正代码。此过程最多进行 60 轮。
输出：如果 KLEE 检测到内存错误，则生成具体的触发输入（.ktest 文件）。

阶段三：具体验证 (Concrete Validation)

目的：消除因 LLM 生成的 Harness 不切实际（如状态初始化错误）导致的误报。
过程：
1. 将符号驱动转换为具体驱动：将 klee_make_symbolic 替换为从 .ktest 读取的具体字节。
2. 使用 AddressSanitizer (ASan) 编译未修改的项目源代码。
3. 运行具体驱动。
判定：只有当 ASan 在原始项目代码中报告内存安全违规（如堆缓冲区溢出）时，漏洞才被标记为已确认 (Confirmed)。

3. 关键贡献 (Key Contributions)

首个全自动化符号执行 Harness 构建流水线：Sailor 无需人工干预，即可将静态分析发现转化为可执行的符号执行目标，并通过 LLM 迭代优化解决 Harness 构建难题。
端到端实现与工具链整合：结合了 CodeQL (SA)、GPT-5/Opus (LLM)、KLEE (SE) 和 ASan (Concrete Validation)，仅需构建脚本即可运行，无需项目特定配置。
大规模实证评估：在 10 个开源 C/C++ 项目（总计 680 万行代码）上进行了评估，证明了其可扩展性、精确性和有效性。
可复现的证据包：每个发现的漏洞都附带路径约束、崩溃输入、ASan 堆栈跟踪和模糊测试种子。

4. 实验结果 (Results)

总体表现：在 10 个项目（6.8M LOC）中，Sailor 发现了 379 个独特的、以前未知的内存安全漏洞，并确认了 421 次崩溃。
对比基线 (Baselines)：
- 最强基线 (B5)：使用具有全代码库访问权限和无限交互的代理 LLM (Claude Opus)，仅发现 12 个漏洞。
- 其他基线：纯 LLM 检测 (B3, B4) 误报率极高（>99%）；人工编写 Harness 的符号执行 (B1) 因状态空间过大或无法编译而发现 0 个漏洞。
- 结论：Sailor 发现的漏洞数量是最佳基线的 30 倍以上。
消融实验 (Ablation Study)：证明了每个阶段的必要性：
- 移除静态分析 (A1)：确认的漏洞数量下降 12.2 倍 (379 -> 31)，表明 SA 对目标定位至关重要。
- 移除迭代优化 (B2)：确认的漏洞降为 0，表明 LLM 的一次性生成无法处理复杂的 Harness 构建。
- 移除符号执行 (B3-B5)：无法发现超过 12 个漏洞，表明 LLM 无法独立推理复杂的路径约束。
- 移除具体验证：会保留大量因 Harness 状态不真实导致的误报。
成本与效率：
- 处理了 87,385 个静态分析发现，最终确认 379 个漏洞。
- 平均每个漏洞消耗约 26K 个 Token（取决于 Harness 复杂度，而非项目大小）。
- 60% 的确认漏洞可通过 KLEE 生成的种子在 OSS-Fuzz 中复现。

5. 意义与影响 (Significance)

突破符号执行的可扩展性瓶颈：Sailor 成功解决了符号执行在大型项目中“无法自动构建 Harness"的核心痛点，使其能够应用于百万行级代码库。
多技术融合的新范式：证明了将静态分析（广度）、LLM（推理与合成）、符号执行（深度与精确性）和具体执行（真实性）有机结合，能产生"1+1+1+1 > 4"的效果。
实际漏洞发现能力：在 Binutils、FFmpeg、libxml2 等关键基础设施项目中发现了大量真实存在的 0-day 漏洞，展示了该技术在现实世界安全审计中的巨大潜力。
方法论的通用性：虽然当前基于 CodeQL/KLEE/GPT-5，但其流水线设计是解耦的，可轻松适配其他静态分析工具、LLM 模型或符号执行引擎。

总结：Sailor 代表了自动化漏洞检测领域的一个重要里程碑，它通过智能编排多种技术，将符号执行从一种需要专家手动干预的研究工具，转变为一种可规模化应用于工业级代码库的自动化漏洞发现系统。