支持微架构防御的安全集成
密码学与安全
2026-01-09 v1 硬件体系结构
摘要
已有大量微架构级攻击导致了众多防御措施的提出。这产生了一个意料之外且尚未解决的安全问题：这些防御措施的朴素集成可能会引发安全漏洞。当一种防御改变了微架构中某个对另一种防御的安全性至关重要的方面时，就会发生这种情况。我们将此问题称为微架构防御假设违例（MDAV）。我们提出了一种两步法，用于在集成早期阶段筛查潜在的 MDAV。第一步是在安全属性的有界模型检验指导下，设计并集成一个组合模型。第二步是在模拟器上具体实现该模型，并通过模拟攻击进行评估。作为对第一步的支撑，我们提出了一种基于事件的建模框架 Maestro，用于测试和评估集成了防御的微架构模型。在我们的评估中，Maestro 揭示了 8 个 MDAV，支持紧凑的表达（约 15 倍的 Alloy 代码行比率），实现了语义可组合性并消除了性能下降（>100 倍）。作为对第二步的支撑，我们使用基于事件的模拟器（GEM5）来研究集成的微架构防御。我们表明，在某些最先进防御的朴素集成实现上可能发生隐蔽信道攻击，而使用我们的集成方法修复后的实现能够抵御该攻击。
引用
@article{arxiv.2601.05057,
title = {Supporting Secured Integration of Microarchitectural Defenses},
author = {Kartik Ramkrishnan and Stephen McCamant and Antonia Zhai and Pen-Chung Yew},
journal= {arXiv preprint arXiv:2601.05057},
year = {2026}
}