💻 computer science

SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

SEAL 是一个模块化的原型静态分析器，用于验证具有无界链式数据结构的程序，它利用分离逻辑和基于 SMT 的 Astral 求解器，在 LinkedLists 类别中取得了具有竞争力的结果，同时为未来的开发提供了显著的可扩展性。

原作者： Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

发布于 2026-02-09

📖 1 分钟阅读☕ 轻松阅读

原作者： Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

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

想象一下，你正在试图验证一个由道路和建筑组成的复杂且不断变化的城市是否安全可通行。你需要确保没有人从桥上掉下去（即“空指针解引用”/NULL-pointer dereference）、没有人试图拆除一栋已经不存在的建筑（即“释放后使用”/use-after-free 错误），以及没有人意外地将同一栋建筑拆除两次（即“双重释放”/double-free 错误）。

这正是 SEAL 所做的事情，只不过它分析的不是城市，而是管理复杂、不断变化的列表（如链表）的计算机程序。

以下是论文对 SEAL 的解释，通过简单的概念进行了拆解：

1. 核心思想：一个专门的侦探

大多数检查这些程序的工具都像是在为每种类型的犯罪使用一套特定且僵化的规则手册。SEAL 则不同。它使用了一个通用的“逻辑引擎”，称为 ASTRAL。

把 ASTRAL 想象成一个超级聪明的翻译官。当 SEAL 看到一个关于内存中数据如何连接的复杂谜题时，它会将这个谜题翻译成一种标准的、功能强大的计算机求解器（称为 SMT 求解器）能够完美理解的语言。这使得 SEAL 非常灵活。这就像是一个侦探可以切换语言去与任何专家交流，而不是被困在只能说一种方言的状态。

2. 挑战：无限 vs 有限

SEAL 检查的程序通常涉及链表——即数据项相互指向的链条。

问题： 有些链表是短小且固定的（比如由 3 个环节组成的链条）。而有些链表是无界的，这意味着它们可能是 10 个环节长，也可能是 10,000 个甚至无限长。
难点： 尝试检查无限长链条中每一种可能的长度对计算机来说是不可能的。这会耗费无穷的时间。
SEAL 的窍门： SEAL 使用了一种名为**抽象（abstraction）**的技术。想象你在观察一列非常长的火车。与其数清每一个车厢，SEAL 会说：“好吧，这是一个‘长火车’。”它用一个简洁的标签（一个“谓词”）替换了链条中间那些混乱的细节。这使得它能够推理整个链条，而不会迷失在细节之中。

3. 工作原理：“形状”分析器

SEAL 是一个“形状分析器”。它不仅仅观察数字，它还观察内存的形状。

符号堆（Symbolic Heaps）： 它使用“符号堆”来创建内存地图。可以将其想象成一张蓝图，上面写着：“这里是一个内存块，它连接到那个内存块。”
循环不动点（The Loop Fixpoint）： 当一个程序在循环中运行（重复执行同一个动作）时，SEAL 会检查内存的“形状”是否趋于稳定。如果当前轮次的形状与上一轮相比看起来“足够安全”，它就会停止检查并宣布该循环是安全的。

4. 当前的优势与不足

论文承认 SEAL 目前仍是一个原型（早期版本），但它拥有一些令人印象深刻的数据统计：

好消息（优势）：

“无界”俱乐部： 在最近的一次比赛中，有 20 个工具尝试验证包含无限链表的程序。其中只有 4 个 工具成功了。SEAL 就是其中之一。
未来潜力： 由于 SEAL 使用了那个灵活的“翻译官”（ASTRAL），教它理解新的形状变得更加容易。作者认为，他们最终可以教会它处理复杂的结构，如树（trees）或跳表（skip-lists，类似于数据的多层高速公路），而这些结构是其他工具难以处理的。

坏消息（不足）：

词汇量有限： SEAL 目前仅能理解 C 语言的一个子集。它目前还无法处理复杂的数学运算或多种类型的指针。
猜测游戏： 有时，SEAL 必须猜测一段代码正在构建什么样的数据结构。如果它猜错了（例如，认为一个复杂的结构只是一个简单的列表），它可能会漏掉 Bug 或给出“我不知道”的答案。
误报（False Positives）： 因为它使用了抽象技术（简化了细节），它有时会误认为程序是不安全的，而实际上程序是正常的。论文指出，他们可以通过在不进行简化的前提下重新运行检查来修复这个问题，但这会耗费更多时间。

5. 底线

SEAL 是一个全新的、模块化的工具，旨在证明管理复杂、无限数据链的程序是安全的。虽然它现在还不完美，也不理解 C 语言的所有特性，但其独特的架构——使用通用翻译器来解决逻辑谜题——使其成为少数能够处理最难的内存安全问题的工具之一。作者希望，通过保持系统的灵活性，他们可以让它在未来的比赛中变得更加强大。

技术摘要：SEAL —— 基于分离逻辑的符号执行

问题陈述

验证操纵无界链式数据结构的程序仍然是静态分析中的一个重大挑战。虽然许多工具依赖于有界模型检测或专门的启发式算法，但这些方法在处理关于任意列表长度和复杂内存形状的推理时往往显得力不从心。此外，现有的基于分离逻辑（Separation Logic, SL）的分析器通常将分析过程与专门的、非模块化的求解器耦合在一起，这限制了其可扩展性以及与其他逻辑理论集成的能力。

