Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction at the instruction set architecture (ISA) level that captures microarchitectural leakage. Hardware-software leakage contracts have recently been proposed as such an abstraction. In this paper, we propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. For a given ISA, our approach relies on human experts to (a) capture the space of possible contracts in the form of contract templates and (b) devise a test-case generation strategy to explore a microarchitecture's potential leakage. For a given implementation of an ISA, these two ingredients are then used to automatically synthesize the most precise leakage contract that is satisfied by the microarchitecture. We have instantiated this methodology for the RISC-V ISA and applied it to the Ibex and CVA6 open-source processors. Our experiments demonstrate the practical applicability of the methodology and uncover subtle and unexpected leaks.

翻译：微架构攻击通过利用缓存和推测执行等微架构优化的软件可见痕迹来破坏安全性。在软件层面防御此类攻击需要在指令集架构（ISA）层面建立恰当的抽象，以捕获微架构泄漏。硬件-软件泄漏契约近期被提出作为此类抽象方案。本文提出一种面向开源微架构的半自动化硬件-软件泄漏契约合成方法。针对特定ISA，我们的方法依赖人类专家完成两项工作：（a）以契约模板形式捕捉可能的契约空间，以及（b）设计测试用例生成策略以探索微架构的潜在泄漏。对于ISA的特定实现，这两个要素将用于自动合成该微架构所满足的最精确泄漏契约。我们已将该方法论实例化于RISC-V ISA，并应用于Ibex与CVA6两款开源处理器。实验验证了该方法论的实践可行性，并揭示了细微且非预期的泄漏现象。