【论文阅读】Agentic Concolic Execution: 让 LLM 接管 Concolic Execution 的建模与求解

普通模糊测试在做什么？#

假设程序非常简单：

1
int foo(int x) {
2
    if (x == 1234567) {
3
        trigger_bug();
4
    }
5
    return 0;
6
}

覆盖率引导模糊测试（Coverage-guided Fuzzing）会不断修改已有输入：

1
1
2
42
3
100
4
...

希望某次变异恰好得到：

1
1234567

如果条件藏在很深的程序路径中，仅靠随机变异往往很难命中。

符号执行怎么处理？#

符号执行（Symbolic Execution）不会一开始就把 x 固定成具体数字，而是把它视为符号变量：

1
x = α

执行到：

1
if (x == 1234567)

之后，可以得到路径条件：

1
α == 1234567

如果目标是进入 true 分支，求解器只需要找到：

1
α = 1234567

然后就可以生成对应的具体输入。

具体-符号执行进一步把两者结合起来#

具体-符号执行可以理解成“具体执行 + 符号执行”。

一次典型流程是：

1
初始输入 I0
2
    │
3
    ▼
4
具体执行
5
    │
6
    ├── 程序输出 O
7
    └── 执行轨迹 T
8
              │
9
              ▼
10
           符号化
11
              │
12
              ├── 路径约束 PC
13
              └── 符号状态 σ
14
                       │
15
                       ▼
16
                   翻转约束
17
                       │
18
                       ▼
19
                     求解
20
                       │
21
                       ▼
22
                   新输入 I'
23
                       │
24
                       └──────────────┐
25
                                      ▼
26
                                   工作队列

论文中的算法可以概括成：

1
1  P~ ← INSTRUMENT(P)
2
2  WorkList ← {I0}
3

