Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Leakage contracts aim to capture the information that processors leak through their microarchitectural implementations. However, so far, we lack a methodology to verify that a processor actually satisfies a given leakage contract. In this paper, we address this challenge by developing LEAVE, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we show how to decouple security and functional correctness concerns. 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 of three open-source RISC-V processors, thereby obtaining the first proofs of contract satisfaction for RTL processor designs.