Dijkstra's Pipe: Timing-Secure Processors by Design

点击翻译按钮获取中文摘要

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.