4
3  while WorkList != ∅:
5
4      I ← SELECT_NEXT(WorkList)
6
5      (O, T) ← EXECUTE(P~, I)
7
6      (PC, σ) ← SYMBOLIZE(T)
8
7      PC' ← FLIP_CONSTRAINT(PC)
9
8      I' ← SOLVE(PC', σ)
10
9      WorkList ← WorkList ∪ {I'}

真正关键的是第 6～8 步：

1
具体执行轨迹
2
    ↓
3
符号约束
4
    ↓
5
翻转目标条件
6
    ↓
7
求解新的输入

而这三步恰好是传统工具最容易遇到复杂度问题的地方。

C1：首先得理解程序究竟在做什么#

例如：

1
float start = atof(argv[1]);
2

3
unsigned temp;
4
memcpy(&temp, &cur, sizeof(float));
5
temp++;
6
memcpy(&cur, &temp, sizeof(float));

这里如果只从源码表面理解，很容易把它看成：

1
cur = cur + 1

但实际执行的是位级操作，并非普通浮点加法。

代码执行的是：

1
float
2
  │
3
  ▼
4
通过 memcpy 读取原始位
5
  │
6
  ▼
7
unsigned + 1
8
  │
9
  ▼
10
重新解释为 float

这里涉及 IEEE-754 浮点数的位表示。单精度浮点数使用固定的 32 位表示：

1
┌─────────┬───────────┬───────────────────────┐
2
│ Sign    │ Exponent  │ Fraction              │
3
│ 1 bit   │ 8 bits    │ 23 bits               │
4
└─────────┴───────────┴───────────────────────┘

因此，传统符号执行器需要同时理解：

• memcpy 的内存语义；
• float 与 unsigned 之间的类型转换；
• IEEE-754 的浮点表示；
• 位向量运算；
• atof 的行为。

像 atof、memcpy 这样的函数也需要进入符号模型。

传统工具通常有几种处理方式：

1. 将函数实现纳入符号执行；
2. 为函数手写符号模型；
3. 将部分参数固定为具体值。

第一种方式会显著增加实现规模，第二种需要长期维护大量模型，第三种则可能丢失部分路径。

C2：模型建立之后，求解器还要面对低层约束#

现代程序的路径约束可能同时包含：

1
大量变量
2
+
3
大量条件
4
+
5
位向量
6
+
7
数组
8
+
9
指针
10
+
11
浮点数
12
+
13
字符串
14
+
15
外部函数

传统执行器往往会把程序实现机械地转换成低层公式。

于是源码只有几十行：

1
for (...) {
2
    memcpy(...);
3
    temp++;
4
    memcpy(...);
5
}

最后形成的约束却可能远比源码复杂。

论文抓住的关键点是：

程序实现层面的复杂度，并不一定等于程序语义层面的复杂度。

对于前面的浮点循环，从程序语义上看，真正需要回答的问题其实非常简单：

1
start 和 end 之间有多少个可表示的单精度浮点数？

如果能够直接把低层实现总结成这个语义问题，后面的求解就可能简单很多。

这里的 +1 到底是什么意思？#

代码每次执行：

1
当前浮点数
2
    ↓
3
读取 IEEE-754 原始位
4
    ↓
5
原始位 + 1
6
    ↓
7
重新解释成浮点数

因此它实际上是在访问相邻的 IEEE-754 单精度可表示值。

这和普通的：

1
cur += 1;

完全是两回事。

初始输入为什么没有触发漏洞？#

论文给出的初始输入是：

1
start = 1.00
2
end   = 1.00001

在 1.0 附近，相邻单精度浮点数的间隔约为：

而：

因此大约可以跨越：

个间隔。

所以 [1.0, 1.00001) 中存在 84 个可表示的单精度浮点数，程序最终得到：

1
cnt = 84

于是：

1
if (cnt <= 20)

条件不成立，漏洞分支不会执行。

传统具体-符号执行会得到什么？#

设：

1
start = α
2
end   = β

定义：

1
f(x)

表示“读取 x 的 IEEE-754 位表示，加 1 后再解释为浮点数”。

经过 i 次循环：

对应的符号状态可以写成：

假设程序需要执行 n 次循环才能让 cur 等于 end，路径约束可以表示为：

如果希望探索漏洞分支，就需要把最后一个条件翻转为：

单独看最后这个条件很简单，真正困难的是：

因为 f 的实现中包含 memcpy、内存操作、类型转换、IEEE-754 语义、atof 以及循环执行。

于是，一个从语义上很简单的问题，经过传统符号化之后，可能变成大量低层约束。

这正是 C1 和 C2 叠加产生的效果：

• C1：这些底层操作如何建立完整的符号模型？
• C2：建立之后，这么复杂的约束如何高效求解？

论文由此引出 CONCOLLMIC。

变化一：符号化从“执行过程中同步完成”变成“执行之后再完成”#

传统具体-符号执行通常会在程序执行过程中不断构造符号表达式：

1
执行一条语句
2
    ↓
3
构造对应符号表达式
4
    ↓
5
更新路径约束
6
    ↓
7
继续执行

CONCOLLMIC 的思路是：

1
先完成具体执行
2
    ↓
3
得到完整执行轨迹
4
    ↓
5
生成执行抽象
6
    ↓
7
再让大语言模型理解这次执行

这样，语言和运行时相关的细节主要集中在前面的插桩阶段，后面的语义推理则建立在统一的执行信息之上。

变化二：约束不再限定为 SMT 公式#

论文允许约束处在不同的抽象层级，例如：

• 自然语言；
• 编程语言；
• SMT 公式。

因此，对于一个问题，大语言模型可以判断：

1
这个约束用自然语言描述已经足够清楚

也可以判断：

1
这个问题结构比较规整，直接交给 Z3 更合适

这也是论文所谓“任意抽象层级”的核心含义。

源码块与控制流追踪#

论文把源码划分成一个个源码块（Source Block）。

例如：

1
for (...) {
2
    ...
3
}

可以被插入：

1
enter count 1
2

3
for (...) {
4
    ...
5
}
6

7
// exit count 1

一般形式为：

1
enter func_name block_no
2
original_code
3
// exit func_name block_no

每个源码块由：

1
(func_name, block_no)

唯一标识。

再通过：

1
<file_path, block_id>

映射到具体源码行。

例如论文图 1 中的映射关系：

程序执行后，就可以得到类似这样的轨迹：

1
[src/count.c] enter main 1
2
[src/count.c] enter count 1
3
[src/count.c] enter count 1
4
...

这样，不同语言的程序最终都可以被描述成统一的“执行过哪些源码块”。

为什么不直接依赖 AST 或编译器分析？#

论文希望保持较强的语言无关性。

如果分别为：

1
C
2
C++
3
Python
4
Java
5
Go
6
...

实现独立的解析器和编译器级插桩逻辑，系统很快又会重新陷入传统程序分析工具的维护成本。

因此论文让大语言模型负责：

1
源码
2
  ↓
3
大语言模型生成插桩
4
  ↓
5
插桩后的源码

但这里并没有完全把正确性寄托在大语言模型上。

论文采用了非常简单的 enter/exit 结构，并配套确定性的验证器。

例如：

1
enter A
2
    enter B
3
    exit B
4
exit A

是合法嵌套。

而：

1
enter A
2
    enter B
3
exit A
4
exit B

则会被判定为错误。

如果发现错误，系统会把：

1
哪个源码块
2
哪一行
3
哪个 enter/exit 不匹配

反馈给大语言模型，让它重新生成插桩。

这个设计的价值在于：

大语言模型负责生成，确定性验证器负责拦截明显错误。

大文件如何处理？#

大文件不能一次性完整交给大语言模型。

论文因此把文件拆成多个代码块：

1
File
2
 ↓
3
Chunk 1
4
Chunk 2
5
Chunk 3
6
...

默认分块大小为：

1
800 lines

并尽量在函数边界处分割。

整体流程可以概括为：

1
读取源码文件
2
    ↓
3
按规模切分
4
    ↓
5
逐块生成插桩
6
    ↓
7
验证 enter/exit 是否匹配
8
    ↓
9
错误则反馈并重新生成
10
    ↓
11
合并结果
12
    ↓
13
建立源码块到源码行的映射

这样设计的核心目的在于控制上下文规模，同时保证插桩过程可验证。

执行抽象：真正解决上下文规模的问题#

插桩完成后，每次运行只需要执行程序，不需要再次调用大语言模型。

例如输入：

1
(1.00, 1.00001)

会产生大量执行轨迹。

如果把完整轨迹原样交给大语言模型，信息量仍然很大。

因此论文进一步生成执行抽象（Execution Abstraction）。

图 3（论文第 5 页）：执行抽象的目标是保留当前执行真正涉及的程序逻辑，同时删除没有执行到的代码，减少后续推理的上下文负担。

例如：

1
函数调用链：
2
[src/count.c] main → [src/count.c] count

以及当前执行涉及的源码：

1
#define FLOATS_BETWEEN_BUG 20
2
int cnt = 0;
3

4
int count(float start, float end) {
5
    for (float cur = start; cur != end; cnt++) {
6
        unsigned temp;
7
        memcpy(&temp, &cur, sizeof(float));
8
        temp++;
9
        memcpy(&cur, &temp, sizeof(float));
10
    }
11

12
    if (cnt <= FLOATS_BETWEEN_BUG) {
13
        // 未执行的 16-17 行被删除。行覆盖率：0/2
14
    }
15
}
16

17
int main(int argc, char **argv) {
18
    float start = atof(argv[1]), end = atof(argv[2]);
19
    __assume__(start < end);
20
    count(start, end);
21
}

这个循环实际上是在逐个遍历 start 和 end 之间的单精度浮点数表示值。

执行抽象的核心是根据一次具体执行结果，对原程序进行裁剪。 以 start = 1.00、end = 1.00001 为例，程序首先从 start 开始，通过修改浮点数的 IEEE-754 位表示逐步得到下一个可表示的浮点数，并持续执行直到 cur == end。这次执行共遍历了 84 个浮点数，因此 cnt 最终为 84。随后判断 cnt <= 20，结果为假，条件分支内部的代码从未执行。基于执行覆盖信息，执行抽象会将该未执行代码块删除，并保留其覆盖信息。最终得到的程序只包含本次具体执行实际涉及的控制流。

1
输入：测试输入 start = 1.00，end = 1.00001
2

3
函数 count(start, end)：
4
    cnt ← 0
5
    cur ← start
6

7
    当 cur ≠ end 时：
8
        将 cur 的 IEEE-754 二进制表示解释为无符号整数 temp
9
        temp ← temp + 1
10
        将 temp 的二进制表示重新解释为浮点数 cur
11

12
        cnt ← cnt + 1
13

14
    如果 cnt ≤ 20：
15
        执行漏洞相关代码
16

17
主函数 main：
18
    start ← 将第一个命令行参数转换为浮点数
19
    end ← 将第二个命令行参数转换为浮点数
20

21
    假设 start < end
22

23
    调用 count(start, end)

这里一个很重要的细节是：

删除的是没有执行到的源码块，已经执行的代码仍然保留。

因此执行抽象仍然保留：

• 当前已经执行过的程序逻辑；
• if、for 等控制结构；
• 全局定义和变量声明；
• 当前覆盖率信息；
• 函数调用关系。

最终得到的是一个面向后续推理的程序视图：

1
具体执行轨迹
2
    ↓
3
执行抽象
4
    ↓
5
“这次运行实际上走了什么”

路径约束总结智能体：先确定要探索哪里#

它接收：

1
当前输入 I
2
+
3
当前执行抽象 EA(P~ | I)

然后通过一组动作逐步完成分析：

因此它的工作方式更接近一个循环：

1
查看当前执行
2
    ↓
3
判断信息是否足够
4
    ↓
5
缺少源码？
6
 ├─ 是 → 请求源码
7
 └─ 否
8
    ↓
9
选择尚未覆盖的目标分支
10
    ↓
11
分析分支条件
12
    ↓
13
总结路径约束
14
    ↓
15
继续寻找其他目标分支
16
    ↓
17
结束

论文还允许一次执行选择多个目标分支。

原因很简单：当前执行抽象本身已经产生了成本，多选几个目标分支可以让这一轮上下文被充分利用。

为什么要先选分支，再总结约束？#

这是一个容易被忽略、但很关键的设计。

传统具体-符号执行通常是：

1
执行
2
 ↓
3
对整条路径进行符号化
4
 ↓
5
选择某个约束进行翻转

CONCOLLMIC 则采用：

1
执行
2
 ↓
3
确定目标分支
4
 ↓
5
针对目标分支总结约束

原因在于：一旦过早把所有实现细节提升到高层语义，例如：

1
“让 start 和 end 之间最多有 20 个可表示的浮点数”

这个条件非常容易理解，但对应源码中的哪个分支可能已经不够明确。

因此论文保留了一个实现级的定位过程：

先确定“要去哪里”，再决定“用什么抽象表达怎么到达那里”。

再跑一次浮点例子#

图 4（论文第 8 页）：左侧是路径约束总结智能体，右侧是约束求解智能体。整个流程可以理解成“查看执行 → 找目标分支 → 提炼条件 → 构造输入 → 重新执行验证”。**

1
1.0
2
1.00001

1
cnt = 84

1
if (cnt <= FLOATS_BETWEEN_BUG) {
2
    printf("BUG triggered!");
3
}

1
CODE_REQUEST

1
src/count.c:16-17

1
printf("BUG triggered!");
2
return -1;

1
CHOOSE_BRANCH

1
if (cnt <= FLOATS_BETWEEN_BUG) => true

1
lines_to_cover:
2
src/count.c:16-17

1
SUMMARIZE

1
a) 程序需要两个命令行参数 start 和 end。
2

