SpecVerif: RTL formal verification for detecting speculative execution trigger mechanisms

The continuous emergence of speculative execution vulnerabilities has posed a significant threat to processor security in recent years. It is imperative for hardware architects to conduct a comprehensive analysis of pre-silicon CPU designs for these vulnerabilities. However, formally verifying a complete speculative attack is challenging, because an end-to-end attack chain involves trigger generation, transient execution, covert-channel encoding, and secret reconstruction, which can lead to severe state-space explosion. This paper proposes SpecVerif, a formal verification framework for detecting misprediction-driven speculative execution trigger mechanisms. The key insight of SpecVerif is to decouple the trigger phase of speculative execution from covert-channel construction and secret leakage during formal analysis, thereby reducing the length of the checked attack chain. This allows the framework to focus on identifying instructions or RTL mechanisms that can open a transient execution window, rather than proving end-to-end exploitability. To realize this insight, we introduce an instruction-oriented differential verification scheme and a PC-based operand injection mechanism that injects controlled differences into the instruction under verification. We evaluated SpecVerif on two open-source RISC-V CPUs, BOOM and CVA6. Experimental results demonstrate that SpecVerif can effectively identify instructions capable of triggering speculative execution and provide bounded non-reachability evidence for instructions that do not violate the security property. Moreover, the framework requires only minimal manual annotations from the user. Our analysis also reveals a new potential speculative execution trigger mechanism in CVA6, which we term Spectre-JT.