技术摘要：充分错误逻辑 (Sufficient Incorrectness Logic, SIL) 与 分离 SIL (Separation SIL)

1. 问题陈述

用于程序验证的形式化方法在历史上依赖于过近似（over-approximation）技术（例如 Hoare 逻辑、抽象解释）来保证无错误。虽然这些方法是可靠的，但不可避免地会产生虚假报警（spurious errors/false alarms），这阻碍了程序员的使用。相反，欠近似（under-approximation）方法（例如 错误逻辑 Incorrectness Logic, IL；以及 有界模型检测 Bounded Model Checking）旨在寻找 Bug，并且由于它们仅报告可达的错误状态，因此不存在虚假报警。然而，现有的欠近似逻辑（如 IL）主要关注证明从某个前置条件出发可以到达错误的存在性。它们并不一定刻画导致此类错误的初始状态集合。

论文指出，在推理错误来源方面存在一个空白。程序员不仅需要知道是否存在 Bug，还需要明确知道哪些输入状态会导致该 Bug，以便有效地界定调试和测试范围。虽然“里斯本三元组”（Lisbon triples，即向后欠近似）此前在结果逻辑（Outcome Logic, OL）的语境下被讨论过，但目前仍缺乏一个专门的、极简且完备的、用于推导错误充分前置条件的证明系统。

2. 方法论

作者引入了 充分错误逻辑 (SIL)，这是一种全新的基于三元组的程序逻辑，旨在进行向后欠近似。

2.1 核心概念：SIL 三元组

SIL 三元组表示为 $\langle\langle P \rangle\rangle r \langle\langle Q \rangle\rangle$。

• 语义： 当且仅当程序 $r$ 对错误状态集 $Q$ 应用向后收集语义时，其结果包含初始状态集 $P$，则该三元组有效。形式化表示为：$J \leftarrow r K (Q) \supseteq P$。
• 解释： “所有满足 $P$ 的输入状态都至少有一次执行 $r$ 的过程会导致满足 $Q$ 的状态。”
• 与 IL 的区别： IL ($[P] r [Q]$) 保证从 $P$ 中的某个状态可以到达 $Q$ 中的某个状态；而 SIL 保证 $P$ 中的每一个状态都能到达 $Q$ 中的错误。这使得 $P$ 成为错误的充分条件。

2.2 证明系统

论文定义了一套用于 SIL 的极简规则集（图 7），该规则集对于常规命令（包括非确定性和循环）是可靠且完备的。

• 向后语义： 规则源自命令的向后语义（例如，赋值使用向后代换）。
• 蕴含规则： $\langle\langle \text{cons} \rangle\rangle$ 规则允许加强前置条件并削弱后置条件，从而促进欠近似。
• 处理循环： 该逻辑包含了迭代规则（$\langle\langle \text{iter} \rangle\rangle$）以及额外的规则，如 $\langle\langle \text{iter0} \rangle\rangle$（跳过循环）和 $\langle\langle \text{unroll} \rangle\rangle$（展开一次），以支持无需循环不变式即可进行终止性分析的实际分析。
• 析取： 与 Hoare 逻辑不同，SIL 允许丢弃前置条件中的析取项（通过 $\langle\langle \text{choice} \rangle\rangle$ 和 $\langle\langle \text{disj} \rangle\rangle$），这对于提高欠近似的扩展性至关重要。

2.3 分离 SIL (Separation SIL)

为了处理指针和动态内存分配，作者将 SIL 与分离逻辑公式相结合，创建了 分离 SIL (Separation SIL)。

• 断言语言： 结合了标准分离逻辑（堆分离、指向）与从错误分离逻辑 (Incorrectness Separation Logic, ISL) 适配而来的断言 $x \not\mapsto$（表示已释放的指针）。
• 规则： 包括堆操作（分配 alloc、释放 free、加载 load、存储 store）的向后规则，以及一个框架规则（$\langle\langle \text{frame} \rangle\rangle$），用于实现关于内存错误的局部推理。
• 完备性： 该系统被证明是可靠的。对于无循环程序，证明其具有相对完备性（假设存在断言间蕴含关系的预言机/oracle）。

3. 主要贡献

1. 引入 SIL： 一种用于充分错误三元组的新颖逻辑，它识别的是错误的来源（初始状态），而非仅仅是 Bug 的存在。
2. 形式化分类法： 论文根据两个轴构建了三元组逻辑的分类法（图 3）：
   • 语义方向： 向前（Hoare 逻辑、IL）与 向后（SIL、必要条件 NC）。
   • 近似类型： 过近似（Hoare 逻辑、必要条件）与 欠近似（IL、SIL）。
   • 该分类法明确了 SIL 是向后语义与欠近似的唯一结合体。
3. 对比分析：
   • SIL vs. IL： IL 发现错误是否可达；SIL 发现哪些输入会导致错误。两者在逻辑上并不等价。
   • SIL vs. Hoare 逻辑 (HL)： 对于确定性且终止的程序，SIL 与 HL 相一致（将后置条件解释为错误状态）。对于非确定性程序，两者会产生分歧。
   • SIL vs. 必要条件 (NC)： 作者证明 NC 与 HL 是同构的（通过双重否定），但在一般情况下，NC 与 IL 或 SIL 不具备可比性。
   • SIL vs. 结果逻辑 (OL)： 虽然 OL 可以表达 SIL 三元组（特别是“里斯本”模式），但作者认为 SIL 的证明系统在推导错误规范的前置条件方面更加直接和自然，特别是在处理析取和向后推理方面。
4. 分离 SIL： 这是一个针对内存错误的可靠且相对完备的实例化，证明了向后欠近似在特定情况下（例如提供实际的见证/witness 进行测试）可以产生比 ISL 更简洁的后置条件和更强的保证。

4. 结果

• 正确性与完备性： 极简的 SIL 规则集被证明对常规命令是可靠且完备的。
• 相对完备性： 分离 SIL 被证明对于无循环程序是相对完备的。
• 工业相关性： 论文指出，SIL 为 Meta 公司工业工具（Zoncolan, Mariana Trench, Pysa）中使用的向后分析策略提供了形式化的事后证明（a posteriori justification），这些工具通过推导充分错误前置条件来检测安全漏洞。
• 推导示例： 论文提供了详细的推导过程（例如涉及 free 和 alloc 的客户端程序），展示了分离 SIL 如何推导出保证错误发生的先决条件，从而提供比面向前方的逻辑更直接的调试路径。

5. 意义与主张

论文声称 SIL 通过提供一个面向后方的欠近似框架，填补了一个关键的理论空白。其意义在于：

• 调试的精确性： 通过识别导致错误的精确输入状态集，SIL 支持了更符合开发者直觉的“向后推理”——即理解“为什么”会发生 Bug，而不仅仅是像向前欠近似那样仅显示 Bug 是否可达。
• 理论统一： 它澄清了程序逻辑的版图，表明虽然 Hoare 逻辑与必要条件之间存在对偶性，但 Incorrectness Logic 与 Sufficient Incorrectness Logic 之间并不存在这种简单的对偶关系。
• 实用价值： 作者认为，分离 SIL 可以比错误分离逻辑 (ISL) 生成更简洁的后置条件和更强的保证，因为它确保了前置条件中的每一个状态都会导致错误，从而提供了具体的见证（witnesses）。

论文总结道，并没有哪一种逻辑是“更好”的；相反，每种逻辑（HL, IL, NC, SIL）都有其特定的用途。SIL 被专门定位为当目标是定位错误来源以指导调试和测试工作时的首选工具。