3
b) 两个参数都必须是合法的浮点数，
4
   且 start < end。
5

6
c) [start, end) 中的不同 IEEE-754
7
   单精度可表示浮点数数量必须 <= 20。

约束求解智能体：重点是“如何构造”#

约束求解智能体可以使用：

这意味着大语言模型不需要自己完成所有精确计算。

典型过程可以是：

1
分析约束
2
    ↓
3
需要精确计算？
4
    ↓
5
执行 Python
6
    ↓
7
得到计算结果
8
    ↓
9
继续推理
10
    ↓
11
需要 SMT？
12
    ↓
13
查询 Z3

整个过程更接近：

1
分析
2
 ↓
3
提出假设
4
 ↓
5
调用工具
6
 ↓
7
检查结果
8
 ↓
9
修正

浮点例子具体怎么求？#

在 1.0 附近，相邻单精度浮点数之间的距离约为：

如果最多允许 20 次相邻浮点数转换，则范围大约为：

论文进一步让智能体生成代码，精确计算下一个单精度可表示浮点数，而不是依赖近似估算。

伪代码可以表示为：

1
def next_float(f):
2
    # 计算下一个 IEEE-754 单精度浮点数
3
    ...
4

5
current = 1.0
6

7
for _ in range(19):
8
    current = next_float(current)
