A Deductive System for Contract Satisfaction Proofs

本文提出了一种基于相对迹等式和相对双模拟的演绎证明系统，利用 Rocq 证明助手实现了硬件 - 软件合同满足性证明的模块化、增量式及自动化验证。

要点

这篇论文讲述了一个关于如何给电脑芯片“做体检”并开具“健康证明”的新方法。

为了让你更容易理解，我们可以把电脑芯片（CPU）想象成一家繁忙的餐厅，把黑客想象成想偷窥顾客点菜内容的竞争对手。

1. 背景：为什么我们需要“合同”？

• 餐厅的泄漏（侧信道攻击）：
  想象一下，虽然顾客（程序）在点菜时没有大声说出秘密（比如密码），但餐厅的厨房噪音、服务员跑动的路线、或者洗碗池的水位（这些是芯片的微架构细节，如缓存、分支预测器）可能会无意中暴露顾客点了什么。

  • 例子： 如果顾客点了“红烧肉”（秘密数据），厨房可能会因为忙碌而发出特定的声音。黑客只要监听这些声音，就能猜出顾客点了什么。

• 硬件 - 软件合同（Hardware-Software Contracts）：
  为了不让每个程序员都去研究复杂的厨房噪音（芯片内部细节），芯片制造商和软件开发者签了一份**“合同”**。

  • 合同的内容： 这份合同规定了：“只要你的程序在‘合同模型’下看起来是安全的（比如，无论点红烧肉还是清蒸鱼，厨房噪音听起来都一样），那么它在真实的芯片上也是安全的。”
  • 核心问题： 这份合同真的靠谱吗？也就是说，真实的厨房（硬件）是否真的遵守了合同里的噪音规则？ 如果合同说“噪音一样”，但实际厨房因为某种原因泄露了秘密，那合同就失效了。

2. 以前的做法 vs. 现在的挑战

• 以前的做法（试错与模型检查）：
  以前，工程师们要么靠手工画图推理（像写几页纸的数学证明，容易出错且难验证），要么用自动化模型检查（像让机器人去遍历所有可能的情况）。

  • 缺点： 手工证明太累太容易错；自动化检查如果找不到规律就会卡死，或者如果机器人本身有 bug，结论也不可信。

• 这篇论文的新方法（交互式证明助手）：
  作者们开发了一套**“逻辑推理工具箱”**，并在一个叫 Rocq 的“超级数学助手”里实现了它。

  • 核心思想： 他们不再试图一次性找出所有规律，而是像搭积木一样，一步步构建证明。

3. 核心概念：相对轨迹相等（Relative Trace Equality）

这是论文最抽象的部分，我们用**“双人舞”**来比喻：

• 场景： 我们有四支舞队（四个执行轨迹）：

  1. 合同版 A（合同模型，输入 A）
  2. 合同版 B（合同模型，输入 B）
  3. 真实版 A（真实芯片，输入 A）
  4. 真实版 B（真实芯片，输入 B）

• 目标： 我们要证明：如果 合同版 A 和 合同版 B 跳出来的舞步（噪音/泄露）是一模一样的，那么 真实版 A 和 真实版 B 跳出来的舞步也必须是一模一样的。

• 难点：

  • 步调不一致： 合同模型可能一步跳完，真实芯片可能因为“猜测”（分支预测）多跳了几步，或者少跳了几步。它们不是同步的（非锁步）。
  • 四重关系： 传统的证明通常只比较两个状态，这里需要同时比较四个状态，非常复杂。

4. 论文的创新：相对双模拟（Relative Bisimulation）

作者发明了一种新的**“舞步同步技巧”，叫相对双模拟**。

• 以前的技巧（锁步）： 要求四个舞队必须严格同步，一步对一步。但这在芯片里行不通，因为芯片经常“乱跳”（推测执行）。
• 新技巧（非锁步）： 允许舞队**“快进”或“暂停”**。
  • 如果合同模型说“这一步没泄露秘密”，我们可以让真实芯片多跳几步，直到它回到一个安全状态，然后再继续比较。
  • 这就好比：合同说“不管你怎么走，只要最后没发出声音就行”。真实芯片可以中间绕个路（推测执行），只要最后绕回来时声音没变，就证明它是安全的。

5. 这个系统怎么工作？（像玩拼图）

作者把这个证明过程变成了一个交互式游戏，在 Rocq 助手里进行：

1. 设定目标： 证明“如果合同 A=合同 B，则 硬件 A=硬件 B"。
2. 逐步拆解： 系统允许你一步步走。
   • C-Step（合同步）： 你可以先让合同模型走一步，看看它泄露了什么。
   • H-Step（硬件步）： 然后让真实芯片走几步，看看它泄露了什么。
   • 循环（Cycle）： 如果你发现现在的状态和之前某个状态很像（或者在“不变量”集合里），你就可以直接宣布“证明完成”，不用每一步都重新算。
