Rigorous Evaluation of Microarchitectural Side-Channels with Statistical Model Checking

• URL: http://arxiv.org/abs/2510.02475v1
• Date: Thu, 02 Oct 2025 18:31:06 GMT
• Title: Rigorous Evaluation of Microarchitectural Side-Channels with Statistical Model Checking
• Authors: Weihang Li, Pete Crowley, Arya Tschand, Yu Wang, Miroslav Pajic, Daniel Sorin,
• Abstract summary: We introduce Statistical Model Checking to the quantitative evaluation of microarchitectural side channels.<n>With SMC, we can treat processors as opaque boxes, and we do not have to abstract or simplify them.<n>We demonstrate the effectiveness of SMC through three case studies.
• Score: 10.093795733515181
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Model Tampering Attacks Enable More Rigorous Evaluations of LLM Capabilities [49.09703018511403]
  Evaluations of large language model (LLM) risks and capabilities are increasingly being incorporated into AI risk management and governance frameworks.<n>Currently, most risk evaluations are conducted by designing inputs that elicit harmful behaviors from the system.<n>We propose evaluating LLMs with model tampering attacks which allow for modifications to latent activations or weights.
  arXiv  Detail & Related papers  (2025-02-03T18:59:16Z)
• What Are the Odds? Improving the foundations of Statistical Model Checking [3.789219860006095]
  Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty.<n>Traditionally verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP.<n>We propose specialised approaches that exploit our knowledge of the MDP.
  arXiv  Detail & Related papers  (2024-04-08T11:47:46Z)
• White-box validation of quantitative product lines by statistical model checking and process mining [1.0918484507642576]
  We propose a novel methodology for validating software product line (PL) models by integrating Statistical Model Checking (SMC) with Process Mining (PM) Our approach focuses on the feature-oriented language QFLan in the PL engineering domain, allowing modeling of PLs with rich cross-tree and quantitative constraints.
  arXiv  Detail & Related papers  (2024-01-23T17:27:13Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. We use state-of-the-art verification techniques to provide guarantees on the interval Markov decision process and compute a controller for which these guarantees carry over to the original control system.
  arXiv  Detail & Related papers  (2023-01-04T10:40:30Z)
• Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty [68.00748155945047]
  Capturing uncertainty in models of complex dynamical systems is crucial to designing safe controllers. Several approaches use formal abstractions to synthesize policies that satisfy temporal specifications related to safety and reachability. Our contribution is a novel abstraction-based controller method for continuous-state models with noise, uncertain parameters, and external disturbances.
  arXiv  Detail & Related papers  (2022-10-12T07:57:03Z)
• Random Noise vs State-of-the-Art Probabilistic Forecasting Methods : A Case Study on CRPS-Sum Discrimination Ability [4.9449660544238085]
  We show that the statistical properties of target data affect the discrimination ability of CRPS-Sum. We highlight that CRPS-Sum calculation overlooks the performance of the model on each dimension. We show that it is easily possible to have a better CRPS-Sum for a dummy model, which looks like random noise.
  arXiv  Detail & Related papers  (2022-01-21T12:36:58Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  We present a novel planning method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP)
  arXiv  Detail & Related papers  (2021-10-25T06:18:55Z)
• Probabilistic robust linear quadratic regulators with Gaussian processes [73.0364959221845]
  Probabilistic models such as Gaussian processes (GPs) are powerful tools to learn unknown dynamical systems from data for subsequent use in control design. We present a novel controller synthesis for linearized GP dynamics that yields robust controllers with respect to a probabilistic stability margin.
  arXiv  Detail & Related papers  (2021-05-17T08:36:18Z)
• Nonintrusive Uncertainty Quantification for automotive crash problems with VPS/Pamcrash [0.0]
  surrogate models (metamodels) allow drastically reducing the computational cost of Monte Carlo process. kernel Principal Component Analysis (kPCA) is found to be effective to simplify the model outcome description. A benchmark crash test is used to show the efficiency of combining metamodels with kPCA.
  arXiv  Detail & Related papers  (2021-02-15T16:59:39Z)
• SAMBA: Safe Model-Based & Active Reinforcement Learning [59.01424351231993]
  SAMBA is a framework for safe reinforcement learning that combines aspects from probabilistic modelling, information theory, and statistics. We evaluate our algorithm on a variety of safe dynamical system benchmarks involving both low and high-dimensional state representations. We provide intuition as to the effectiveness of the framework by a detailed analysis of our active metrics and safety constraints.
  arXiv  Detail & Related papers  (2020-06-12T10:40:46Z)
• Efficient statistical validation with edge cases to evaluate Highly Automated Vehicles [6.198523595657983]
  The widescale deployment of Autonomous Vehicles seems to be imminent despite many safety challenges that are yet to be resolved. Existing standards focus on deterministic processes where the validation requires only a set of test cases that cover the requirements. This paper presents a new approach to compute the statistical characteristics of a system's behaviour by biasing automatically generated test cases towards the worst case scenarios.
  arXiv  Detail & Related papers  (2020-03-04T04:35:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.