Global Microprocessor Correctness in the Presence of Transient Execution

TL;DR

This paper proposes a formal, refinement-based approach to define microprocessor correctness that accounts for transient execution attacks like Meltdown and Spectre, enabling more robust verification of processor security and functionality.

Contribution

It introduces a global correctness notion using refinement theory, including action skipping refinement, and demonstrates how to verify microprocessor models against transient execution vulnerabilities.

Findings

Formal correctness specifications can encompass transient execution attacks.

Action skipping refinement enables automated verification of microprocessor correctness.

Light-weight property-based testing can identify transient execution bugs.

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.