Hardware-software contracts are abstract specifications of a CPU's leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without having to explicitly reason about the microarchitectural details of the CPU. Using the abstraction powers of a contract requires proving that the targeted CPU satisfies the contract in the sense that the contract over-approximates the CPU's leakage. Besides pen-and-paper reasoning, proving contract satisfaction has been approached mostly from the model-checking perspective, with approaches based on a (semi-)automated search for the necessary invariants. As an alternative, this paper explores how such proofs can be conducted in interactive proof assistants. We start by observing that contract satisfaction is an instance of a more general problem we call relative trace equality, and we introduce relative bisimulation as an associated proof technique. Leveraging recent advances in the field of coinductive proofs, we develop a deductive proof system for relative trace equality. Our system is provably sound and complete, and it enables a modular and incremental proof style. It also features several reasoning principles to simplify proofs by exploiting symmetries and transitivity properties. We formalized our deductive system in the Rocq proof assistant and applied it to two challenging contract satisfaction proofs.

翻译：硬件-软件契约是CPU泄漏行为的抽象规约，它们使得在不显式推演CPU微架构细节的情况下，能够验证高级程序抵抗侧信道攻击的安全性。使用契约的抽象能力需要证明目标CPU满足该契约，即契约对CPU泄漏行为具有过近似性。除纸笔推演外，契约满足性证明目前主要采用模型检验方法，基于（半）自动搜索必要不变量。作为替代方案，本文探讨如何在交互式证明助手中开展此类证明。我们首先发现契约满足性是一个更一般问题（我们称之为相对迹等价）的实例，并引入相对互模拟作为关联证明技术。利用余归纳证明领域的最新进展，我们为相对迹等价开发了一个演绎证明系统。该系统具有可证明的可靠性和完备性，支持模块化与增量式证明风格。系统还包含若干推理原则，通过利用对称性和传递性简化证明过程。我们在Rocq证明助手中形式化了该演绎系统，并将其应用于两个具有挑战性的契约满足性证明案例。