9

10
print(next_float(current))

最终得到：

1
1.000002384185791

于是可以构造：

1
start = 1.0
2
end   = 1.000002384185791

这时程序执行 20 次循环，最终：

1
cnt <= 20

成立，漏洞分支被覆盖。

这里真正重要的设计在于：

大语言模型识别出问题的语义是“寻找下一个可表示的单精度浮点数”，再把精确计算交给代码执行工具。

最后还要重新执行验证#

大语言模型总结路径约束时仍然可能出错，因此系统不会直接相信它生成的结果。

得到新输入：

1
I'

之后重新执行：

1
具体执行
2
    ↓
3
新的执行轨迹
4
    ↓
5
覆盖率 / 目标源码行
6
    ↓
7
验证

如果目标源码行确实被覆盖，就保留这个输入。

如果没有命中目标分支，但带来了新的全局覆盖率，也可以保留。

因此形成一个闭环：

1
智能体提出方案
2
      ↓
3
具体执行
4
      ↓
5
验证结果
6
      ↓
7
成功 → 加入工作队列
8
失败 → 丢弃

这也是论文处理大语言模型不可靠性的重要工程手段。

为什么这种架构比“一次性让 LLM 给答案”更稳？#

论文实际上采用了三层约束。

1
具体执行
2
+
3
执行轨迹
4
+
5
覆盖率
6
+
7
源码

1
测试输入
2
→ 具体执行
3
→ 覆盖率检查

