|
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.
|