Supporting Secured Integration of Microarchitectural Defenses

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autori principali: Ramkrishnan, Kartik, McCamant, Stephen, Zhai, Antonia, Yew, Pen-Chung
Natura: Preprint
Pubblicazione: 2026
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866912810206756864
author Ramkrishnan, Kartik
McCamant, Stephen
Zhai, Antonia
Yew, Pen-Chung
author_facet Ramkrishnan, Kartik
McCamant, Stephen
Zhai, Antonia
Yew, Pen-Chung
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2601_05057
institution arXiv
publishDate 2026
record_format arxiv
spellingShingle Supporting Secured Integration of Microarchitectural Defenses
Ramkrishnan, Kartik
McCamant, Stephen
Zhai, Antonia
Yew, Pen-Chung
Cryptography and Security
Hardware Architecture
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.
title Supporting Secured Integration of Microarchitectural Defenses
topic Cryptography and Security
Hardware Architecture
url https://arxiv.org/abs/2601.05057