【论文阅读】Gordian: Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

3.1 从一个简单的非线性约束开始#

论文 Figure 4 给出了下面这个例子：

1
int hard_func(int x) {
2
    return (x * x + 6) % 97;
3
}
4

5
int main(void) {
6
    int a = symbolic_input();
7

8
    int b = hard_func(a);
9

10
    if (b == 42) {
11
        assert(a > 20);
12
    }
13
}

这里用 symbolic_input() 表示符号输入，是为了方便阅读；论文原图使用符号变量 $\alpha$。

假设我们想探索 b == 42 且 a > 20 的路径，那么需要求解：

困难在于第一个约束包含平方和取模。这个小例子不意味着 Z3 一定解不了，而是用于说明更复杂的 Solver-hostile 函数可以如何处理。

Gordian 的想法是：既然正向求解 hard_func(a) == 42 可能很麻烦，能不能生成一个反向函数？也就是已知：

1
b = 42;

反过来求出可能的 a。

对于这个例子：

可以找到两个模 97 意义下的根：

需要特别注意，6 和 91 是模 97 的剩余类代表，不是原始无界整数域上的全部解。论文示例的逆向函数只搜索 0..96，因此生成的是候选值。

再结合：

就可以选取 $a = 91$。最终：

这里真正重要的不是数学计算，而是求解方向发生了改变。

传统做法是让 Solver 直接处理整个复杂函数。Gordian 则让 LLM 生成一个类似这样的函数：

1
void f_inv(int b, int *results) {
2
    int count = 0;
3

4
    int t = (b - 6) % 97;
5
    if (t < 0)
6
        t += 97;
7

8
    for (int a = 0; a < 97; a++) {
9
        if ((a * a) % 97 == t) {
10
            results[count++] = a;
11

12
            if (count == 2)
13
                break;
14
        }
15
    }
16
}

这段代码的含义就是：

1. 根据目标输出 b 计算需要满足的模平方条件。
2. 在一个有限候选域内搜索可能的 a。
3. 把候选输入交还给 Gordian。
4. 继续与原程序其他位置的路径约束进行协调。

代码本身并没有什么高级算法，核心是把求解困难函数的任务转换成具体程序搜索候选输入。

当然，真正的技术难点还在后面。

3.2 为什么只生成逆函数还不够？#

假设我们有一个困难函数：

程序前面有一个条件：

程序后面还有一个条件：

想要到达目标位置，必须同时满足：

LLM 可以通过逆函数，根据满足后置条件的 y 计算候选 x。但是这个 x 不一定满足前面的约束。

这就是关键问题：局部逆向计算只解决了函数附近的约束，不能保证整条程序路径的可行性。

因此，Gordian 设计了双向约束传播（Bidirectional Constraint Propagation）。

它的思路是：把困难函数两侧的约束暂时拆开求解，再通过正向和逆向计算，让两边产生的候选值逐步靠近。

3.3 Havoc：先把困难函数的输入输出关系断开#

原来的程序：

1
int b = hard_func(a);

在符号执行时，Gordian 暂时将其替换为：

1
int b = fresh_symbolic_value();

这类操作在程序分析中一般称为 havoc。

原来有 $b=f(a)$，经过替换以后：

其中 $\beta$ 是一个全新的符号变量。

也就是说，KLEE 暂时不需要理解 hard_func 是怎么计算的。它可以单独探索后面的逻辑：

1
if (b == 42) {
2
    assert(a > 20);
3
}

于是求解器可以得到：

以及：

此时的路径约束确实容易解多了。但是这里引入了一个很严重的问题。

b 和 a 之间的真实关系被断开了。

Solver 可以随便选择一个满足 a > 20 的值，比如 a = 30，同时认为 b = 42。可真实程序里 hard_func(30) 不一定等于 42。

所以 havoc 只是暂时绕开了困难计算，并没有真正完成求解。接下来必须把这条关系补回来。

3.4 双向约束传播：让前后约束逐步对齐#

论文的 Figure 5 给出了完整算法。

根据论文 Figure 5 简化的双向传播流程。实际实现还包括后置约束优化、可满足性检查及失败退出条件。

Step 1：求解 Suffix Constraint。

先只考虑困难函数后面的约束：

求出一个目标输出 $y_0$。

Step 2：执行逆函数。

调用 LLM 生成的：