1
EXECUTE_CODE
2
QUERY_SMT
3
CODE_REQUEST

1
大语言模型：
2
语义理解、规划、抽象、工具编排
3

4
程序运行时：
5
提供真实执行结果
6

7
Python / Z3：
8
提供精确计算
9

10
验证器：
11
检查生成结果

案例：如何主动制造一次 malloc() 失败？#

目标代码：

1
void *bc_malloc(size_t size) {
2
    void *ptr = (void *)malloc(size);
3

4
    if (ptr == NULL) {
5
        // target branch
6
    }
7

8
    return ptr;
9
}

这个分支为什么难覆盖？

因为普通运行环境下：

1
malloc(size)

通常会成功。

因此：

1
普通输入
2
  ↓
3
malloc 正常返回
4
  ↓
5
无法进入错误处理分支

仅靠输入变异，很难把运行时环境变成：

1
第 N 次 malloc 必须失败

路径约束总结智能体先提炼条件#

它可以得到：

1
条件 1：
2
程序必须调用 bc_malloc。
3

4
条件 2：
5
bc_malloc 内部的 malloc(size) 必须返回 NULL。

第二个条件已经从“输入应该是什么”转变成了：

1
运行时环境应该是什么？

约束求解智能体开始构造运行环境#

智能体可以推断：

可以通过替换 malloc 的运行时行为，让指定次数之后的分配直接返回 NULL。

于是生成一个包装器：

1
void* malloc(size_t size) {
2
    ...
3
    malloc_count++;
4

5
    if (malloc_count >= fail_after) {
6
        return NULL;
7
    }
8

9
    return real_malloc(size);
10
}

再通过：

1
gcc
2
  ↓
3
malloc_wrapper.so
4
  ↓
5
LD_PRELOAD
6
  ↓
7
启动 bc

把这个运行时环境注入目标程序。

图 6（论文第 11 页）：左侧是 malloc == NULL 的目标分支，右侧是智能体生成的包装器和 LD_PRELOAD 测试驱动程序。这个案例体现了系统的一个重要能力：目标不再局限于“生成一个输入文件”，还可以生成满足路径条件所需的运行环境。**

最终测试驱动程序大致执行：

1
compile_result = subprocess.run(
2
    ["gcc", "-shared", "-fPIC",
3
     "malloc_wrapper.c",
4
     "-o", "malloc_wrapper.so",
5
     "-ldl"]
6
)
7

8
env = os.environ.copy()
9
env["LD_PRELOAD"] = "./malloc_wrapper.so"
10

11
subprocess.run(
12
    ["./bc/bc", "non_existent_file.bc"],
13
    env=env
14
)

完整过程可以理解为：

1
发现目标分支
2
    ↓
3
理解条件：malloc 必须失败
4
    ↓
5
构造分配器包装器
6
    ↓
7
编译共享库
8
    ↓
9
设置 LD_PRELOAD
10
    ↓
11
启动目标程序
12
    ↓
13
指定次数后的 malloc 返回 NULL
14
    ↓
15
进入错误处理分支

因此，这里的测试生成对象实际上已经从“输入数据”扩展到了程序运行环境。

多语言系统为什么也能处理？#

论文还测试了：

• ultrajson：Python + C
• jansi：Java + C
• py4j：Python + Java
• protobuf-go：Go + C++

图 7（论文第 12 页）：四个跨语言项目都观察到了持续的内部行覆盖率增长。相对初始输入，论文报告的平均覆盖率增长分别为：ultrajson 3.5×、jansi 8.2×、py4j 1.9×、protobuf-go 1.9×。论文还使用前面的 GCov 实验验证了内部覆盖率与参考真值之间的相关性。

传统工具在多语言场景中需要同时考虑：

1
C 的符号模型
2
Java 的符号模型
3
Python 运行时
4
Go 运行时
5
跨语言边界
6
...

CONCOLLMIC 则统一成：

1
不同语言源码
2
      ↓
3
大语言模型生成插桩
4
      ↓
5
统一执行轨迹
6
      ↓
7
统一执行抽象
8
      ↓
9
同一套智能体工作流

后续智能体关注的是：

1
函数调用链
2
+
3
已执行源码块
4
+
5
源码行
6
+
7
覆盖率

而不需要为每一种语言维护完全独立的符号表达体系。

二进制输入为什么也能处理？#

论文中的 woff2 和 oggenc 都涉及二进制输入。

这类输入对大语言模型本身并不友好，例如：

1
48 46 4F 4E 54 ...

仅靠模型直接生成一段复杂的十六进制数据，很难保证格式始终正确。

论文中的工作流更接近：

