Structural Operational Semantics for Functional and Security Verification of Pipelined Processors

Abstract The design of computer microarchitectures is a challenging task, involving a trade-off between efficiency and security. In the literature, two concerns which are affected by the details of the microarchitecture – formal assembly semantics, and vulnerability discovery and mitigation – are often addressed separately. In this paper we provide a structural operational semantics for pipelined microprocessors (Arm, x86, RISC-V) that is based on a regular understanding of microarchitectural features (pipelines, branch prediction, caches, privilege checks), conforms to established memory consistency models, and exposes the Spectre and Meltdown vulnerabilities. A key point is that the operational rules correspond to stages of the pipeline and are based almost entirely on syntactic aspects of fetched instructions, as is generally understood to be the case in real pipelines. We develop a model checker based closely on the semantics, which we use to experimentally validate the model and to provide the basis for security analyses.