Secure Computing using Certified Software and Trusted Hardware

Building applications that ensure confidentiality of sensitive data is a non-trivial task. Such applications constantly face threats due to vulnerabilities in the application's code, or infrastructure attacks due to malicious datacenter insiders and exploits in the lower computing layers (i.e. OS, hypervisor, BIOS, firmware) that the application relies upon.This dissertation presents a novel approach for developing and verifying applications with provable confidentiality guarantees, even in the presence of such privileged adversaries. Our primary defense against infrastructure attacks is the use of trusted primitives such as Intel SGX enclaves, for isolating sensitive code and data within protected memory regions; enclaves are inaccessible to all other software running on the machine (i.e. OS, hypervisor, etc.), thus removing these large software layers from the trusted computing base (TCB). A central question addressed by this thesis is how the trusted hardware primitives can be used safely to build the trusted components of modern applications with provable guarantees. Prior experience suggests that even expert developers write unsafe programs that leak sensitive data due to programming errors and side channel attacks. To address this problem, this thesis makes contributions in formal threat models, modeling and specification of trusted platforms, and techniques to verify confidentiality properties of enclave programs.First, this thesis formalizes adversary models, an abstract, interface-level model of trusted platforms (including Intel SGX and MIT Sanctum), and formal semantics of enclave execution. This formal framework is required for reasoning about a program's behavior in the presence of a privileged adversary. Next, this thesis presents tools and techniques for certifying confidentiality (at the binary level), a property that we decompose into the following desiderata: 1) lack of explicit leak of secrets via enclave's outputs, 2) protection against certain side-channel leaks --- we only remove leaks via page-level memory access pattern, which is a new channel for privileged adversaries. For both desiderata, we develop verification tools and evaluate them on application's binaries including Map-Reduce programs from the Microsoft VC3 system, SPEC benchmarks, and several machine learning algorithms