Spectre Attack Detection with Formal Method on RISC-V Processor at RTL Design Level

Spectre Attack Detection with Formal Method on RISC-V Processor at RTL Design Level

연구 분야: Cryptography

학회: 2025 International VLSI Symposium on Technology, Systems and Applications (VLSI TSA)

Speculative execution, widely used in modern processors, improves performance but is vulnerable to Spectre attacks. By mistraining the branch predictor, attackers execute transient instructions to access confidential data and leave traces in the cache, exposing sensitive information despite squashed instructions. Many detection methods have been proposed, but currently, none of them can be directly applied to processor design register transfer level (RTL) without any manual efforts to provide a robust and exhaustive exploration conclusion. This work proposes a formal verification detection workflow at RTL for determining spectre-induced vulnerabilities by focusing on two critical phases: speculative load data manipulation and cache state alteration during the speculative time window. In addition, our approach can validate its effectiveness by providing different detection results respectively on an out-of-order processor (RSD) without/with mitigation mechanisms and thus offer a rigorous solution to secure modern processors.