RTL验证用于安全推测的契约影子逻辑
RTL Verification for Secure Speculation Using Contract Shadow Logic
AI总结：
本文提出契约影子逻辑，一种利用体系结构见解提升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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
