Spectres, Meltdowns, Zombies, Orcs: Can formal methods banish the ghosts that haunt our computing systems?

Wolfgang Kunz (RPTU Kaiserslautern, D)

Abstract

Hardware (HW) security violations have been reported at an alarming rate in recent years.  Attacks based on microarchitectural side channels, such as Spectre and Meltdown, pose a genuine threat to the security of modern computing systems. Despite recent advances, understanding the intricate implications of microarchitectural design decisions on processor security remains a great challenge and has caused a number of update cycles in the past.

This talk addresses the challenge of formal security analysis in Systems-on-Chip. We discuss challenges related to transient execution side channels, such as Spectre and Meltdown, security violating design bugs and HW weaknesses violating data obliviousness. We present a formal method called Unique Program Execution Checking (UPEC) to detect such vulnerabilities. UPEC does not require a priori knowledge on possible attacks and detects HW vulnerabilities systematically without demanding the clever thinking of a human attacker.

We present several cases studies on open-source RISC-V systems including Rocketchip, Ariane, BOOM and Pulpissimo.

Curriculum Vitae

Since 2001 Wolfgang Kunz is a professor at the Department of Electrical & Computer Engineering at Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau (RPTU).
He conducts research in the area of System-on-Chip design and verification and has been collaborating with numerous industrial partners including AbsInt, Bosch, IBM, Infineon, Intel, Minres, OneSpin Solutions, Siemens EDA and Xilinx.
For his research activities Wolfgang Kunz received several awards including the Berlin Brandenburg Academy of Science Award. For works related to this talk, he and his team recently received the Intel Hardware Security Award 2022 and the DAC-22 Best Paper Award. Wolfgang Kunz is a Fellow of the IEEE and a member of Academia Europaea.