1
理解二进制格式
2
    ↓
3
提出结构假设
4
    ↓
5
用 Python 生成十六进制数据
6
    ↓
7
具体执行
8
    ↓
9
观察程序行为
10
    ↓
11
修正假设
12
    ↓
13
再次生成

因此真正发挥作用的是：

1
语义推理
2
+
3
程序执行
4
+
5
工具反馈

系统并不要求大语言模型一次生成最终二进制输入。

插桩与测试使用不同的 Temperature#

1
Instrumentation Agent:
2
temperature = 0
3

4
Summarization / Solving Agent:
5
temperature = 0.5

插桩更强调确定性，因此使用 0。

后面的路径总结和约束求解需要一定的探索空间，因此使用 0.5。

提示词缓存#

智能体是多轮运行的，前面的上下文会被不断重复使用。

论文采用了后端的增量提示词缓存，以降低重复传输上下文带来的成本。

这类优化对于下面这种循环尤其重要：

1
THINK
2
→ TOOL
3
→ THINK
4
→ TOOL
5
→ ...

如果每次都重新发送完整上下文，成本会快速增加。

多个约束并行求解#

路径约束总结智能体一次可以选择多个目标分支：

1
             PC1 ─→ 求解流程 1
2
            /
3
总结智能体 ─── PC2 ─→ 求解流程 2
4
            \
5
             PC3 ─→ 求解流程 3

这些相互独立的约束可以并行求解。

这属于比较直接的工程优化：大语言模型调用的主要成本之一是延迟，因此可以并行的求解流程没有必要全部串行执行。

实验对象#

其中 krep 和 confetti 在 Claude 3.7 Sonnet 的训练数据截止时间之后才公开，用于降低训练数据泄漏对实验结果的影响。

对比工具包括：

• KLEE
• KLEE-Pending
• SymCC
• SymSan
• KLEE-Float
• AFL++

实验环境为：

1
Docker
2
2 CPUs
3
8 GiB RAM
4
48 h testing budget
5
每个工具 / subject 重复 5 次

如果 CONCOLLMIC 连续 30 分钟没有内部覆盖率增长，则提前终止。

C/C++ 分支覆盖率：为什么最终能超过传统工具？#

图 5（论文第 10 页）：重点观察整体趋势即可。CONCOLLMIC 在多个项目上能够较早进入覆盖率平台期，同时最终覆盖率高于传统动态符号执行工具。**

论文报告：

• 相比 KLEE：平均分支覆盖率提高 233%；
• 相比 KLEE-Pending：提高 135%；
• 相比 SymCC：提高 130%；
• 相比 SymSan：提高 115%；
• 相比 48 小时运行的 AFL++：提高 81%。

8 个 C/C++ 基准中，CONCOLLMIC 有 7 个项目的平均表现高于 AFL++，只有 libyaml 低于 AFL++。

这里更值得关注的问题是：

一个明显更慢的系统，为什么最终覆盖率反而更高？

论文给出的原因主要集中在两个方面。

1
位向量
2
数组
3
指针
4
浮点数
5
内存
6
...

1
满足某种结构关系的输入

1
命令行参数组合
2
LD_PRELOAD
3
网络输入
4
运行时环境

浮点约束实验：最能体现论文的核心思想#

FP-Bench 最终使用了 26 个适合测试生成的程序。

结果如下：

CONCOLLMIC 相比：

• KLEE-Float：覆盖率提高 20%；
• KLEE：覆盖率提高 107%。

这里不应该简单理解成“LLM 比 KLEE-Float 更懂浮点数”。

更准确的解释是：

1
这个循环实际上是在枚举可表示的浮点数。

1
[start, end) 中最多允许 N 个可表示浮点数。

漏洞发现：它真的找到了新的漏洞吗？#

答案是肯定的。

CONCOLLMIC 一共发现了：

11 个此前未知的漏洞。

包括：

其中：

• 9 个漏洞已经得到开发者确认或修复；
• libsoup 的第 8 个问题获得 CVE-2025-4945；
• 其他部分进入漏洞披露或 CVE 申请流程；
• 其中 6 个漏洞没有被对比工具发现。

对比工具发现的漏洞数量为：

1
KLEE          1
2
KLEE-Pending  1
3
SymCC         4
4
SymSan        5
5
AFL++         3

因此，这里的结果并不只是覆盖率曲线上的提升，还体现为实际漏洞发现能力。

为什么有些漏洞特别适合这种方法？#

论文进一步做了人工分析。

这些漏洞往往需要同时满足多个相互关联的条件。

例如：

1
精确的畸形 WAV INFO 块

