Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL

Inhalt:
Spectre and Meltdown attacks proved Transient Execution Side Channels to be a notable challenge for designing secure microarchitectures. In this overview paper, we present a recently published secure-by-construction RTL design methodology addressing this issue. Our methodology is based on a new hardware protection framework underpinned by a generic control infrastructure that can be integrated into industry-grade microarchitectures. The methodology uses formal verification to systematically detect possible leakage paths and to customize the generic infrastructure accordingly for the design. We propose an iterative flow which semi-automatically leads to an RTL design that is guaranteed to be secure w.r.t. transient execution attacks. In addition, our case study on BOOMv3, an open-source RISC-V processor with a deep out-of-order pipeline, shows the feasibility and scalability of our methodology, resulting in competitive performance compared to other microarchitectures for secure speculation.