现在得到一个可能让困难函数产生目标输出的输入。

Step 3：利用前置约束修正输入。

检查：

如果不满足，就不能直接使用这个值。Gordian 调用优化求解器（Optimization Modulo Theories, OMT），寻找一个既满足前置条件，又尽量接近原候选值的输入：

这里论文针对单个数值变量使用 L1 距离。如果涉及多个变量，直接优化数值距离可能比较昂贵，于是会使用 Partial MaxSAT，尽量保留更多原来的变量赋值，只修改必要的部分。

Step 4：正向执行真实函数，再修正后置状态。

有了 $x_1$，重新执行真实函数：

然后根据实际输出 $y_1$，在满足 Suffix Constraint 的候选空间中进行优化。

如果两侧约束已经对齐，就可以生成测试输入。否则继续：

反复进行 Refinement。

从直觉上理解，就是：后面的约束告诉我们需要什么输出，逆函数告诉我们可能需要什么输入，前面的约束再告诉我们这个输入是否合法。

如果不合法，就调整输入，重新计算输出，再看看还能不能满足后面的条件。

两边不断调整，尝试找到一个共同满足全部条件的解。

不过，这个过程是启发式优化，并不保证一定收敛。如果预算耗尽或者近似误差太大，可能无法找到可行输入，即使目标路径实际上是可达的。

4.1 先把 sin 和 cos 暂时符号化#

Gordian 选择困难片段：

1
s = sin(x);
2
c = cos(x);

将其替换为两个新符号：

这样后面的分支就变成：

对于 SMT Solver 来说，这比直接处理完整三角函数关系要容易得多。

Solver 可能返回：

显然 $10\times(-1)<0$，后置约束满足。

但这里有一个问题。对于真实的 sin 和 cos：

因此 (10, -1) 根本不可能是真实的三角函数输出。

原因很简单：前面通过 havoc 暂时删掉了 s、c 与 x 的联系。

Solver 给出的后置状态只满足局部路径条件，不一定满足原始函数语义。

4.2 LLM 生成近似逆函数#

Gordian 让 LLM 生成一个逆向搜索函数。

原论文使用黄金分割搜索（Golden-section Search），寻找使下面误差尽可能小的 x：

这个设计很巧。

因为对于任意输入的目标 (α, β)，都不保证存在严格的逆。

于是这里干脆不要求一定求出真正的逆函数，而是寻找一个输出尽量接近目标状态的输入。

对于 (10, -1)，论文得到近似值：

但是：

不满足前面的约束。

4.3 利用前置条件修正输入#

Gordian 现在不再重新让 LLM 想一个输入，而是直接调用优化求解器：

满足：

于是得到：

然后真正执行：

1
s = sin(2.0);
2
c = cos(2.0);

得到近似：

因此 $s\times c<0$，同时 $|x|\ge2$，前后的约束终于对齐了。

这时候再把 x = 2.0 放回原始程序执行，确认能否真实到达目标分支。

这就是 Gordian 的 Code Inversion 真正解决的问题：

不是单纯生成一个逆函数，而是用逆函数在困难代码两侧传递候选状态，再借助 SMT/OMT 修正这些状态，直到满足整条执行路径的约束。

这一点比简单地让 LLM 猜一个满足三角函数条件的输入更重要。

6.1 为什么完全符号化的 Heap 很难探索？#

考虑论文 Figure 2 的简化 Skiplist：

1
typedef struct SNode {
2
    int val;
3
    char *name;
4

5
    struct SNode *lvl0;
6
    struct SNode *lvl1;
7
} SNode;

其中：

• lvl0 指向普通链表中的下一个节点。
• lvl1 是高层跳跃指针，可以跨过部分节点。
• val 和 name 保存节点的数据。

现在有一个函数：

1
int proc_if_ring(SNode *h, SNode *g) {
2
    SNode *a = h ? h->lvl0 : NULL;
3
    SNode *b = a ? a->lvl0 : NULL;
4
    SNode *c = b ? b->lvl0 : NULL;
5
    SNode *d = c ? c->lvl0 : NULL;
6

7
    if (!h || !a || !b || !c || !d)
8
        return 0;
9

10
    if (d != h)
11
        return 0;
12

13
    if (h->lvl1 != b ||
14
        a->lvl1 != c ||
15
        b->lvl1 != d ||
16
        c->lvl1 != a)
17
        return 0;
18

19
    SNode *g1 = g ? g->lvl0 : NULL;
20
    SNode *g2 = g1 ? g1->lvl0 : NULL;
21

22
    if (g2 != h)
23
        return 0;
24

25
    return proc_ring_values(h);
26
}

