💻 computer science

Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

本文提出了 Gordian 框架，通过利用大语言模型选择性生成辅助幽灵代码来增强 SMT 求解器处理符号执行中“逻辑炸弹”等难题的能力，从而在显著提升代码覆盖率的同时大幅降低了 LLM 的 Token 消耗。

原作者： Dimitrios Stamatios Bouras, Sergey Mechtaev

发布于 2026-03-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Dimitrios Stamatios Bouras, Sergey Mechtaev

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

这篇论文介绍了一个名为 Gordian（戈耳狄俄斯）的新工具，它巧妙地结合了两种强大的技术：符号执行（一种像“上帝视角”一样分析代码的方法）和 大语言模型（LLM，也就是现在的 AI）。

为了让你轻松理解，我们可以把这段技术故事想象成**“一位经验丰富的侦探（符号执行）遇到了一位才华横溢但偶尔会犯迷糊的顾问（AI）”**。

1. 侦探的困境：遇到“逻辑炸弹”

想象一下，侦探（符号执行引擎）正在调查一个复杂的案件（程序代码）。他的工作方式是：

推演所有可能性：他拿着一个放大镜，试图推演输入不同数据时，程序会走哪条路。
依靠逻辑计算器：他有一个超级严谨的逻辑计算器（SMT 求解器），用来验证每一步是否符合数学规则。

问题出在哪？
有些代码片段太复杂了，比如涉及极其高深的三角函数、复杂的数学公式，或者像迷宫一样的动态数据结构（比如链表、树）。

对于逻辑计算器来说，这些就像“天书”，它算不出来，或者算得慢到死机。
一旦遇到这些“逻辑炸弹”，侦探就卡住了，无法继续深入调查，导致很多隐藏的漏洞（Bug）被漏掉。

2. 纯 AI 方案的失败：聪明的顾问，糊涂的导航

最近，有人想：“既然计算器算不出来，不如直接请 AI 顾问来算吧！”

纯 AI 方案：让 AI 直接分析代码，猜测输入什么数据能触发某个分支。
结果：AI 很聪明，能看懂局部逻辑。但是，如果案件链条很长（比如需要连续通过 10 个检查点），AI 就会“记不住”前面的条件，或者在长链条中前后矛盾。它就像是一个只懂局部、缺乏全局观的向导，容易走错路。

3. Gordian 的绝招：给侦探配个“幽灵助手”

Gordian 没有选择二选一，而是想出了一个**“混合双打”的策略。它不替换侦探，而是给侦探配了一个“幽灵助手”**（Ghost Code）。

这个助手是由 AI 生成的，但它只干三件特定的事，而且干完就消失，不干扰侦探的全局推理：

绝招一：逆向工程（把“死胡同”变成“双向道”）

场景：侦探遇到一个复杂的数学公式，正向推演（从输入到输出）太难解。
AI 的作用：AI 帮侦探写了一段“反向代码”。
比喻：就像侦探在迷宫里迷路了，AI 帮他画了一张**“倒着走”的地图。侦探先看看终点想要什么结果，然后让 AI 写的代码倒着推**回来，告诉侦探：“如果你想要这个结果，输入大概应该是这个数。”
效果：侦探利用这个线索，结合自己严谨的逻辑，成功找到了正确的入口。

绝招二：找替身（用“简单模型”代替“复杂怪兽”）

场景：代码里有一个极其复杂的加密或数学函数，像一头难以驯服的怪兽。
AI 的作用：AI 写了一个**“替身”**（Surrogate）。这个替身长得像怪兽，行为也差不多，但内部逻辑非常简单，逻辑计算器能轻松算出来。
比喻：侦探要过一座摇摇欲坠的独木桥（复杂函数），AI 在旁边搭了一座坚固的简易桥（替身模型）。侦探先过简易桥探路，确认方向对了，再回头去验证真桥。
效果：既保留了关键信息，又让计算器能轻松工作。

绝招三：给迷宫画“分区图”（防止在无限空间里迷路）