方法论

SEAL 是一种旨在验证操纵无界链式数据结构的程序的静态分析器。它采用基于分离逻辑（SL）公式的前向抽象解释。其核心方法论的独特之处在于其模块化架构，该架构将分析引擎与逻辑推理引擎清晰地解耦。

核心组件

抽象域（符号堆）：
- SEAL 将抽象内存状态表示为符号堆，即形式为 $\exists x_1, \dots, x_m. \phi_1 * \dots * \phi_n$ 的 SL 公式。
- 原子公式 ( $\phi_i$ $ϕ_{i}$ ) 包括：
  - 纯公式（Pure formulae）： 描述指针（不等）关系或非指针值的约束。
  - 指向原子（Points-to atoms）： 描述单个堆单元。
  - 归纳谓词（Inductive predicates）： 描述无界指针序列（例如列表）。
  - 空闲内存（Free memory）： 一个特殊的谓词，显式表示仍处于可达状态的已释放内存。
- 该域追踪特定范围内的精确整数值（默认范围为 $[-5, 5]$ ）。程序位置的状态表示为符号堆的析言（集合）。
抽象与拓宽（Abstraction and Widening）：
- 为了处理循环和无限状态空间，SEAL 通过泛化内存形状来进行拓宽。这涉及寻找兼容的空间谓词（指向谓词或列表谓词），并将它们合并为一个单一的列表谓词，前提是该链接位置不受外部指针或程序变量的目标影响。
- 系统追踪固定上限内的最小列表长度，以确保抽象过程中的无环性保证。
- 谓词猜测（Predicate Guessing）： 目前，SEAL 在分析前根据字段数量（例如，一个自引用字段 $\to$ 单向链表；两个 $\to$ 双向链表）来猜测预期的 C 结构归纳谓词。这种启发式方法可能会导致分类错误（例如，将一个意图作为嵌套列表的结构误分类为双向链表）。
ASTRAL 求解器：
- 不同于大多数使用专门启发式算法进行可满足性和蕴含性检查的 SL 工具，SEAL 依赖于 ASTRAL，一个通用的分离逻辑求解器。
- ASTRAL 将 SL 公式转换为 SMT 理论（特别是位向量和数组），并使用对谓词展开的限制。
- 转换后的公式被传递给 BITWUZLA SMT 求解器。
- ASTRAL 支持用户自定义归纳谓词，允许 SEAL 在无需内置求解器支持的情况下定义自己的谓词。
分析机制：
- 循环不动点（Loop Fixpoints）： 当当前循环迭代状态 ( $S$ ) 与前一次迭代状态 ( $T$ ) 之间的蕴含关系成立时，即达到不动点。这通过检查是否对于 $S$ 中的每个堆，都存在一个能蕴含它的 $T$ 中的堆来进行近似。
- 过程间分析（Interprocedural Analysis）： 函数调用通过摘要（前置条件/后置条件对）进行优化。
- 简化（Simplification）： 系统应用句法简化，例如减少等价类和移除超出作用域的变量。

核心贡献

模块化架构： 通过 ASTRAL 将抽象解释引擎与逻辑推理引擎分离，SEAL 实现了一种旨在易于扩展和结合其他理论进行推理的设计。
通用求解： 对 ASTRAL 的集成使得 SEAL 能够利用 SMT 求解器进行 SL 蕴含和可满足性检查，从而避免了为每种特定的逻辑变体开发定制专用求解器的需求。
无界列表验证： 该工具能够验证操纵无界链表的程序，而这类程序是许多竞争工具无法处理的类别。

实验结果

SEAL 参加了 SV-COMP 竞赛中的 MemSafety-LinkedLists 类别。

整体性能： 在全部 134 个程序中，SEAL 将 55 个验证为“True”（正确），发现了 4 个“False”（缺陷），有 75 个报告无结果。
无界列表子集： 在需要处理无界数据结构的 69 个程序子集中，SEAL 验证了 14 个程序为正确，并发现了 2 个缺陷。
对比：
- SEAL 的表现优于 2LS（后者仅验证了 3 个无界程序）。
- SEAL 验证的程序数量少于 PREDATORHP (46) 和 CPACHECKER (40)，这两者均使用符号内存图（SMG）。
- SEAL 是仅有的四个能够验证该类别中无界列表程序的分析器之一。

意义与主张

论文将 SEAL 定位为一个具有前景的原型，其重点在于可扩展性而非单纯追求原始性能的统治地位。

未来潜力： 作者声称，SEAL 的模块化设计及其对 ASTRAL 的依赖，为支持那些难以用 SMG 表达的复杂数据结构（如跳表和树）提供了坚实的基础。
局限性： 作为早期原型，SEAL 目前仅支持 C 语言的一个子集（有限的指针算术、特定的整数追踪），并且依赖启发式谓词猜测，这可能导致由于缺少整数信息而产生误报或无法报告违规情况。
路线图： 作者打算改进分析期间的谓词选择，从示例中合成归纳谓词，并可能将 SEAL 嵌入为 Frama-C EVA 框架中的一个抽象域，以处理更复杂的非指针值。

总之，SEAL 证明了基于 SMT 的通用分离逻辑求解方法是一种可行且可扩展的替代方案，为未来在竞赛中验证复杂的无界链式数据结构开辟了路径。