PI: Vashti Galpin, Co-I: David Aspinall, University of Edinburgh

  • Transient execution vulnerabilities (such as Spectre) take place at micro-architecture level in out-of-order processors with speculation.
  • Attacks leveraging these vulnerabilities can undermine the security of all system components built on top of a susceptible micro-architecture.
  • Mitigations for these vulnerabilities can be expensive in terms of loss of computing cycles due to a reduction in speculation.
  • Formal modelling of micro-architecture behaviour together with performance analysis is needed.
  • We present a cycle-level model of a generic out-of-order processor with speculation in CARMA, a quantitative modelling language with Markov chain semantics.

We have developed a CARMA model of micro-architecture that includes pipeline details and hardware speculation. We have developed a very generic ISA (instruction set architecture) that consists of instructions that are similar to those found in RISC processors (such as ARM) and to the micro-ops that are obtained from the ISA in x86 systems. This enables us to work with essentially a RISC ISA and to abstract from the more complex ISA of x86. This model takes as input an abstract stream of instructions which indicates the dependence of an instruction on the results of previous instructions.

This allows for input to be created from profiles of actual code rather than working with the code directly, and supports abstraction of program characteristics hence allowing for performance analysis over a family of programs rather than specific executions.

To ensure that attacks and mitigations can be modelled, the ROB (reorder buffer) is an explicit component of the model. This gives sufficient micro-architectural details that Spectre can be modelled as well as mitigations based on memory fences and timing experiments can be conducted to understand performance. The model serves as a proof-of-concept for the proposed approach.

PUBLICATIONS. The model developed and the software tool to experiment with it can be found on this link.

RELATED GRANTS. V Nagarajan, S Ainsworth, TC Grosser, D Aspinall, EPSRC Grant EP/V038699/1, Dijkstra’s Pipe: Timing-Secure Processors by Design, £535,239.

IMPACT. “One class of vulnerabilities that we hope the Morello board will mitigate against is side-channel attacks, whilst minimising any impact on performance. In order for this to be fully assessed, we need to be able to reason about and model both security properties and performance at the micro-architecture level. The simulator that this proposal hopes to develop will be a valuable asset in this regard. We also welcome the longer term aim of developing a compositional approach to micro-architecture security, as deriving the properties of a full system from individual components will become increasingly important as systems and interconnects get increasingly complex.” – Matt Rivers-Latham, Senior Director of Operations, Arm Ltd. –