Trusted execution for private and secure computation: a composable approach

Abstract

Trusted Execution Environments (TEEs) protect and isolate programs, sometimes referred to as enclaves, from all other software executed on the same processor, through a combination of specialised hardware, microarchitectural design, and cryptography. They are used both to underpin the security of computing infrastructure that processes sensitive data, and as a component in the design of efficient privacy-preserving protocols. The adoption of this technology is driven by a desire to shift trust from the operator of computing equipment to its manufacturer. A core feature of the architecture is remote attestation, allowing a remote party to verify that a TEE is running a certain program. While initial industrial deployments often used this to prevent sensitive data from leaking to untrusted clients, e.g. for media content protection, there is a growing interest in using TEEs to ensure that programs deployed on a cloud server will not run any unauthorised or outright mailcious computation on sensitive data provided by users.

TEEs are still a relatively novel technology, with security implications that are still not fully understood, and whose implementation has been shown to be vulnerable to many attacks. It is paramount to carefully analyse the guarantees offered by TEEs when used as a primitive in the construction of application protocols, and how multiple protocols relying on TEEs might interact with each other when composed. We approach this task using the tools of the cryptographic literature. In particular, we use the \emph{universal composability (UC)} framework to examine a high-level formalisation of TEEs that supports composition without delving into the specific of implementation or different architectural choices.

To demonstrate the scope of the task, we follow the construction of a cryptographic protocol through several stages. We first extend and reformalise IRON (Fisch et al, CCS17), a protocol that provides secure computation in a cloud setting by implementing the functional encryption primitive. Our extension, called Steel, broadens the class of allowable functions a cloud server can compute, and we prove the security of our protocol in UC, by using the formalisation of TEEs provided by Pass et al (EUROCRYPT17).

We then question the cryptographic assumption of this formalism, showing that it doesn't adequately capture existing attacks which would make Steel insecure, such as state continuity attacks. We address this vulnerability by providing a modular trusted execution abstraction that can adequately capture TEE implementations with different functional and adversarial guarantees, and provides a more flexible attestation mechanism. Our new formalism aims to capture existing work in the literature and rescue previous proofs into a more realistic setting, closer to real-world implementations.

Finally, we show how the Steel protocol can be used as a composable building block to provide a privacy preserving contact tracing service that bridges the privacy properties of decentralised contact tracing with the ability to conduct data analytics enabled by centralised contact tracing. We construct and prove the protocol in a modular manner, showcasing the power of universal composability.