我们希望到达：

1
return proc_ring_values(h);

这要求传入的数据结构满足一系列非常具体的条件。

首先，四个节点必须构成一个环：

其次，lvl1 还必须满足：

最后，g 沿着 lvl0 走两步，还必须回到 h。

假设所有节点和指针都是 Symbolic 的。

那么 KLEE 就需要探索不同的节点别名关系、空指针情况、环形结构以及多层指针组合。

这里的问题不是某一个判断特别难，而是能够构造出来的 Heap 形状实在太多了。

大量探索可能浪费在无效链表、断裂节点、错误环结构上。

论文中，普通 KLEE 在 10 分钟的限制内没有到达目标函数。

6.2 Gordian：直接生成具有语义的数据结构#

Gordian 让 LLM 分析 SNode 结构以及 proc_if_ring 中的判断，然后生成一个专门构造 Heap 形状的函数：

1
void constrain_heap(
2
    SNode *n0,
3
    SNode *n1,
4
    SNode *n2,
5
    SNode *n3,
6
    SNode **h,
7
    SNode **g
8
) {
9
    switch (xi) {
10
        case 1:
11
            /* broken chain */
12
            break;
13

14
        /* other topology cases */
15

16
        case 5:
17
            n0->lvl0 = n1;
18
            n1->lvl0 = n2;
19
            n2->lvl0 = n3;
20
            n3->lvl0 = n0;
21

22
            n0->lvl1 = n2;
23
            n1->lvl1 = n3;
24
            n2->lvl1 = n0;
25
            n3->lvl1 = n1;
26

27
            *h = n0;
28
            *g = n2;
29
            break;
30
    }
31
}

这里的 xi 表示一个新的符号化拓扑选择变量；代码根据论文示例做了精简。

当 xi == 5 时，Gordian 构造的就是能够满足目标检查的 Ring。

根据论文 Figure 2 整理的 Ring Shape 示意。蓝色表示 lvl0 的环，橙色虚线示意 lvl1 的跨节点连接关系，具体关系以代码中的赋值为准。

这套结构就满足 d == h 以及所有 lvl1 判断。

同时设置：

1
*g = n2;

因为：

1
n2->lvl0 == n3
2
n3->lvl0 == n0

所以从 g 开始沿 lvl0 走两步，刚好回到 h。

这样一来，程序就能够到达 proc_ring_values(h)。

论文对这个例子的报告是：使用 Gordian 后，可以在 2 秒内覆盖目标函数以及 proc_ring_values 的全部分支。

6.3 为什么不直接把所有字段都具体化？#

这是 Semantic Heap Partitioning 比较关键的设计。

它并不是让 LLM 生成一整个完全确定的数据结构。

对于 Ring 而言，Gordian 只固定必要的指针连接关系。

例如：

1
n0->lvl0 = n1;
2
n1->lvl0 = n2;
3
n2->lvl0 = n3;
4
n3->lvl0 = n0;

但节点中的 n0->val、n1->val、n2->val、n3->val 以及相关数据字段，仍然可以保留为 Symbolic。

原因很简单。

我们现在已经知道程序必须接收一个 Ring 才能继续执行，那就没必要让 Solver 再花大量时间探索链表结构。

但是进入 proc_ring_values(h) 以后，可能还需要探索：

1
if (h->val == 1337) {
2
    trigger();
3
}

如果提前把 val 也写死，就可能错过这个分支。

因此 Gordian 固定的是：Shape（结构）；保留的是：Contents（数据内容）。

这就形成了论文所谓的 Semantic Topology：部分具体、部分符号化的 Heap 配置。

其本质是利用 LLM 的程序语义理解能力，对原本庞大的 Heap 搜索空间进行有意义的划分。

但这里也存在覆盖范围上的取舍：LLM 没有生成的结构形状，可能就不会被探索到。它是一种搜索空间约束，并不是完整的 Heap 状态枚举。

7.1 实验环境#

Gordian 基于 KLEE 实现，使用 Z3 作为求解器，并在涉及浮点操作时使用 KLEE-Float。