场景：程序处理的是动态数据结构（比如链表），像是一个无限延伸的迷宫，侦探不知道从哪里开始探索，容易陷入“路径爆炸”（路太多走不过来）。
AI 的作用：AI 根据经验，帮侦探把无限的空间划分成几个有意义的“形状”（比如：环形的、直线的、断开的）。
比喻：侦探面对一片茫茫大海（无限内存），AI 递给他一张**“寻宝图”**，告诉他：“别乱游了，我们只重点检查这三个特定的岛屿形状。”
效果：侦探不再盲目探索，而是精准地检查最有价值的区域。

4. 为什么这个方案这么牛？

既严谨又灵活：侦探（符号执行）负责全局逻辑，确保每一步都严丝合缝；AI 助手只负责局部难点，提供灵感。
省钱又高效：
- 纯 AI 方案需要 AI 一直思考，消耗巨大的“算力”（Token 费用）。
- Gordian 只在最关键的时刻叫 AI 帮忙写几行代码，然后让侦探自己跑。
- 结果：论文数据显示，Gordian 找到的漏洞比传统方法多 52%~84%，比纯 AI 方法多 86%~419%，而且AI 的调用成本降低了 90% 以上！

总结

Gordian 就像是在一位严谨的数学家（符号执行）旁边，请了一位博学的老工匠（AI）。

遇到难题时，老工匠不直接替数学家算题（那样容易出错且慢），而是给数学家提供一个巧妙的解题思路或辅助工具（幽灵代码）。
数学家拿到工具后，结合自己严密的逻辑，瞬间就能解开以前解不开的“逻辑炸弹”。

这种方法既保留了数学的严谨性，又利用了 AI 的创造力，是目前解决复杂代码分析问题的一个非常聪明的“混合双打”方案。

论文技术总结：利用 LLM 生成的幽灵代码化解符号执行中的逻辑炸弹

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

符号执行（Symbolic Execution）是一种强大的程序分析技术，通过抽象输入、将程序行为编码为逻辑约束并利用 SMT 求解器进行分析。然而，其在实际应用中面临三大核心瓶颈：

求解器不友好的代码片段：涉及复杂计算（如非线性算术、三角函数、浮点运算）的代码会生成难以求解的 SMT 约束，导致求解失败。
精确建模困难：现实环境中的系统调用、网络通信等难以精确建模。
路径爆炸与堆空间无限性：动态内存分配和复杂的指针结构导致执行路径无限，且堆配置空间巨大。

现有的尝试利用大语言模型（LLM）替代 SMT 求解器的方法（如 ConcoLLMic, Autobug），虽然规避了求解器的不可判定性问题，但在处理深层执行路径时，由于 LLM 难以维持跨函数、跨状态的全局一致性推理，往往无法生成满足复杂约束的输入。

2. 方法论：Gordian 框架 (Methodology)

作者提出了 Gordian，一种混合符号执行框架。其核心思想是不替代 SMT 求解器，而是利用 LLM 在求解器受阻的特定环节生成轻量级的幽灵代码（Ghost Code），作为求解器的辅助工具。Gordian 在 KLEE 符号执行引擎上实现，主要包含三种 LLM 生成的幽灵代码策略：

2.1 困难代码片段的逆向与双向约束传播 (Inversion & Bidirectional Propagation)

问题：当代码片段（如三角函数计算）难以正向求解时，SMT 求解器无法推导输入。
方法：
1. LLM 识别困难片段 $f$ ，并生成其逆过程 $f^{-1}$ （例如使用黄金分割搜索法近似逆运算）。
2. 在符号执行中，将困难片段替换为新鲜符号变量（Havoc 语句）。
3. 双向传播：
  - 先求解后缀路径条件（Suffix Constraints）得到目标输出值。
  - 利用 LLM 生成的逆函数 $f^{-1}$ 将目标值逆向执行回推，得到候选输入。
  - 利用优化求解器（OMT）在满足前缀路径条件（Prefix Constraints）的前提下，寻找最接近候选输入的可行解。
4. 最终验证生成的输入是否确实触发目标分支。

2.2 求解器友好的代理模型 (Solver-Friendly Surrogates)