1
特定命令行模式
2
+
3
特定参数组合

1
HTTP 消息解析
2
+
3
畸形 Cookie 时间戳
4
+
5
算术约束

1
高层语义理解
2
+
3
精确计算
4
+
5
具体执行验证

失败案例也很重要#

论文从 oggenc 中随机抽取了 50 次失败的测试生成迭代，并进行了分类：

这个结果很重要。

它说明当前系统的主要失败来源之一来自：

大语言模型仍然可能错误理解程序语义，并进一步生成错误的路径约束。

因此“程序语义 → 路径约束”这个环节仍然缺乏传统符号执行所追求的严格可靠性。

插桩和内部覆盖率可靠吗？#

如果第一阶段的插桩本身不准确，后续覆盖率判断也会受到影响。

因此论文使用 GCov 作为参考真值进行验证。

行覆盖率相关性#

CONCOLLMIC 内部覆盖率与 GCov 的皮尔逊相关系数：

平均值和中位数均为 94%

说明内部覆盖率与真实覆盖率高度相关。

论文认为差异主要来自：

• 少数控制流结构没有被插桩；
• GCov 对变量声明和赋值的统计方式不同。

验证准确性#

内部验证结果相对于 GCov：

1
Precision = 84%
2
Recall    = 79%
3
F1        = 81%

验证器本身也存在误差。

论文采用了一个实际的补救策略：

除了保留命中目标源码行的输入，还保留能够带来新的全局覆盖率的输入。

这样，即使目标分支判断出现漏检，只要某个输入能够继续扩大覆盖率，也不会被立即丢弃。

成本到底有多高？#

这是 CONCOLLMIC 最现实的问题之一。

论文给出的平均成本为：

1
插桩：
2
$0.56 / 1 kLoC
3

4
测试：
5
$0.21 / 每个测试输入
6
69 秒 / 每个测试输入

平均每个项目：

1
约 4.06 小时
2
约 $53.86

传统具体-符号执行可以快很多。

论文以 bc 为例指出：

SymCC 在 60 秒内可以生成 700 多个不同输入，论文将其描述为约 800× 更快。

因此 CONCOLLMIC 的定位并不追求单位时间内生成尽可能多的输入。

但它的“慢”也有另一面#

如果目标是达到各基线工具运行 48 小时后的最终分支覆盖率，论文报告 CONCOLLMIC 平均只需要：

1
31 个测试输入
2
≈ $6.1
3
≈ 32 分钟

可以把两种思路理解成：

1
传统工具：
2
大量输入
3
   ↓
4
持续探索
5
   ↓
6
覆盖率逐渐增长
7

8
CONCOLLMIC：
9
较少输入
10
   ↓
11
针对难走分支进行推理
12
   ↓
13
定向生成高价值输入

因此论文更偏向：

面向质量的定向测试生成

它更强调高价值路径的定向探索。

大语言模型调用的成本主要花在哪里？#

论文图 9 对调用进行了拆解。

总结智能体中：

1
SUM-INITIAL       23.0%
2
SUM-CODE_REQUEST  22.2%

求解智能体中：

1
SOL-THINK         8.4% cost / 15.0% frequency
2
SOL-EXECUTE_CODE 13.9% cost / 17.9% frequency

从实际行为来看，比较典型的循环是：

1
THINK
2
  ↓
3
EXECUTE_CODE
4
  ↓
5
VALIDATE
6
  ↓
7
THINK
8
  ↓
9
EXECUTE_CODE
10
  ↓
11
...

这也是智能体式设计和“一次性提示词”的主要区别之一：模型可以在工具反馈之后继续修正自己的假设。

智能体还会根据问题选择不同的约束表示#

论文发现，不同基准项目中工具调用方式差异明显。

例如：

1
woff2

会更频繁地调用：

1
QUERY_SMT

原因是其二进制格式包含大量字段之间的结构关系，这类问题比较适合结构化表示和 SMT 求解。

对应的流程可能是：

1
语义分析
2
    ↓
3
发现约束结构比较规整
4
    ↓
5
转换为 SMT
6
    ↓
7
Z3

对于其他问题，自然语言约束或直接编写 Python 程序可能已经足够。

因此：

约束表示可以根据问题类型选择合适的抽象层级。

这正是本论文相较传统固定符号表示方式比较有意思的一点。

第一层：把符号化建模从运行时执行中拆出来#

传统系统：

1
执行 + 符号化

通常高度耦合。

CONCOLLMIC：

1
具体执行
2
    ↓
3
执行轨迹
4
    ↓
5
大语言模型符号化

符号化被推迟到具体执行之后，语言和运行时相关的问题主要集中在插桩阶段。

