Supporting Secured Integration of Microarchitectural Defenses

TL;DR

The paper tackles the problem that integrating multiple microarchitectural defenses can create new security vulnerabilities (MDAVs). It introduces a two-step methodology: (1) Maestro, an event-based modeling framework with semantic composition, coupled with Alloy to exhaustively check security properties, and (2) GEM5-based simulation to validate concrete implementations against attacks. Key contributions include identifying eight MDAVs, achieving a ~15x Alloy LoC efficiency, enabling semantic composition, and demonstrating that certain integrated defenses can be resilient while others reveal MDAVs requiring fixes. The work provides a practical framework for early-stage defense integration, offering a path to safer, more scalable secure microarchitectures by systematically screening defenses before full hardware implementation.

Abstract

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.

Figures (3)

• Figure 1: An example illustrating key concepts in the construction of an event tree. A box represents an event instance. In a given step (column), an event exists in an active state (dark blue circle) or a pending state (light blue circle). An event always ends in an active state. The event tree represents the event sequence of a cache miss as explained in §\ref{['subsection:framework']}.
• Figure 2: The model integration workflow that we use to study the interaction between multiple defenses. We add defenses one at a time to build up a larger defense while allowing for the possibility to reject violation-causing defenses that we cannot revise (see §\ref{['subsection:framework']}).
• Figure 3: A timeline showing how the MDAV caused by sending coherence information to the core is exploited using the LRBS probe on a TORC + DSRC configuration. In case A, the timeline of the probe is shown, when a remote cache line in the E state is present in the LLC (slower due to redo). In case B, the timeline is shown when there is a cache miss (faster).