Wankupi's Website
HomeBlog

Interplay of Efficient Model Checking and Secure Processor Design: A Case Study on Secure Speculation

很荣幸能在 2025 年的暑假和秋季学期，加入 Mengjia Yan 老师的研究团队，与 Tingzhen Dong 及其他老师同学一起合作完成了这篇论文，收获了我人生中第一次 Submission 和 Publication。

文章链接，Artifact链接

本文将从更 engineering 视角回顾这篇工作。也许之后随着我理解深入，我可以再写一篇更学术性的介绍。 但是现在我的讲故事功底还不太足，只好先讲一讲其中的过程，权当记录。

TLDR:

  • 我们发现证明 Non-interference 问题不需要完整证明处理器的正确性，而只需要信息流相关的性质。
  • 我们提出了 HUF, 一种模块级信息流抽象方法，并搭建了证明框架 SHUFFLE。
  • 我们提出了一些可以让防御机制更容易证明的设计思路。
  • 我们在 BOOM 处理器上验证了我们的方法和设计思路。

Start by Learning

在故事的最初，我们有一个明确的目标：验证乱序处理器不会通过时间侧信道泄漏数据。以下是一些相关概念。

Contract

首先回顾 Spectre 攻击的原理。乱序处理器在执行分支指令时会进行预测，预测错误时，预测执行的指令虽然不改变架构状态，但是改变了微架构的状态。这导致其他指令完成时间受到影响，从时间侧信道泄漏了数据。

Contract 建模了处理器不受到 Spectre 攻击的条件。 基本思想是，如果一个程序在顺序单步模拟执行的情况下，它每条指令的 commit 时间都不受到隐私数据的影响，那么处理器应当保证这个程序在实际执行的时候，每条指令的 commit 时间也不受到隐私数据的影响。 其中的主要关键点就是处理器内部可能存在预测执行，但是我们要求预测执行不会对 commit 时间产生影响。

在验证场景下，LeaVe 给出了最早的建模，使用了 2 个 ISA Machine 和 2 个 OoO Machine； 《RTL Verification for Secure Speculation Using Contract Shadow Logic》给出了仅使用 2 个 OoO Machine 的简化构造。

PDR/IC3

PDR/IC3 是一种模型检验算法，适用于证明某命题在状态转移下恒成立。我们用了一段时间学习 IC3 的原理和实现细节，并最终选择了开源的 rIC3 作为我们的模型检验工具。

选择 rIC3 的主要动机是开源的特性使得我们可以在 timeout 的情况下，具体分析验证的中间结果，定位到难以 scale 的原因。

这里也简单描述一下 IC3 的原理。整体的逻辑类似于寻找循环不变量，IC3 不断构造出一些 lemma, 其中有些是归纳的，有些不是归纳的，最终在证明结束时，所有的 lemma 与(AND)在一起是归纳的，并且能导出我们想要证明的性质。

Berkeley BOOM

一个开源的乱序处理器，具有完整的乱序执行机制，支持分支预测等特性，是我们验证的理想对象。

背景

在硬件验证这一领域，有两种常见做法：

  1. 形式化证明: 使用 Rocq, BlueSpec 等形式化工具，人工对处理器建模并撰写证明，由程序检查证明的正确性;
  2. 模型检验: 通过模型检验工具 (如 rIC3, z3, ABC 等)，将处理器建模为状态转移系统，自动证明所有可达状态空间均满足性质。

先前一些工作如 UPec 使用人工提供引理的方式证明。 组里的学长尝试过使用 JasperGold（一个商业模型验证工具）进行验证，但是 scalability 问题比较严重，只能验证非常小的乱序处理器。

那么为什么迁移到大型乱序处理器上就无法处理了呢？我们从两个方向进行了探索。

  1. 理论分析，IC3 这种算法的能力边界是什么？是否足以证明我们想要的性质？
  2. 实验分析，在检验过程中，Model Checker 遇到了哪些瓶颈？

理论分析告诉我们需要 Model Checker 需要支持一个特定的 assume/assert 语义才能处理 Constant Time Contract，但是现在的 rIC3 不支持，因此我们的这篇工作局限在 SISP 和 Sandbox Contract 这两个问题上。

实验分析成功定位到了瓶颈，据此我们提出了一个优化方法。 这个 insight 对验证性能提升更直接，也是这篇工作主要的内容和贡献的来源。

Bottlenecks

在大约学习和讨论了一个月左右后，我们渐渐理解了各类算法和工具。然后尝试了 SISP 问题的验证。

SISP 问题相比 Contract 更简单。 最主要的区别是，SISP 的前条件更强，保证所有输入的指令都是 constant time 的，与之相比，Contract 对程序的指令集本身没有要求，要求的是模拟执行情况下的运行不受数据影响。 选择 SISP 的原因是我们认为它更容易验证，能够更快地得到结果。

SISP 和 Contract 的共同点是，都可以表达为 non-interference 问题。 Non-interference 问题是说，对于一个系统，某个输入的变化不会影响某个输出的值。 因此 SISP 和 Contract 在 verilog 层面的建模是类似的。 我们检验 non-interference 的办法是构造两个处理器实例，执行相同的指令序列，唯一的区别在于输入的隐私数据是独立的，然后证明这两个处理器实例的 commit 时间是相同的。 (这一步还有其他构造方式，比如 taint-tracking，但是我们选择了self-composition 这种最精确的方式)

实验结果显示，rIC3 验证 SISP 问题时，同样会遇到 scalability 的问题。 我们简单修改了 rIC3，使其输出中间结果。分析后发现，当证明停滞时，大部分的 lemma 都包含着诸如 rob, rename, issue 的内部状态的量，并且看不出这些 lemma 具体如何解释。

