一句话：提出契约影子逻辑，利用体系结构设计洞察提升 RTL 安全推测验证的可扩展性，既能发现攻击也能给出完整证明。
现代乱序处理器面临推测执行攻击，尽管已有多种软硬件缓解措施，新的漏洞仍不断出现，因此迫切需要严格形式化地评估硬件设计抵御此类攻击的能力。本文提出一种称为 Contract Shadow Logic 的形式验证技术，旨在以较少人工投入显著提升 RTL 验证的可扩展性，并适用于不同防御机制。该技术利用计算机体系结构设计经验，针对以软硬件契约形式表达的安全推测属性来改进验证性能，使计算机体系结构研究者无需深厚形式化方法背景即可使用。作者在多个 RTL 设计（包括三个乱序处理器）上评估了该技术，实验结果表明，与基线以及两种最先进的验证方案 LEAVE 和 UPEC 相比，该方法在发现不安全设计中的攻击以及对安全设计给出完整证明方面具有显著优势。
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 with little manual effort 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2407-12232,
title = {RTL Verification for Secure Speculation Using Contract Shadow Logic},
author = {Qinhan Tan and Yuheng Yang and Thomas Bourgeat and Sharad Malik and Mengjia Yan},
booktitle = {ASPLOS},
year = {2025},
doi = {10.1145/3669940.3707243}
}