问题：某些片段无法完美逆向（如多对一映射、依赖外部状态）。
方法：LLM 生成一个简化的代理函数（Surrogate），该函数保留了原代码的关键行为（如分支逻辑），但将复杂的理论（如浮点运算、加密调用）替换为求解器友好的形式（如位向量、线性算术）。
验证：生成的测试用例会在原始程序上重新执行，以确保代理模型未引入错误路径（保证声性 Soundness）。

2.3 基于语义的堆空间划分 (Semantic Heap Partitioning)

问题：处理动态数据结构（如链表、跳表）时，指针别名和堆形状的组合导致路径爆炸。
方法：
1. LLM 根据领域知识识别出几种语义拓扑结构（Semantic Topologies），例如“长度为 3 的链表段”、“环形结构”等。
2. 生成幽灵代码 constrain_heap，在符号执行前根据一个符号变量 $\xi$ 选择特定的堆拓扑。
3. 该代码将堆约束为部分具体、部分符号化的结构（例如固定前几个节点的链接关系，但保持节点值符号化），从而在保留符号探索能力的同时，大幅减少无效的路径分支。

3. 关键贡献 (Key Contributions)

新颖的混合范式：提出了一种利用 LLM 生成辅助幽灵代码来增强 SMT 求解器的方法，而非完全用 LLM 替代求解器，兼顾了 LLM 的领域知识与 SMT 的全局精确推理能力。
三种实用的幽灵代码变体：
- 基于逆向的双向约束传播算法。
- 保留关键行为的求解器友好代理模型。
- 基于领域洞察的语义堆拓扑划分。
全面的评估与消融实验：在合成基准、数学库和真实结构化输入程序上进行了广泛测试，证明了各组件的有效性。

4. 实验结果 (Results)

研究在三个基准集上进行了评估：

LogicBombs（53 个合成程序，包含逻辑炸弹）：
- 覆盖率：Gordian 触发了 94.3% 的逻辑炸弹，比传统 KLEE（~~39%）提高了 138%，比纯 LLM 方法 ConcoLLMic（~~64%）提高了 47%。
- Token 效率：Token 使用量减少了 90-96%（平均 0.32M vs ConcoLLMic 的 3.07M）。
FDLibM（78 个数学库入口点，含复杂浮点运算）：
- 覆盖率：Gordian 实现了 91.7% 的平均行覆盖率，比 ConcoLLMic 提高了 183.5%，比最佳 KLEE 配置提高了 22%。
- 优势：证明了 LLM 难以单独处理长链浮点约束，而 Gordian 的双向传播有效解决了此问题。
结构化输入程序（libexpat, jq, bc）：
- 覆盖率：Gordian 在总覆盖率上比 KLEE 提高了 79-108%，比 ConcoLLMic 高出 9.7 倍，比 Cottontail 平均提高 86%。
- 原因：语义堆划分有效处理了复杂的解析逻辑和数据结构。

总结数据：Gordian 在平均覆盖率上比传统符号执行提高 52-84%，比 LLM 技术提高 86-419%，同时 Token 消耗降低 90-96%。

5. 意义与局限性 (Significance & Limitations)

意义

实用性：证明了在真实世界代码库中，LLM 与符号执行结合的巨大潜力，特别是处理“逻辑炸弹”和深层路径时。
成本效益：通过仅在关键难点使用 LLM，大幅降低了推理成本，解决了纯 LLM 方法在长路径推理上的不稳定性。
声性保证：通过“生成 - 验证”机制（在原始程序上重跑），确保了即使 LLM 生成的幽灵代码有误，也不会导致错误的分析结果（仅影响效率）。

局限性

集成复杂度：目前需要重新编译目标程序以注入幽灵代码，对于大型复杂构建系统可能较繁琐。
LLM 幻觉：虽然通过验证保证了声性，但错误的幽灵代码可能导致漏报（Missed Paths）。
全局依赖：对于复杂性源于全局不变量或难以建模的环境交互的程序，效果可能受限。
收敛性：双向约束传播算法基于启发式优化，不保证数学上的收敛。

未来方向

将 LLM 辅助模块更深地集成到符号执行引擎内部（如 KLEE），实现在线检测和动态委托，并构建可复用的求解器友好模型库。