  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.
