Student project proposals by Jeremy Yallop (jeremy.yallop@cl.cam.ac.uk)

Programming language features for Trusted Execution Environments

This project investigates programming language features for confidential information, making use of Trusted Execution Environments (TEEs).

Many architectures currently support facilities for Confidential Computing (e.g. Arm TrustZone, Intel SGX and TDX, AMD SEV, Arm CCA). However, these solutions all restrict how applications are structured and deployed. In a typical system, only critical sub-components of a large application (e.g. a web-server) run in the TEE; most of the application runs in a traditional non-confidential mode. Unfortunately, with existing tools, dividing up the execution in this way is a challenging task.

Inspired by the literature on information-flow security (eg. fabric jif) and tierless web programming (eg. Eliom Links), this project investigates how to build programming-language features and compiler techniques, that make it possible to write applications that use confidential data in TEEs without requiring the programmer to think about all the details of the TEE infrastructure.

The solution space of this problem is very large. A simple approach might look at a functional or object-oriented language in which some functions, modules or classes are considered confidential. A more ambitious design might draw inspiration from distributed systems such as actor-oriented programming Erlang SGX and web tierless programming

(Joint proposal with Gustavo Petri, Arm Research)

An embedded DSL for cryptographic algorithms

Cryptographic algorithms (ciphers) are often written in assembly code rather than in high-level languages, for reasons of both efficiency and security. One security concern is the presence of timing attacks, in which an attacker can discover information about encrypted data by observing changes in the execution times of ciphers when the input is changed. When ciphers are written in high-level languages like C, the compiler may silently and inadvertently introduce these kinds of timing side channels into generated code.

Although writing ciphers in assembly code provides sufficient control to avoid these security problems, it makes implementation significantly more challenging. Ideally, ciphers would instead be written in a high-level language closer to the way they might be described by cryptographers.

This project involves building a domain-specific compiler from cipher descriptions to assembly language. There are four stages:

  1. embedding part of the Arm instruction set as a low-level domain-specific language
  2. building a second embedded domain-specific language for describing ciphers
  3. building a compiler from the cipher language to the Arm code embedding
  4. building some machine-checked proofs of functional correctness of the compiler (and perhaps showing that it eliminates a class of side-channel attacks)

Using a modern dependently-typed language like Agda or Idris, these four stages can be written as a single program.

(Joint proposal with Dominic Mulligan, Arm Research)

Background reading