Speculative execution attacks, such as the recent Spectre attacks, are a recent class of security threats that affect almost all modern processors (that is, millions of IT systems). These attacks exploit the hardware side-effects of a CPU optimization called speculative execution to break fundamental security assumptions on how programs are executed and to leak sensitive information.
Hardware/software co-design is an essential principle for building practical systems that are secure against these attacks. Following this principle, hardware and software should collaborate to thwart speculative execution attacks. Hardware platforms should provide precise security guarantees and expose control on the internal microarchitectural state. Software, instead, should leverage these guarantees to achieve end-to-end security. Unfortunately, we currently lack foundations, guiding principles, and tools for co-design for security.
This project will develop foundations, models, and tools for enabling co-design for secure speculation. The project will revolve around the notion of hardware/software security contract, an abstraction enabling the distribution of security obligations between hardware and software. The project will provide developers with languages for specifying security contracts as well as techniques for automatically determining whether proposals for secure speculation effectively prevent speculative execution attacks.