13.11.2024
Automatically Uncovering Hardware Side-Channels in Processor RTL with Multi-μPATH Synthesis
Abstract
Modern hardware side-channel defenses are designed with respect to microarchitectural leakage contracts, which characterize microarchitectures' hardware side-channels. Numerous leakage contracts have been proposed in the literature and by industry (e.g., Arm DIT, Intel DOIT, RISC-V Zkt) to support a variety of hardware side-channel defenses, implemented in hardware or software. Yet, no automated nor scalable approach exists for formally verifying hardware adherence to any of them.
In this talk, I will present SynthLC, an automated approach/tool for synthesizing (“uncovering”) a variety of formally verified leakage contracts — which collectively support ten state-of-the-art hardware side-channel defense — from a SystemVerilog processor design, assuming an attacker that monitors program execution time or resource contention. SynthLC is built on top of another automated approach/tool, called RTL2MμPATH, for synthesizing (“uncovering”) a complete set of formally verified microarchitectural execution paths (μPATHs) for each instruction from processor RTL. This deign choice exploits our key observation: μPATH variability (>1 μPATH) for an instruction strongly indicates there is a hardware side-channel in the input design.
Bio
Caroline Trippel is an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University working in the area of computer architecture. A central theme of her work is leveraging formal methods techniques to design and verify hardware systems in order to ensure that they can provide correctness and security guarantees for the applications they intend to support. Trippel's research has been recognized with and NSF CAREER Award, IEEE Top Picks distinctions, the 2024 Intel Rising Star Award, the 2023 Intel Outstanding Researcher Award, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest® Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering. She was also awarded an NVIDIA Graduate Fellowship (2017-2018) and selected to attend the 2018 MIT Rising Stars in EECS Workshop.
If you want to join, contact socialmedia@iaik.tugraz.at until 13th of Nov, 15:00 for the invite link!
Modern hardware side-channel defenses are designed with respect to microarchitectural leakage contracts, which characterize microarchitectures' hardware side-channels. Numerous leakage contracts have been proposed in the literature and by industry (e.g., Arm DIT, Intel DOIT, RISC-V Zkt) to support a variety of hardware side-channel defenses, implemented in hardware or software. Yet, no automated nor scalable approach exists for formally verifying hardware adherence to any of them.
In this talk, I will present SynthLC, an automated approach/tool for synthesizing (“uncovering”) a variety of formally verified leakage contracts — which collectively support ten state-of-the-art hardware side-channel defense — from a SystemVerilog processor design, assuming an attacker that monitors program execution time or resource contention. SynthLC is built on top of another automated approach/tool, called RTL2MμPATH, for synthesizing (“uncovering”) a complete set of formally verified microarchitectural execution paths (μPATHs) for each instruction from processor RTL. This deign choice exploits our key observation: μPATH variability (>1 μPATH) for an instruction strongly indicates there is a hardware side-channel in the input design.
Bio
Caroline Trippel is an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University working in the area of computer architecture. A central theme of her work is leveraging formal methods techniques to design and verify hardware systems in order to ensure that they can provide correctness and security guarantees for the applications they intend to support. Trippel's research has been recognized with and NSF CAREER Award, IEEE Top Picks distinctions, the 2024 Intel Rising Star Award, the 2023 Intel Outstanding Researcher Award, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest® Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering. She was also awarded an NVIDIA Graduate Fellowship (2017-2018) and selected to attend the 2018 MIT Rising Stars in EECS Workshop.
If you want to join, contact socialmedia@iaik.tugraz.at until 13th of Nov, 15:00 for the invite link!