Global Microprocessor Correctness in the Presence of Transient Execution

• URL: http://arxiv.org/abs/2506.17154v1
• Date: Fri, 20 Jun 2025 16:56:14 GMT
• Title: Global Microprocessor Correctness in the Presence of Transient Execution
• Authors: Andrew T. Walter, Konstantinos Athanasiou, Panagiotis Manolios,
• Abstract summary: We advocate for the use of formal specifications, using the theory of refinement.<n>We introduce notions of correctness that can be used to deal with transient execution attacks, including Meltdown and Spectre.
• Score: 0.16385815610837165
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Correctness for microprocessors is generally understood to be conformance with the associated instruction set architecture (ISA). This is the basis for one of the most important abstractions in computer science, allowing hardware designers to develop highly-optimized processors that are functionally "equivalent" to an ideal processor that executes instructions atomically. This specification is almost always informal, e.g., commercial microprocessors generally do not come with conformance specifications. In this paper, we advocate for the use of formal specifications, using the theory of refinement. We introduce notions of correctness that can be used to deal with transient execution attacks, including Meltdown and Spectre. Such attacks have shown that ubiquitous microprocessor optimizations, appearing in numerous processors for decades, are inherently buggy. Unlike alternative approaches that use non-interference properties, our notion of correctness is global, meaning it is single specification that: formalizes conformance, includes functional correctness and is parameterized by an microarchitecture. We introduce action skipping refinement, a new type of refinement and we describe how our notions of refinement can be decomposed into properties that are more amenable to automated verification using the the concept of shared-resource commitment refinement maps. We do this in the context of formal, fully executable bit- and cycle-accurate models of an ISA and a microprocessor. Finally, we show how light-weight formal methods based on property-based testing can be used to identify transient execution bugs.

Related papers

• Easy Data Unlearning Bench [53.1304932656586]
  We introduce a unified and benchmarking suite that simplifies the evaluation of unlearning algorithms.<n>By standardizing setup and metrics, it enables reproducible, scalable, and fair comparison across unlearning methods.
  arXiv  Detail & Related papers  (2026-02-18T12:20:32Z)
• Monadic Context Engineering [59.95390010097654]
  This paper introduces Monadic Context Engineering (MCE) to provide a formal foundation for agent design.<n>We demonstrate how Monads enable robust composition, how Applicatives provide a principled structure for parallel execution, and crucially, how Monad Transformers allow for the systematic composition of these capabilities.<n>This layered approach enables developers to construct complex, resilient, and efficient AI agents from simple, independently verifiable components.
  arXiv  Detail & Related papers  (2025-12-27T01:52:06Z)
• Valida ISA Spec, version 1.0: A zk-Optimized Instruction Set Architecture [2.0790368408580138]
  The Valida instruction set architecture is designed for implementation in zkVMs to optimize for fast, efficient execution proving.<n>This specification intends to guide implementors of zkVMs and compiler toolchains for Valida.
  arXiv  Detail & Related papers  (2025-05-12T23:03:02Z)
• Computational Reasoning of Large Language Models [51.629694188014064]
  We introduce textbfTuring Machine Bench, a benchmark to assess the ability of Large Language Models (LLMs) to execute reasoning processes.<n> TMBench incorporates four key features: self-contained and knowledge-agnostic reasoning, a minimalistic multi-step structure, controllable difficulty, and a theoretical foundation based on Turing machine.
  arXiv  Detail & Related papers  (2025-04-29T13:52:47Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
  We present a new formalism that combines the ability of object-centric Petri nets to capture one-to-many relations and the one of Petri nets with identifiers to compare and synchronize objects based on their identity. We propose a conformance checking approach for such nets based on an encoding in satisfiability modulo theories (SMT)
  arXiv  Detail & Related papers  (2023-12-13T21:53:32Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  We propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core.
  arXiv  Detail & Related papers  (2023-08-15T13:19:17Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  In deductive verification and software model checking, dealing with certain specification language constructs can be problematic. We propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation.
  arXiv  Detail & Related papers  (2023-05-26T14:55:35Z)
• Task-Oriented Over-the-Air Computation for Multi-Device Edge AI [57.50247872182593]
  6G networks for supporting edge AI features task-oriented techniques that focus on effective and efficient execution of AI task. Task-oriented over-the-air computation (AirComp) scheme is proposed in this paper for multi-device split-inference system.
  arXiv  Detail & Related papers  (2022-11-02T16:35:14Z)
• Empowering parameter-efficient transfer learning by recognizing the kernel structure in self-attention [53.72897232951918]
  We propose adapters that utilize the kernel structure in self-attention to guide the assignment of tunable parameters. Our results show that our proposed adapters can attain or improve the strong performance of existing baselines.
  arXiv  Detail & Related papers  (2022-05-07T20:52:54Z)
• How Fine-Tuning Allows for Effective Meta-Learning [50.17896588738377]
  We present a theoretical framework for analyzing representations derived from a MAML-like algorithm. We provide risk bounds on the best predictor found by fine-tuning via gradient descent, demonstrating that the algorithm can provably leverage the shared structure. This separation result underscores the benefit of fine-tuning-based methods, such as MAML, over methods with "frozen representation" objectives in few-shot learning.
  arXiv  Detail & Related papers  (2021-05-05T17:56:00Z)
• Automatic Microprocessor Performance Bug Detection [3.6462412165522466]
  We present a two-stage, machine learning-based methodology that is able to detect the existence of performance bugs in microprocessors. Our best technique detects 91.5% of microprocessor core performance bugs whose average IPC impact is greater than 1%. When evaluated on memory system bugs, our technique achieves 100% detection with zero false positives.
  arXiv  Detail & Related papers  (2020-11-17T17:18:45Z)
• The Advantage of Conditional Meta-Learning for Biased Regularization and Fine-Tuning [50.21341246243422]
  Biased regularization and fine-tuning are two recent meta-learning approaches. We propose conditional meta-learning, inferring a conditioning function mapping task's side information into a meta- parameter vector. We then propose a convex meta-algorithm providing a comparable advantage also in practice.
  arXiv  Detail & Related papers  (2020-08-25T07:32:16Z)

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.