[论文] SEAL：符号执行与分离逻辑（竞赛贡献）

Source: arXiv - 2602.05703v1

（请提供您希望翻译的具体内容，我将为您翻译成简体中文。）

概述

SEAL 项目引入了一种新的静态分析工具，能够自动验证操作 无界链式数据结构（如列表、树以及其他指针密集型结构）的程序。通过将 分离逻辑 与现代基于 SMT 的求解器相结合，SEAL 实现了模块化和可扩展性的水平，使其区别于早期的验证框架，并且在最近的 SV‑Comp “LinkedLists” 类别中表现竞争力。

关键贡献

• 通用分离逻辑引擎 – SEAL 复用 Astral 求解器，将分离逻辑蕴含翻译为 SMT 查询，避免了手工编写的领域特定证明器的需求。
• 模块化架构 – 分析流水线被清晰划分为前端（程序解析）、抽象状态表示和后端（SMT 求解）。这使得插入额外理论（例如算术、数组）变得直接。
• 支持无限列表 – SEAL 是为数不多的四个工具之一，能够证明分配和操作任意长度列表的程序的正确性，这是静态分析器长期面临的挑战。
• 竞争性比赛结果 – 在 SV‑Comp “LinkedLists” 基础类别中，SEAL 与许多成熟工具持平或超出它们的表现，尽管它仍是一个原型。
• 开放式可扩展性 – 作者明确将 SEAL 设计为一个研究平台，可通过新的抽象域、自定义谓词或混合推理策略进行扩展。

方法论

1. Program Front‑end – SEAL parses C (or a subset used in the competition) and builds a control‑flow graph (CFG).
   程序前端 – SEAL 解析 C（或竞赛中使用的子集）并构建控制流图（CFG）。

2. Abstract Memory Model – Memory states are expressed in separation logic: heap fragments are described by predicates (e.g., list(x) for a linked list starting at x). This naturally captures disjointness and sharing.
   抽象内存模型 – 内存状态使用 分离逻辑 表示：堆片段由谓词描述（例如 list(x) 表示从 x 开始的链表）。这自然捕获了不相交性和共享。

3. Symbolic Execution – The tool walks the CFG symbolically, updating the separation‑logic formula at each program point.
   符号执行 – 工具对 CFG 进行符号遍历，在每个程序点更新分离逻辑公式。

4. Entailment & Satisfiability via Astral

   • Each symbolic step may generate a verification condition (VC) that asks whether a current heap predicate entails a required one (e.g., after a free, the list predicate should no longer hold).
   • Astral translates these VCs into SMT‑LIB formulas, delegating the heavy lifting to state‑of‑the‑art SMT solvers (Z3, CVC5, …).

   通过 Astral 的蕴涵与可满足性

   • 每个符号步骤可能生成一个 验证条件（VC），用于询问当前堆谓词是否蕴涵所需的谓词（例如，在 free 之后，列表谓词应不再成立）。
   • Astral 将这些 VC 转换为 SMT‑LIB 公式，并将繁重的计算委托给最先进的 SMT 求解器（Z3、CVC5，……）。

5. Result Aggregation – If all VCs are proved, the program is declared safe; otherwise, a counterexample trace is produced.
   结果聚合 – 如果所有 VC 都被证明，则程序被声明为安全；否则，会生成一个反例跟踪。

Because the heavy logical reasoning is outsourced to an SMT solver, SEAL avoids implementing its own low‑level decision procedures, which is where most of the engineering effort in traditional separation‑logic tools resides.
由于繁重的逻辑推理被外包给 SMT 求解器，SEAL 避免了实现自己的低层决策过程，这正是传统分离逻辑工具中大部分工程工作所在。

结果与发现

关键要点是模块化不必牺牲验证能力。通过利用 Astral + SMT，SEAL 能够处理与更为整体化的工具相同类别的问题，同时保持代码库简洁且易于适配。

实际影响

• 更安全的低层代码 – 编写系统代码（例如内核模块、嵌入式驱动）的开发者经常手动操作链表结构。SEAL 可以自动证明不存在常见错误，如空指针解引用、内存泄漏或列表更新错误。
• 集成到 CI 流水线 – 由于 SEAL 的后端是 SMT 求解器，可以无交互运行并生成机器可读的证明证书，适合持续集成检查。
• 可扩展的验证平台 – 需要领域特定不变式（例如网络数据包缓冲区、无锁队列）的公司可以添加自定义分离逻辑谓词，而无需重写核心求解器。
• 混合分析 – 该架构允许与其他静态分析（例如数值范围的抽象解释）结合，在一次遍历中对混合数据（列表 + 整数计数器）进行推理。

简而言之，SEAL 为 指针密集代码的实用、可扩展验证 打开了大门，无需终端用户具备深厚的定理证明专业知识。

限制与未来工作

• 原型成熟度 – 当前实现缺少许多工程细节（例如增量求解、并行化），这些改进可以提升在大型代码库上的可扩展性。
• 性能开销 – 将分离逻辑蕴含翻译为 SMT 会产生非平凡的成本；对于非常大的程序，分析速度可能会慢于专门的、手工调优的工具。
• 语言覆盖范围 – SEAL 侧重于竞赛中使用的受限 C 子集；完整的 C 支持（宏、内联汇编）仍不在范围之内。
• 作者提出的未来方向 包括：
  • 添加 领域特定扩展（例如用于树、图的谓词）。
  • 改进 求解器集成（缓存、增量查询）。
  • 探索 与其他理论的组合，如算术或位向量，以验证更复杂的不变式。

总体而言，SEAL 展示了干净的分离逻辑 + SMT 架构既强大又可扩展；通过进一步的工程投入，它有望成为需要对指针密集代码提供严格保证的开发者的主流工具。

作者

• Tomáš Brablec
• Tomáš Dacík
• Tomáš Vojnar

论文信息

• arXiv ID: 2602.05703v1
• 分类: cs.SE
• 发布日期: 2026年2月5日
• PDF: 下载 PDF