ERC Starting Grant · 2021
Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
The Instruction Set Architecture (ISA) is the interface that processor hardware offers to software developers. Current ISAs do not explicitly specify the security properties guaranteed by that interface, so that, for example, recent severe micro-architectural side-channel vulnerabilities like Spectre did not even violate the specifications. This project proposes a fundamentally new approach to specify ISA security properties by using what we call universal contracts. These are formal contracts in a compositional program logic that automatically hold for arbitrary code. Such contracts capture ISA-enforced upper bounds on the effects of arbitrary (even attacker-controlled) software. While…
From the public funding record at EU CORDIS. Describes the funded project, not the reviews below.