There has been a plethora of microarchitectural-level attacks leading to many proposed countermeasures. This has created an unexpected and unaddressed security issue where naive integration of those defenses can potentially lead to security vulnerabilities. This occurs when one defense changes an aspect of a microarchitecture that is crucial for the security of another defense. We refer to this problem as a microarchitectural defense assumption violation} (MDAV). We propose a two-step methodology to screen for potential MDAVs in the early-stage of integration. The first step is to design and integrate a composed model, guided by bounded model checking of security properties. The second step is to implement the model concretely on a simulator and to evaluate with simulated attacks. As a contribution supporting the first step, we propose an event-based modeling framework, called Maestro, for testing and evaluating microarchitectural models with integrated defenses. In our evaluation, Maestro reveals MDAVs (8), supports compact expression (~15x Alloy LoC ratio), enables semantic composability and eliminates performance degradations (>100x). As a contribution supporting the second step, we use an event-based simulator (GEM5) for investigating integrated microarchitectural defenses. We show that a covert channel attack is possible on a naively integrated implementation of some state-of-the-art defenses, and a repaired implementation using our integration methodology is resilient to the attack.

翻译：微架构层面的攻击层出不穷，催生了大量相应的防护措施。然而，这些防御措施的简单集成可能引发意料之外且尚未解决的安全问题，即当一种防御措施改变了微架构的某个方面，而该方面对另一种防御措施的安全性至关重要时，就会产生安全漏洞。我们将此问题称为微架构防御假设违反（MDAV）。本文提出一种两步法，用于在集成早期阶段筛查潜在的MDAV。第一步是在安全属性的有界模型检验指导下，设计并集成组合模型。第二步是在模拟器上具体实现该模型，并通过模拟攻击进行评估。作为支持第一步的贡献，我们提出一个基于事件的建模框架——Maestro，用于测试和评估集成防御措施的微架构模型。在我们的评估中，Maestro揭示了MDAV（8个），支持紧凑的表达（约15倍Alloy代码行数比），实现了语义可组合性并消除了性能下降（>100倍）。作为支持第二步的贡献，我们使用基于事件的模拟器（GEM5）研究集成的微架构防御。我们证明，在某些先进防御措施的简单集成实现上可能发生隐蔽信道攻击，而采用我们集成方法修复后的实现能够抵御此类攻击。