Repository logo
 

Architectural Contracts for Safe Speculation

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

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

Abstract

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.

Description

Keywords

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

1063-6404
2576-6996

Volume Title

Publisher

IEEE
Sponsorship
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”).