Details of Grant 

EPSRC Reference:	EP/V038699/1
Title:	Dijkstra's Pipe: Timing-Secure Processors by Design
Principal Investigator:	Nagarajan, Dr V
Other Investigators:	Grosser, Dr TC Aspinall, Professor D Ainsworth, Dr S
Researcher Co-Investigators:
Project Partners:	ARM Ltd Stanford University
Department:	Sch of Informatics
Organisation:	University of Edinburgh
Scheme:	Standard Research
Starts:	01 July 2021	Ends:	30 June 2024	Value (£):	535,239
EPSRC Research Topic Classifications:	Computer Sys. & Architecture Fundamentals of Computing
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:	Panel Date Panel Name Outcome 10 Feb 2021 Cross-RI PaCCS 2020 prioritisation panel Announced
Summary on Grant Application Form
Society relies on microprocessors, from mobile phones to datacentres. The microprocessor industry, however, is facing a security crisis. The recently discovered speculation-based timing-channel vulnerabilities, such as Spectre, allows for a malicious actor running code on a system -- e.g., JavaScript adverts within a browser -- to potentially steal secrets and break down barriers. The culprit in this case is sophisticated hardware speculation techniques, which allow for instructions (such as those conditionally dependent on branches) to be tentatively executed even before it is known whether they can execute. Such techniques have been the bread-and-butter of high-performance processors, and it is unlikely that companies can afford to do away with them. How does one design a microprocessor that provably guarantees security against such timing-channel vulnerabilities without compromising performance? In this project, we propose a new way of designing processors that are guaranteed to be timing-secure by design. Our approach is based on a new foundational specification, called a timing influence model that specifies how speculative instructions are allowed to impact other instructions. We will build on this foundation by investigating a methodology and a tool flow wherein the designer expresses their microarchitectural design while our tool automatically verifies the said design against the timing influence model, and estimates its performance via cycle-accurate simulation. If successful, our secure-by-construction methodology will not only help address the security crisis faced by today's processors, it also has the potential to reduce costs by reforming processor design entirely.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.ed.ac.uk