第二层：把“公式接口”变成“语义接口”#

传统组件之间的接口更接近：

1
程序
2
 ↓
3
符号表达式
4
 ↓
5
SMT 求解器

CONCOLLMIC 则更接近：

1
程序
2
 ↓
3
执行抽象
4
 ↓
5
语义约束
6
 ↓
7
约束求解智能体

两个智能体之间不再要求共享一种固定的低层符号表示。

约束可以处在：

1
自然语言
2
编程语言
3
SMT

等不同层级，并且可以在这些层级之间转换。

第三层：让求解器成为工具，服务于上层推理#

传统方式：

1
约束
2
  ↓
3
求解器

CONCOLLMIC：

1
约束
2
  ↓
3
约束求解智能体
4
  ├── 推理
5
  ├── Python
6
  ├── Z3
7
  └── 生成测试驱动程序

这样，求解器不需要承担所有程序语义理解工作，只需要在擅长的精确计算部分提供可靠结果。

可以概括成：

大语言模型负责编排与语义推理，传统工具负责精确执行和计算。

几个比较漂亮的工程设计#

1
enter
2
code
3
exit

1
当前执行过什么
2
+
3
哪些地方没有覆盖
4
+
5
需要时再请求源码

1
实现级信息
2
    ↓
3
确定“要去哪里”
4

5
语义级信息
6
    ↓
7
确定“怎么去”

1
创建文件
2
设置环境变量
3
编译包装器
4
LD_PRELOAD
5
启动进程
6
检查输出

1
语义推理
2
  ↓
3
生成测试输入
4
  ↓
5
具体执行
6
  ↓
7
验证
8
  ↓
9
反馈

成本仍然很高#

如果：

1
每个输入 ≈ $0.21

一个项目生成几百个输入，成本就会迅速上升。

对于长期运行的大规模模糊测试任务，这很难接受。

论文提出的一个自然方向是和：

1
AFL++
2
+
3
传统具体-符号执行
4
+
5
CONCOLLMIC

进行混合式集成。

例如：

1
模糊测试器
2
  ↓
3
高吞吐量探索
4
  ↓
5
发现长期无法覆盖的复杂分支
6
  ↓
7
CONCOLLMIC
8
  ↓
9
定向生成高价值输入
10
  ↓
11
回到模糊测试器

这种架构比直接让 CONCOLLMIC 独立承担全部测试任务更现实。

上下文窗口仍然是硬限制#

论文中的测试程序大多只有几十 kLoC，没有明显耗尽 Claude Sonnet 3.7 的 200K 上下文窗口。

但如果：

1
程序规模更大
2
+
3
执行轨迹更长
4
+
5
执行抽象更复杂

仍然可能遇到上下文规模问题。

论文提出的方向是增量式总结：

1
执行轨迹
2
 ↓
3
片段 1 → 总结 1
4
片段 2 → 总结 2
5
片段 3 → 总结 3
6
...
7
 ↓
8
增量式执行轨迹总结

这可能是后续扩展到大型软件的重要方向。

大语言模型本身缺乏严格可靠性#

CONCOLLMIC 更适合：

1
测试
2
漏洞发现
3
覆盖率探索

而不适合：

1
证明程序不存在漏洞

原因很直接：

1
大语言模型可能理解错程序
2
大语言模型可能总结错约束
3
大语言模型可能生成错误的测试驱动程序

论文的核心策略是利用：

1
具体执行
2
+
3
工具调用
4
+
5
结果验证

限制错误传播，而不依赖大语言模型自身具备严格的符号执行可靠性。

数据泄漏问题#

由于实验使用：

1
Claude Sonnet 3.7

而不少基准项目是公开项目，因此存在一种潜在风险：

1
基准代码
2
    ↓
3
可能出现在训练数据中
4
    ↓
5
模型提前“见过”代码
6
    ↓
7
实验结果被高估

论文专门加入了：

1
krep
2
confetti

这两个项目在模型训练数据截止时间之后才公开。

论文观察到，在这两个项目上没有看到明显的性能下降。

这不能彻底证明不存在数据泄漏，但至少提供了一项合理的检查。

路径选择并非主要收益来源#

论文还进行了路径选择的初步实验，对比了：

1
基于大语言模型的路径选择

和：

1
深度优先搜索等传统策略

结果没有发现明显的性能差异。

这个结果反而帮助明确了论文真正的贡献：

性能提升的关键并不主要来自“大语言模型更会选择下一条路径”，而更可能来自符号化建模、约束表示、约束求解以及运行时环境操控。

因此，论文更值得关注的是让大语言模型处理传统符号执行中最难维护的程序语义。