RTL Verification for Secure Speculation Using Contract Shadow Logic

TL;DR

The paper tackles RTL verification of speculative-execution defenses by introducing Contract Shadow Logic, a two-phase, architecture-driven approach that extracts ISA traces from out-of-order processors to verify software-hardware contracts. By shifting from four-machine baselines to a two-machine paradigm augmented with shadow logic, it achieves greater scalability and applicability across defenses, enabling both attack discovery on insecure designs and unbounded proofs for secure ones. The authors demonstrate superior performance against Baseline, LEAVE, and UPEC across multiple OoO processors and defense mechanisms, while acknowledging remaining scalability challenges and the potential for automation and taint-propagation enhancements. This work meaningfully improves practical RTL security verification for speculative vulnerabilities and offers a reusable framework that decouples security verification from functional RTL verification, with broad implications for processor security validation.

Abstract

Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from unknown vulnerabilities. Thus, a formal and rigorous evaluation of the ability of hardware designs to deal with speculative execution attacks is urgently desired. This paper proposes a formal verification technique called Contract Shadow Logic that can considerably improve RTL verification scalability while being applicable to different defense mechanisms. In this technique, we leverage computer architecture design insights to improve verification performance for checking security properties formulated as software-hardware contracts for secure speculation. Our verification scheme is accessible to computer architects and requires minimal formal-method expertise. We evaluate our technique on multiple RTL designs, including three out-of-order processors. The experimental results demonstrate that our technique exhibits a significant advantage in finding attacks on insecure designs and deriving complete proofs on secure designs, when compared to the baseline and two state-of-the-art verification schemes, LEAVE and UPEC.

Figures (2)

• Figure 1: Overview of Contract Shadow Logic.
• Figure 2: Verification time when varying the size of the register file, data memory, and re-order buffer.