IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2023 > Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

Zilong Wang

Tuesday, June 27, 2023

10:00am Meeting room 302 & Zoom3 https://zoom.us/j/3911012202 (pass: @s3)

Zilong Wang, PhD Student, IMDEA Software Institute

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

Abstract:

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 talk, we will introduce LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we will 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.