我们尝试进行了一些人工推理。assert 的是最终 commit 时间相等，那么为了证明这个性质，我们需要一些 lemma 表达影响 commit 的量也是相等的。由此反溯，表达某些量相等的 lemma 对这个问题来说更有意义一些。

因此我们定位到了 Bottleneck: rIC3 生成的 lemma 中很多只是在表达某些结构的值应该是什么状态，但这些 lemma 与我们的问题关联不大。

HUF & SHUFFLE

因此我们希望找一种方法，能够引导 rIC3 生成更有意义的 lemma。

Qinhan 告诉了我们一个方式是 Uninterpreted Function (UF)，是一种在 SAT/SMT 中常用的抽象方法，可以将一些复杂的函数抽象为一个黑盒函数，只关心它的输入输出关系，而不关心它的内部实现。

遵循着这样一种 idea, 我们开始思考在处理器的验证中，是否也可以使用类似的抽象方法来引导模型检验工具生成更有意义的 lemma，或者说阻止模型检验工具生成一些无关的 lemma。

根据上文讲述的观察结果，主要卡住的地方在于 ROB, Rename, Issue 这种包含复杂时序逻辑的模块。 如果我们尝试分析，其实我们并不会在意一个 logical register 对应的 physical register 具体是谁，也不在意一个指令在 ROB 中的具体位置。我们关注的只是它是不是被放入了正确的 Execution Unit，是否经过了常量时间完成执行。

因此我们提出了 HUF (Uninterpreted Function with History)，一种针对时序逻辑的抽象方法。 HUF 的基本思想是，如果一个 module 自始至终的输入在self-composition 中都相等(与隐私数据无关)，那么它的输出也应该相等(与隐私数据无关)。 我们就可以构造一个简化的逻辑取代原本的复杂逻辑，只要记录输入的历史相等状态，然后据此输出一个随机的值。 这一步的合理性在于 Model Checker 检查了“随机”的所有可能取值。

在论文中，我们详细描述了 HUF 的构造和一些变体，以及针对变体的合理性证明（Refinement Proof）。 这一些系列技术性的东西合在一起成为了我们的证明框架 SHUFFLE。

讲一个细节，这一步我们发现的最有意思的地方在于，我们其实可以将 ROB 也完全抽象掉。 抽象 ROB 对验证性能的提升是非常显著的。 经过消融分析，我们发现其中起决定性作用的是将新指令的 rob_idx 抽象为随机数。 Rob 正常情况下应当保证指令拥有顺序且唯一的编号，并且按照顺序进行提交，这其实是一个很强的结构约束。 模型检验工具在生成 lemma 时会试图表达这个结构约束，从而导致生成了很多无关的 lemma。

HUF 非常适合用于在 non-interference 问题下，解耦 functionality 和 information-flow。

借助 HUF, 通过将绝大多数的模块都抽象，仅保留少数必要的 functionality （如 decode），我们成功加速了 SISP 问题的证明。

Secure Hardware Design

证明了 SISP 之后，大概是八月份或是九月份，我们回到了更关心的 Contract 上面。

我们首先尝试了一个简单的防御策略，delayHeadOfRob。 这个策略是将所有 load 指令都推迟执行，直到这个指令到达了 Head Of Rob。 从防御的角度，这样可以确保 load 一定会提交（不考虑外部中断等），那么根据 Sandbox Contract 语义，软件应该保证此刻读入的内存是非隐私数据。

但实际上，为了使用 2 Machine 的构造进行验证，我们并没有提前对程序进行检查，而是在 commit 的时候，通过 assume 两个 Machine 的 commit write back data 是相等的来限制 Model Checker 只考虑 commit data 相等的程序。 这就带来一个问题是，在我们这样的构造下，commit 前 Model Checker 都对内存数据没有任何限制，相当于两个无关的随机值。 我们必须要求 Model Checker能对 write back data 进行的及时的限制，而这只发生在 commit 周期，因此也导致我们的证明强依赖于 ROB 的顺序性。 但这并不是一个 trivial 的命题。

于是我们有两条路可以选：

  • 尝试证明这种困难的 Functionality, 然后在证明 security 时 assume 它；
  • 尝试从头设计一套新防御机制，依赖更少的 functionality。

我们选择了第二条路。

我们设计了一个名为 DelayForwarding-All 的防御机制。 使用一个类似 cache 结构的 buffer, 先将指令的结果存储起来，然后 Rob 说哪个指令 commit，它就释放哪个结果。 在使用 HUF 之后，虽然 Rob 不再按顺序 commit，但我们可以保证对数据的 assumption check 和数据进入流水线是同时发生。

在这个过程中，我很细致地读了 Boom 的源代码，同时为了修改，也学习了 Chisel，感觉自己的体系结构知识变得更完整了一些。

这个防御机制被我们成功证明。这是在 Sandbox Contract 这个问题下，第一个不需要人工参与太多的并且被证明的防御。 虽然有点针对方法特别优化的成分，我们认为这种将验证时的 insight 反过来引导硬件设计的思路，也有其思考价值。

我们还在一个与之类似但更 fine-grained 的防御机制上尝试了证明，最终在人工提供一些帮助的情况下（我们倒是可以说相对干净地提供帮助），在减小规模的 BoomCore 上完成了证明。 这个防御上我们投入了很多时间，甚至最终十一月投稿前一周我们还在尝试优化这里的证明。 虽然并没能彻底解决这个问题，但至少我们的理解变得清晰许多，也算是我们对这个问题的一点贡献。

尾声

感谢看到这里。也再次感谢在这篇工作中参与或帮助过我们的人们。

对我来说，这是一次很极限、也很有纪念意义的投稿。

深深感到未来还有很长路要走。

仍需继续努力。