Repository logo

Architectural Contracts for Safe Speculation

Accepted version


Conference Object

Change log


Woodruff, Jonathan 
van der Maas, Marno 
Rugg, Peter 
Joannou, Alexandre 


We propose architectural contracts that specify the allowable limits of speculative execution to enable both software safety guarantees and hardware verification. Transient-execution attacks have presented a major threat in recent years, driving deployment of software mitigations and research into hardware solutions. Recent work on hardware/software contracts for secure speculation recognizes the need for cooperation between hardware guarantees and software analysis, and demonstrates that speculative execution models can enable formal analysis of programs with respect to transient-execution vulnerabilities. Therefore, we have extended these limited models into comprehensive architecture-level contracts that can be verified at a microarchitecture level. We define a set of speculation contracts for translation (TSC) and branching (BSC), and for memory ordering (MOSC). We also develop a set of directed-random test routines that reproduce all known contract violations in a prototype out-of-order processor, most of which represent known transient-execution vulnerabilities. We also extend the RiscyOO processor to enforce each contract and evaluate performance, demonstrating the practicality of the chosen contracts with an overhead between -1.2% and +1.8% for this prototype. These general-purpose contracts set the stage for specification of speculative execution for complete instruction-set architectures, and particularly for new security-focused ISA extensions.



33 Built Environment and Design, 46 Information and Computing Sciences, 4604 Cybersecurity and Privacy, 3301 Architecture, 4612 Software Engineering

Journal Title

2023 IEEE 41st International Conference on Computer Design (ICCD)

Conference Name

41st IEEE International Conference on Computer Design

Journal ISSN


Volume Title


EPSRC (via Queen's University Of Belfast) (R1098ECI)
This project was supported by the NCSC under the UK RISE Initiative. This work was supported in part by the Engineering and Physical Sciences Research Council EP/S030867/1. Distribution Statement A: Approved for public release; distribution is unlimited. This work was supported in part by the Defense Advanced Research Projects Agency (DARPA) under contract HR0011-18-C-0016 (“ECATS”).