Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural implementations. However, so far, we lack a verification methodology to check that a processor actually satisfies a given leakage contract. In this paper, we address this problem by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction. LeaVe leverages this decoupling to make verification of contract satisfaction practical. To scale to realistic processor designs LeaVe further employs inductive reasoning on relational abstractions. Using LeaVe, we precisely characterize the side-channel security guarantees provided by three open-source RISC-V processors, thereby obtaining the first contract satisfaction proofs for RTL processor designs.

翻译：泄露契约最近被提出作为指令集架构（ISA）层面的一种新的安全抽象机制。此类契约旨在准确反映处理器通过微架构实现的副作用可能泄露的信息。然而，目前尚缺乏一种验证方法学来检验处理器是否实际满足给定泄露契约。本文通过开发LeaVe——首个针对寄存器传输级（RTL）处理器设计验证ISA级泄露契约的工具——解决了这一问题。为此，我们引入了解耦定理，该定理在验证契约满足性时将安全性与功能正确性关注点分离。LeaVe利用这种解耦使得契约满足性验证变得切实可行。为了扩展到实际处理器设计，LeaVe进一步采用基于关系抽象上的归纳推理。通过使用LeaVe，我们精确刻画了三个开源RISC-V处理器所提供的侧信道安全保障，从而首次获得了RTL处理器设计的契约满足性证明。