基于编译的欠约束执行引擎（OSDI 2026）
原题：A Compilation-based Under-Constrained Execution Engine
一句话总结：解释执行引擎在大规模 C/C++ 代码上速度不足，UCSAN 借助 LLVM 编译插桩、伪指针和按需初始化把任意函数集合编译成用户态可执行文件；与 SymSan 结合后，在 Linux 内核 UBI 告警处理中平均每条告警 0.32 秒，比 KLEE-IL 的 5.14 秒快 15.06 倍，但分析范围、外部函数建模、循环和并发仍决定误报与漏报。
问题与动机
动态分析比静态分析更精确，却通常需要测试 harness 和完整运行环境。内核函数往往依赖启动流程、设备或虚拟机，内部模块难以单独调用。静态分析可以覆盖更大的代码范围，但 Linux 内核 UBI 分析产生的 147,643 条告警中只有 52 条得到确认，误报成本很高。
欠约束执行允许从任意内部函数开始，并把未初始化对象延迟到首次访问时创建，因此避开完整环境。现有 UC-KLEE 和 Angr 主要采用解释执行，速度限制了文件系统、协议栈和驱动等模块的分析。UCSAN 的目标是把欠约束执行从具体的符号执行实现中拆出来，以编译后的普通二进制作为动态分析载体。
关键观察 / 隐含假设
- 观察 1：欠约束分析的主要瓶颈来自解释执行，而不是必须保留解释器才能处理未初始化内存。nbench 和链表微基准表明，编译路径可以保留欠约束语义并获得更高吞吐（§5.2）。
- 依赖假设：目标代码能够生成 LLVM IR，且 LLVM 插桩可以覆盖其指针操作。
- 可能失效场景：大量未支持的 inline assembly、特殊 ABI 或不可建模的外部函数会在编译阶段失败。
- 观察 2：从任意内部函数开始时，堆对象的大小、别名关系和输入内容无法预先完全确定，需要执行期间逐步物化。链表示例中的
container_of会让入口参数的结构类型小于实际对象类型（§2.2）。- 依赖假设：指针的来源和数据流能够由 shadow pointer 追踪，且错误的大小估计可以安全地重新分配。
- 可能失效场景：动态重分配可能掩盖边界错误；循环数据结构、复杂指针关系和并发访问超出当前模型。
- 假设 1：分析范围包含从入口到相关分配/释放点及错误使用点的足够路径。证据强度：强。论文明确指出范围过小会丢失约束并产生误报或漏报（§3.4、§6）。
核心方法
UCSAN 是 LLVM Pass 与运行库的组合。配置文件指定入口函数、分析范围以及范围外函数的处理策略。UCSAN 删除范围外代码，生成新的 main，并把结果链接为自包含用户态程序。外部函数可以使用自定义 wrapper、纯函数假设或“任意修改”模型；这使 kmalloc 可以映射到 malloc，但也把建模正确性留给配置和 wrapper。
UCSAN 的核心抽象是伪指针（pseudo-pointer）。程序数据流中保留的是逻辑地址，真正访问内存前才转换成有效地址。shadow pointer 类似软件实现的段寄存器，记录逻辑基址、对象 ID、真实对象地址，以及指针从哪个对象的哪个偏移加载而来。该设计回应了观察 2：它可以在首次解引用时创建对象，并让别名指针映射到同一对象。
按需初始化（JITI）由 check_ptr 完成。它先判断指针是否已经是有效 real-pointer；若对象尚未创建，则根据类型、指针运算和访问大小推断分配大小，分配并初始化对象，再根据 seed 中的对象关系恢复内容，最后计算逻辑偏移对应的真实地址。real-pointer 只交给当前内存访问，不写回程序数据流，所以对象扩容不会留下 stale pointer（§3.2）。
seed 将输入组织成带对象 ID、来源关系、大小和内容的对象列表。根对象放在 Super Object 中；动态对象通过从根对象开始的解引用链定位。这让不同执行路径可以用具体 seed 驱动，而不要求真实虚拟地址满足符号约束。
论文还复用 sanitizer 的 shadow memory 实现 OOB、UAF 和 UBI 检查器。UCSAN† 将 UCSAN 与 SymSan 结合：SymSan 记录符号路径，Python/C++ companion server 用 Z3 求解并生成新 seed。UCSAN 本身不依赖特定动态分析器，也可以接入 fuzzing 或其他路径探索器。
设计取舍
- 编译性能换取运行时通用性：LLVM 编译使执行速度接近原生代码，但每个分析范围都要插桩、组装和链接，且必须处理 LLVM IR、ABI 和 inline assembly。
- 欠约束灵活性牺牲上下文精度：从内部函数启动减少 harness 成本，却可能遗漏外部函数带来的约束。AFGen 数据集中 7 个误报都归因于范围外函数约束缺失（§5.4.2）。
- 透明扩容换取安全检查边界：JITI 的动态重分配避免了错误大小估计导致的崩溃，但未知大小的缓冲区溢出需要关闭该能力才能检测（§5.4.2）。
实验与结果
- 链表 20 节点微基准中，UCSAN 用时 9 秒，KLEE-IL 用时 20 秒，Angr 用时 79 秒（§5.2）。
- nbench 中 UCSAN 比 KLEE-IL 快数个数量级；Angr 在 18 小时内未完成一次迭代并因内存耗尽崩溃（表 1）。
- Linux 4.14、5.10.240 和 6.16.0 的兼容性分别达到 UBI 告警范围的较高覆盖，以及 14,503/15,077（96.2%）和 139,509/156,924（88.9%）个分析范围成功编译；失败主要与 inline assembly 有关（§5.3）。
- 在 2 分钟、2 GB 限制和 24 个并行实例下，UCSAN† 平均 TTF 比 KLEE-IL 快 6.36 倍；每条告警平均 0.32 秒，对比 5.14 秒，完成 95.46% 而 KLEE-IL 完成约 41%（§5.4.1、图 7、表 2–3）。
- UCSAN† 重现了 AFGen 数据集中的 69/94 个 CVE，以及 SyzSpec 中的 26/38 个内核 bug；失败案例主要来自路径爆炸、范围不完整和并发不支持（§5.4.2、表 4–5）。
论断—证据表
| 论断 | 证据 | 评测边界 | 置信度 |
|---|---|---|---|
| 编译式欠约束执行显著快于解释式引擎 | 链表测量；nbench 表 1 | 单机、LLVM 12、KLEE-IL/Angr 对照 | 强 |
| UCSAN 可编译大规模内核分析范围 | Linux 4.14/5.10/6.16 兼容性，§5.3 | 失败主要集中在 inline assembly | 强 |
| 更高速度提升了静态告警确认能力 | 0.32 秒/告警、95.46% 完成率，§5.4.1、表 2–3 | 2 分钟超时、24 并发、UBITect 告警 | 强 |
| 欠约束执行可以减少 harness 工作 | CVE 与 SyzSpec 重现，§5.4.2 | 配置部分由人工或 coding agent 生成，仍需范围信息 | 中 |
批判性分析
论证链条
性能结果支持编译执行比解释执行更适合大范围分析，UBI 结果也支持“速度能转化为更多已处理告警”。但“无需手工 effort”表述需要收窄：CVE 实验仍由人工或 coding agent 确定入口、范围和 wrapper；工具消除的是 harness 实现，不是分析配置工作。
假设压力测试
范围外函数默认纯函数或任意修改都会改变路径可行性。字符串、文件 I/O 和 fstat 等函数当前缺少精确模型，论文已观察到由此造成的失败和误报。单入口模型也不适合 tcp_v4_do_rcv 这类需要多次调用才能建立状态的代码。论文在 Binder 模块中观察到的 7 个空指针告警全部是缺失上下文造成的误报。
实验可信度
性能对照覆盖了微基准、nbench 和真实内核告警，且统一了 Z3、超时、内存和并发设置。CVE 重现展示了适用范围，但数据集是已知漏洞，配置又部分依赖 agent 生成，不能直接推出未知漏洞发现率。Linux 兼容性主要以能否编译为指标，未充分反映运行时错误、覆盖率和运维成本。
系统性缺陷
当前实现不支持并发、循环数据结构和多个入口；循环与递归只能使用全局迭代阈值。inline assembly 需要启发式处理或手写 wrapper。JITI 的对象扩容和 under-constrained 输入可能改变内存安全检查语义，使用者需要明确区分“探索可执行性”和“真实程序中的边界条件”。
局限与后续工作
- 局限 1：范围标注仍是用户责任；错误范围会产生误报或漏报。后续可评估静态分析、LLM 和人工修订的组合在更大内核版本上的准确率。
- 局限 2：外部函数模型不完整。应为字符串和文件 I/O 建立带输入—返回值依赖的 wrapper，并用真实调用轨迹检查误报率。
- 局限 3：不支持循环对象、并发和多入口状态。可分别以循环链表、并发内核 bug 和多次
tcp_v4_do_rcv调用作为可重复验证集。 - 局限 4：路径爆炸仍存在。应比较按循环、递归和模块划分的局部阈值策略，而不是只提高全局阈值。