Secure-by-Construction Applications using Trusted Execution Environments

Abstract

Language-based security mechanisms—such as sophisticated type systems for information- flow control—are used to express and enforce security requirements at the application-level. However, the security guarantees break down in the presence of powerful low-level attackers that are not bound by the language-level abstractions, for example, attackers that are capable of injecting arbitrary code to extract secrets. Trusted Execution Environments (TEEs)—such as Intel SGX, ARM TrustZone and Sanctum— offer strong architectural protection mechanisms and thus have the potential to provide strong security guarantees even in the presence of malicious privileged software, including OS kernels. Moreover, TEEs can provide remote attestation: attesting to the execution of known code on an untrusted host. However, TEEs aren’t a panacea. They do nothing to ensure that code executing inside the TEE is trustworthy. This dissertation shows how to complement the strengths of language-based security mechanisms with TEEs, in a principled way, to build applications that are secure-by-construction. First, it presents IMPe, a C-like language with support for TEEs. IMPe statically enforces confidentiality against a spectrum of attackers of varying strengths. Second, it presents DFLATE, an ML-like functional language with support for TEEs in a distributed setting, and enforces both confidentiality and integrity against multiple threat models. Third, it proposes the idea that TEEs can be viewed as computation principals—principals representing computations—and explores the expressiveness of access control policies using computation principals.