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.CCS Concepts• Hardware → Theorem proving and SAT solving; Semi-formal verification; • Security and privacy → Logic and verification; Side-channel analysis and countermeasures.
This paper discusses the correctness of microprocessors in the face of transient execution attacks like Meltdown and Spectre, advocating for formal specifications using refinement theory. It introduces global correctness notions that formalize functional correctness and conformance to Instruction Set Architecture (ISA), proposing action skipping refinement as a novel refinement type. This enables automated verification of aspects influenced by factors such as pipeline optimizations and speculative execution. The authors detail two distinct correctness notions for Meltdown and Spectre, featuring tools for modeling and verifying compliance with these notions using the ACL2 theorem prover. The research aims to establish a feasible hardware-software interface that fosters the design of performant microprocessors while addressing security vulnerabilities.
This paper employs the following methods:
- formal specifications
- refinement theory
- witness refinement
- action skipping refinement
The following datasets were used in this research:
- Establishment of global notions of correctness for addressing transient execution attacks.
- Introduction of action skipping refinement and share-resource commitment refinement maps for verification.
- Implementation of formal models of ISA and microprocessors using the ACL2 theorem prover.
The authors identified the following limitations:
- The research requires consensus on observer models and abstractions needed for modern processors, which may impede broader acceptance.
- Significant effort is necessary to formalize the models and achieve acceptance of the specifications proposed.
- Number of GPUs: None specified
- GPU Type: None specified
- Compute Requirements: None specified