一种在处理器 RTL 设计中检测瞬态执行侧信道的穷举方法
密码学与安全
2022-02-23 v3
摘要
近年来硬件（HW）安全问题以惊人的速度涌现。尤其是瞬态执行攻击，对现代计算系统的安全构成了切实威胁。尽管取得了近期进展，理解微体系结构设计决策对处理器安全性的复杂影响仍是一项巨大挑战，并在过去引发了多次更新周期。本文针对在寄存器传输级（RTL）保证处理器安全性的 HW 签核验证新方法的需求。为此，我们引入了关于瞬态执行攻击的安全的形式化定义，将其表述为一种 HW 属性。我们提出了一种基于唯一程序执行检查（UPEC）的形式化证明方法，可用于系统性地检测 RTL 设计中所有对瞬态执行攻击的漏洞。UPEC 不利用任何关于已知攻击的先验知识，因此也能检测基于新的、迄今未知的信道类型的漏洞。这通过我们在 UPEC 实验中发现的两种新攻击场景得到证明。UPEC 可扩展到广泛的 HW 设计，包括顺序处理器（RocketChip）、具有乱序写回的流水线（Ariane）以及具有深度乱序推测执行的处理器（BOOM）。据我们所知，UPEC 是首个穷举覆盖具有现实复杂性的处理器中瞬态执行侧信道的 RTL 验证技术。
引用
@article{arxiv.2108.01979,
title = {An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors},
author = {Mohammad Rahmani Fadiheh and Alex Wezel and Johannes Mueller and Joerg Bormann and Sayak Ray and Jason M. Fung and Subhasish Mitra and Dominik Stoffel and Wolfgang Kunz},
journal= {arXiv preprint arXiv:2108.01979},
year = {2022}
}