EVENT

Event News

Talk on "Verification of Side-Channel Security for Open-Source Processors via Leakage Contracts" by Prof. Jan Reineke from Saarland University (Saarbruecken, Germany)

We are pleased to inform you about the upcoming seminar by Prof. Jan Reineke from Saarland University (Saarbruecken, Germany) titled : "Verification of Side-Channel Security for Open-Source Processors via Leakage Contracts" Everyone interested is cordially invited to attend!

Title:

Verification of Side-Channel Security for Open-Source Processors via Leakage Contracts

Abstract:

Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations like caches and speculative execution. To use modern hardware securely, programmers must be aware of the security implications of these optimizations.
Unfortunately, instruction set architectures (ISAs), the traditional abstraction layer between hardware and software, are not an adequate basis for secure programming: they fully abstract away microarchitectural details and thus fail to capture their security implications.

To enable the construction of secure software systems on top of modern hardware, we have recently proposed leakage contracts as a new security abstraction at the ISA level. However, such contracts are only useful once processors are available that are known to satisfy them. In this talk, I will introduce LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts.

To scale to realistic processor designs, LeaVe exploits a new decoupling theorem that shows how to separate security and functional correctness concerns. LeaVe employs inductive reasoning on relational abstractions to obtain unbounded contract satisfaction proofs and invariant synthesis to automate the process. 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.

Speaker Bio:

Jan Reineke is a professor of computer science at Saarland University.
His research centers around problems at the boundary between hardware and software.

In the area of real-time systems, he is particularly interested in principles for the design of timing-predictable hardware and in precise and efficient timing-analysis techniques for multi-core architectures. His recent results include the design of the first provably timing-predictable pipelined processor design and the first exact analyses for LRU caches.

Another focus of his work are security vulnerabilities of hardware-software systems. Recent results include the development of automatic techniques to detect information leaks introduced by speculative execution, techniques to quantify the information leakage through cache side channels, and automatic methods to obtain highly detailed performance models for modern microarchitectures (uops.info).

In 2021 he received an ERC Advanced Grant, the European Union's most highly endowed research grant. His papers have been awarded multiple awards, most recently at CCS 2023, S&P ("Oakland") 2021, and RTSS 2023,2019 and 2018.