3. 利用对称性： 系统还允许你利用“对称性”（比如 A 和 B 互换位置结果一样）来简化证明，就像做数学题时利用公式简化计算一样。

6. 实际效果：两个挑战

作者用这个系统成功证明了两个复杂的芯片特性：

1. “总是猜错”合同（Always-Mispredict）：

   • 比喻： 这是一个防御策略。合同规定：“不管厨师猜对猜错，我都假装猜错，把两条路都走一遍，所以噪音永远一样。”
   • 证明： 作者证明了，即使真实芯片有时候猜对了（只走一条路），它的噪音也不会比“总是猜错”的合同泄露得更多。这就像证明：“即使厨师偶尔偷懒只走一条路，他发出的声音也不会比‘故意走两条路’更吵。”

2. “乱序执行”合同（Sequential Contract）：

   • 比喻： 现代厨师（CPU）喜欢乱序做菜（先做简单的，后做难的）。合同规定：“不管你怎么乱序，只要最后端出来的菜（泄露）是按顺序的就行。”
   • 证明： 作者证明了，即使真实芯片乱序做菜，只要它遵守某些规则，最终泄露给黑客的信息和“按顺序做菜”的合同是一样的。

总结

这篇论文就像给芯片安全领域提供了一套**“乐高积木式的证明工具”**。

• 以前： 证明芯片安全像徒手攀岩，既危险又累，容易掉下去（出错）。
• 现在： 有了这个工具，就像有了安全绳和自动上升器。工程师可以一步步、模块化地构建证明，利用“相对双模拟”来处理芯片那种“时快时慢、乱序执行”的复杂行为。

最终，这让软件开发者可以放心地相信：只要他们的程序符合高层的“合同”，底层的芯片就绝对不会因为微架构的漏洞而泄露秘密。这为防御像 Spectre 和 Meltdown 这样的超级黑客攻击提供了坚实的数学基础。

技术摘要

这是一份关于论文《A Deductive System for Contract Satisfaction Proofs》（合同满足性证明的演绎系统）的详细技术总结。

1. 研究背景与问题 (Problem)

背景：
在云计算等共享硬件环境中，侧信道攻击（如 Meltdown 和 Spectre）利用微架构泄露（如缓存状态、分支预测器状态）窃取秘密数据。为了防御此类攻击，研究者提出了硬件 - 软件合同（Hardware-Software Contracts）。这是一种在指令集架构（ISA）层面抽象描述 CPU 泄露行为的规范。

• 核心逻辑： 如果软件证明其程序在“合同”层面是安全的（即不泄露秘密），且硬件证明其满足该合同（即硬件的实际泄露被合同所覆盖/过近似），那么该软件在真实硬件上也是安全的。

问题：
验证硬件是否满足合同（Contract Satisfaction）是一个关键挑战。

• 现有方法的局限：
  • 测试与模型检测： 虽然自动化程度高，但依赖算法正确性，且难以处理复杂的归纳不变式。
  • 纸笔证明： 严谨但极其冗长且难以验证（例如，早期关于推测执行合同的证明长达 25 页密集文本）。
• 形式化验证的难点：
  • 四元关系推理（4-ary reasoning）： 合同满足性是一个超属性（Hyperproperty），需要同时比较两条合同执行轨迹和两条硬件执行轨迹。
  • 异步性（Asynchronicity）： 合同执行步骤与硬件执行步骤不同步（例如，硬件可能正确预测分支，而合同为了安全总是先执行错误分支，导致两者轨迹长度和步调不一致）。
  • 不变式构造困难： 现有的基于模拟关系（Simulation Relation）的方法通常需要预先猜测复杂的不变式，这在交互式证明助手（如 Rocq/Coq）中非常困难。

2. 方法论 (Methodology)

作者提出了一种基于**相对迹等式（Relative Trace Equality）**的演绎证明系统，并在交互式证明助手 Rocq 中进行了形式化。

2.1 核心概念：相对迹等式

合同满足性被定义为一种“迹等式蕴含迹等式”的问题：

如果两条合同轨迹相等（$\llbracket P \rrbracket_C(\sigma) = \llbracket P \rrbracket_C(\sigma')$），则两条硬件轨迹也必须相等（$\llbracket P \rrbracket_H(\mu, \sigma) = \llbracket P \rrbracket_H(\mu, \sigma')$）。

2.2 核心技术：相对双模拟（Relative Bisimulation）

为了解决上述挑战，作者引入了相对双模拟作为证明技术：

• 四元关系： 定义了一个包含四个状态（两个合同状态 $s_1, s_2$ 和两个硬件状态 $h_1, h_2$）的关系。
• 非同步推理（Non-lockstep reasoning）： 传统的锁步（lockstep）双模拟要求所有轨迹同步推进。但合同满足性中，合同轨迹和硬件轨迹可能不同步。
  • 解决方案： 作者设计了一个混合了**最大不动点（Coinduction，用于硬件轨迹）和最小不动点（Induction，用于合同轨迹）**的谓词。
  • 机制：
    • 硬件步骤（Coinductive）： 允许硬件轨迹异步推进，只要泄露相等即可。
    • 合同步骤（Inductive）： 合同轨迹的推进被视为归纳步骤，允许“跳过”合同步骤以匹配硬件状态，或者利用合同泄露不等（Leakage Inequality）来终止证明分支。
