Secure Programming with Trusted Execution Environments

I

Aditya Oak, Musard Balliu, and Guido Salvaneschi

 

Abstract:

Confidential computing is a promising technology to protect code and data-in-use on untrusted host machines through using Trusted Execution Environments (TEE). A TEE is a hardware protected execution environment that allows performing confidential computations over sensitive data on untrusted hosts. However, despite its appealing concept, seamless integration of TEE programming into software applications in a way that is both accessible for developers and technically secure remains an open problem. There are mainly two challenges that hinder the adoption of TEEs in practice:
1. Existing TEE implementations don't support high-level managed languages such as Java or Scala, thus taking advantage of the current implementations is a complex and error-prone task.
2. Partitioning the application into components that run inside and outside a TEE may break application-level security policies, thus resulting in an overall insecure application.

In this work, we set out to study both these challenges. We present a programming model that seamlessly integrates a TEE, by abstracting away low-level programming details such as initialization and loading of data into the TEE. This programming model only requires developers to add annotations to their programs to enable the execution within the TEE. We leverage information flow control to secure applications running within TEEs against a passive and active attackers. We formalize a security type system for the core of our programming model and prove it sound with respect to this characterization of security.
We implement the programming model and the security type system to enable Java programs running on Intel SGX with strong security guarantees.