Rigorous Evaluation of Microarchitectural Side-Channels with Statistical Model Checking

TL;DR

This work addresses the challenge of rigorously evaluating probabilistic microarchitectural side channels by applying Statistical Model Checking (SMC) to cycle-accurate simulators. By treating the system as an opaque box and formulating security questions as STL properties, the authors obtain statistically backed guarantees without relying on distributional assumptions or simplified models. Through three case studies—Prime+Probe, ScatterCache vs Mirage, and CleanupSpec/unXpec with obfuscated cleanup latency—the paper demonstrates how SMC yields actionable, quantitative insights into attacker success probabilities, defense effectiveness, and performance trade-offs. The results enable precise planning of noise injection and obfuscation strategies, offering a practical pathway for defenders to achieve targeted security levels with controllable costs. The approach is broadly applicable to real hardware or detailed simulators and establishes SMC as a robust tool for security evaluation in modern microarchitectures.

Abstract

Rigorous quantitative evaluation of microarchitectural side channels is challenging for two reasons. First, the processors, attacks, and defenses often exhibit probabilistic behaviors. These probabilistic behaviors arise due to natural noise in systems (e.g., from co-running processes), probabilistic side channel attacks, and probabilistic obfuscation defenses. Second, microprocessors are extremely complex. Previous evaluation methods have relied on abstract or simplified models, which are necessarily less detailed than real systems or cycle-by-cycle simulators, and these models may miss important phenomena. Whereas a simple model may suffice for estimating performance, security issues frequently manifest in the details. We address this challenge by introducing Statistical Model Checking (SMC) to the quantitative evaluation of microarchitectural side channels. SMC is a rigorous statistical technique that can process the results of probabilistic experiments and provide statistical guarantees, and it has been used in computing applications that depend heavily on statistical guarantees (e.g., medical implants, vehicular computing). With SMC, we can treat processors as opaque boxes, and we do not have to abstract or simplify them. We demonstrate the effectiveness of SMC through three case studies, in which we experimentally show that SMC can evaluate existing security vulnerabilities and defenses and provide qualitatively similar conclusions with greater statistical rigor, while making no simplifying assumptions or abstractions. We also show that SMC can enable a defender to quantify the amount of noise necessary to have a desired level of confidence that she has reduced an attacker's probability of success to less than a desired threshold, thus providing the defender with an actionable plan for obfuscation via noise injection.

Figures (9)

• Figure 1: Experiment 1.1a: P&P Success Probability vs. Noise Level. We use the Clopper-Pearson method to build confidence intervals for the probability of attack success for 5 distinct levels measuring the magnitude of injected noise. As one collects more data (i.e., for larger $N$), one can make more precise assertions about the security confidence interval.
• Figure 2: Confidence Attack Success Probability $<F$ vs Number of Failed Attacks Observed for different values of $F$. This experiment empirically shows that in experiments in which we only observe failed attacks, we must collect significantly more samples to be confident in high (e.g., >=99%) security.
• Figure 3: Experiment 1.1b: P&P Success Probability vs. Number of Cache Replacements. We evaluate the probability that an attack will succeed given a cache replacement number in the range (A-B, A+B). We use the Clopper-Pearson method to generate confidence intervals for the attack's success probability in the varying windows of the number of cache replacements for our 5 different noise levels. With this information, we can monitor system security with cache replacements as a proxy, and potentially inject noise to artificially drive up replacements to maintain a desired security level.
• Figure 4: Tunnel Graph Creation Methodology. Similar to how SPA mazurek:micro:2023 creates a confidence interval by iterating on a discrete metric in an SMC property along one dimension, a tunnel graph creates 2-dimensional intervals by: iterating on discrete input data filters, constructing new confidence intervals (either with SPA or Clopper-Pearson), and connecting their bounds in a 2D graph. Since each confidence interval adheres to a certain, user-specified confidence level, our entire tunnel graph does as well. Making the iterations in both dimensions more granular provides more continuous insights.
• Figure 5: Experiment 1.2: P&P Attack Success Probability vs. Frequency of Noise Injection. We create a tunnel graph to evaluate the relationship between obfuscation and success probability. As outlined in Figure \ref{['fig:tunnel_graph_diagram']}, we iterate on a window of noise magnitude to filter samples. We use the Clopper-Pearson method to generate 90% confidence intervals on the attack success probability at each noise window and thus create a 90% confidence tunnel. Noise does not manifest in discrete levels in real systems so it is valuable to have a rigorous and continuous understanding of the relationship between noise and attack success.