• 完备性： 证明了该相对双模拟关系在逻辑上等价于相对迹等式（Sound and Complete）。

2.3 演绎系统：参数化共归纳（Parameterized Coinduction）

为了在证明助手中高效地构建不变式，作者基于 Hur 等人提出的**参数化共归纳（Paco）框架，设计了一套五元组证明（Proof Quintuples）**规则：

• 证明状态： 使用五元组 $R \vdash \begin{bmatrix} s_1 & h_1 \\ s_2 & h_2 \end{bmatrix}$ 表示证明状态，其中 $R$ 是当前的归纳假设（不变式）。
• 核心规则：
  • C-Leak / C-Step： 处理合同侧。如果合同泄露不同，证明成立；或者跳过一步合同执行（利用归纳假设）。
  • H-Step： 处理硬件侧。如果硬件泄露相等，推进硬件状态（释放归纳假设的“守卫”）。
  • Invariant / Cycle / Guard： 用于累积不变式、检测循环和恢复守卫。
• 优势： 不需要预先提供完整的不变式，而是可以在证明过程中增量式地构建不变式。

2.4 增强技术（Up-To Techniques）

为了简化证明，作者引入了利用对称性和传递性的“向上（Up-To）”技术：

• 对称性： 允许在证明过程中交换状态顺序。
• 传递性： 允许将证明分解，例如通过引入中间状态来减少合同泄露或增加硬件泄露，从而简化不变式。
• 兼容性（Compatibility）： 证明了这些操作在参数化共归纳框架下是安全的（Sound）。

3. 主要贡献 (Key Contributions)

1. 形式化定义： 将合同满足性形式化为“相对迹等式”问题，并提出了**相对双模拟（Relative Bisimulation）**作为其充要条件。
2. 演绎系统： 开发了一套完整的演绎证明系统，支持**非锁步（Non-lockstep）**推理，能够处理合同与硬件执行速度的不匹配。
3. 增量证明风格： 基于参数化共归纳，实现了模块化、增量式的证明风格，无需预先猜测复杂的不变式。
4. Up-To 技术集成： 将对称性、传递性等简化原则安全地集成到证明系统中，显著降低了证明复杂度。
5. 形式化验证： 在 Rocq（Coq 的分支）中完整形式化了该系统，并证明了其可靠性（Soundness）和完备性（Completeness）。

4. 实验结果 (Results)

作者使用该系统在 Rocq 中对两个具有挑战性的硬件 - 软件合同进行了形式化验证：

1. 总是误预测合同（Always-Mispredict Contract）：

   • 场景： 模拟 Spectre 风格的分支预测错误和推测执行。合同总是先执行错误分支，然后回滚。
   • 验证： 成功证明了推测执行的硬件模型满足该合同。
   • 难点处理： 展示了系统如何处理合同与硬件在推测窗口（Speculation Window）内的异步执行（合同在错误分支上多走几步，硬件可能正确预测直接跳转）。

2. 顺序执行合同（Sequential Contract）：

   • 场景： 模拟乱序执行（Out-of-Order Execution）。合同假设指令按顺序执行，而硬件允许指令重排。
   • 验证： 成功证明了带有简单乱序缓冲区的硬件模型满足顺序执行合同。
   • 难点处理： 处理了指令重排导致的执行顺序差异，利用 Up-To 技术证明了交换可延迟指令不会改变泄露。

5. 意义与影响 (Significance)

• 提升形式化验证的可及性： 将原本需要数百行纸笔推导或复杂模型检测的任务，转化为交互式证明助手中可管理的、模块化的证明过程。
• 解决异步推理难题： 提出的混合不动点（Inductive-Coinductive）方法为处理不同步的系统（如推测执行、乱序执行）提供了通用的理论框架，不仅限于硬件合同，也可用于安全编译（Secure Compilation）等领域。
• 推动侧信道防御： 为构建可验证的、安全的硬件 - 软件接口提供了坚实的理论基础，有助于在硬件设计早期发现侧信道漏洞。
• 开源贡献： 提供了完整的 Rocq 形式化代码，为后续研究硬件安全验证提供了基准工具和库。

总结：
这篇论文通过引入“相对双模拟”和基于参数化共归纳的演绎系统，成功解决了硬件 - 软件合同满足性证明中复杂的四元关系和异步执行问题。它不仅提供了一种强大的形式化工具，还通过实际案例证明了其在验证现代 CPU 微架构（如推测执行和乱序执行）安全性方面的有效性和实用性。