实验运行在 Ubuntu 24.04.3 LTS、Intel Core Ultra 7 258V、32 GiB RAM 的机器上。论文给每个工具配置分配了 36 小时的 Wall-clock 预算。

LLM Backend 包括 GPT-5、Claude 3.7 和 DeepSeek-Chat。

主要测试对象如下：

Baseline 包括 KLEE-STP、KLEE-Z3、KLEE-Float-Z3，以及 LLM-based 的 ConcoLLMic 和 Cottontail。

7.2 RQ1：能不能真正解决 Solver-hostile 的 Logic Bomb？#

LogicBombs 中共有 53 个 Logic Bomb，每个程序包含两条 Critical Path，因此一共 106 条 Critical Path。

论文 Table 1 的部分结果：

这里最有意思的一点是，Gordian 并不需要让 LLM 从头到尾推理整个路径。

它只要成功跨过那个最困难的程序片段，剩下的约束仍然由 KLEE 负责处理。

论文 Figure 8 的消融实验还表明，三种 Ghost Code 覆盖的困难类型并不完全重合，因此三者组合比只使用一种方法更有效。

7.3 RQ2：在真实项目上还能不能有效？#

在 FDLibM 上，Gordian 达到最高 91.7% 的平均行覆盖率和 90.2% 的总体行覆盖率。

相比之下，ConcoLLMic 在 FDLibM 上的平均行覆盖率只有 37.2%–40.0%。

这说明 LLM 即使能够理解三角函数或数学公式，也不一定能够稳定地生成满足多层浮点路径条件的输入。

Gordian 则通过 Inversion 和 SMT 结合，把复杂数学片段与其他路径条件协调起来。

结构化输入程序的结果同样明显。以下采用论文 Table 3 中 GPT-5 Backend 的总体行覆盖率数据，并为 KLEE 选择相应项目上表现最好的传统配置：

为什么 libexpat、libyaml 这种程序适合 Gordian？

因为它们内部涉及大量状态对象、复杂输入结构和指针关系。

如果完全依赖符号执行遍历所有可能的输入和 Heap 结构，搜索空间非常大。

Semantic Heap Partitioning 可以提前选出一些有意义的结构，让 KLEE 把计算资源花在结构满足要求之后的程序行为上。

这里需要注意，论文报告的是 Coverage，而不是发现了多少真实漏洞。因此这些结果支持“能够探索更多代码路径”，不能直接等同于“漏洞发现能力提升相同比例”。

7.4 RQ3：为什么 Gordian 的 Token 成本这么低？#

这一点也很值得注意。

论文统计了结构化输入 Benchmark 上的 Token 消耗：

使用 GPT-5 时，Gordian 消耗约 47 万 Token，而 ConcoLLMic 消耗约 1490 万 Token。

其实原因很直接。

ConcoLLMic 这类方法会持续调用 LLM 理解执行过程、分析约束并尝试生成输入。

Gordian 则只在识别出 Solver-hostile 代码片段时调用 LLM。

生成一次 Ghost Code 后，后续的大部分路径探索仍然交给符号执行引擎。

论文报告 LLM 调用约占 Gordian 总执行时间的 9.2%。

LLM 在这里不是执行引擎，而是一个按需调用的程序转换组件。

这也是它能够降低 Token 开销的根本原因。

7.5 RQ4 / RQ5：覆盖率为什么呈阶梯式增长？#

论文 Figure 10 展示了 Coverage 随时间变化的趋势。

普通 KLEE 在运行初期快速获得一部分 Coverage，随后逐渐进入 Plateau。

原因是容易探索的路径很快覆盖完了，剩下的路径可能涉及复杂约束或数据结构。

而 Gordian 的覆盖率曲线呈现出明显的阶梯状。

当某个 Ghost Code 成功生成并解除一处求解瓶颈之后，原本被挡住的一片代码区域会突然变得可达。

于是 Coverage 出现明显增长。

这一点很符合 Gordian 的设计逻辑。

它并不一定每分钟都比 KLEE 多探索很多路径，而是通过解决关键阻塞点，打开新的程序区域。

论文还在 libyaml 上分析了不同方法覆盖代码的重合情况。Gordian 独有的覆盖行数占全部已覆盖行数的 19.2%，说明它的改进并不只是重复覆盖其他方法已经访问过的代码。