This course will explore the nascent field of secure compilation, which sits at the intersection between security and programming languages. The goal of a secure compiler is to compile source programs in a way that preserves source security properties (e.g., memory safety) in the target program produced by the compiler.
The course will present:
- the threat model that secure compilers consider, in order to understand what kind of attackers can a secure compiler defend against and what attack vectors are in scope for such attackers
- correctness criteria for secure compilation, in order to understand what kind of security properties can a secure compiler preserve and against which attacker
- specific instances of secure compilers, in order to familiarise oneself with the kind of modern mechanisms that can be used to build a secure compiler and the kind of security properties that a secure compiler can preserve. Examples of such mechanisms include access checks on pointer dereferencing (e.g. Intel MPX, Hardbound, WatchdogLite, Oracle SSM, SPARC ADI, or HWASAN), protected enclaves (e.g. Intel SGX, ARM TrustZone, Sanctum, or Sancus), capability machines (e.g. CHERI), or micro-policy machines (e.g. Draper PUMP, Dover CoreGuard). Examples of such security properties are: absence of speculation leaks (protection against Spectre), memory safety (both spatial and temporal).
- proof techniques for secure compilation, in order to understand how to provide formal guarantees that a compiler is indeed secure.
Evaluation: the evaluation is based on a small problem set of exercises (at the end of tue and wed classes) plus a paper presentation (likely on thu afternoon + fri morning)
