Dissertation Talk: Provably Secure Computing using Certified Software and Trusted Hardware
Presentation | May 1 | 11 a.m.-12 p.m. | 531 Cory Hall
Security-critical applications constantly face threats from exploits in lower computing layers
such as the OS and Hypervisor, or even attacks from malicious datacenter insiders.
In order to protect sensitive data from such privileged adversaries, there is increasing development of secure hardware primitives, such as Intel SGX, ARM TrustZone, and Sanctum RISC-V extensions.
This dissertation explores building cloud applications with provable security guarantees,
including only these hardware primitives (i.e. nearly zero software) in the trusted computing base.
In this talk, I will demonstrate compiler and verification techniques to develop applications that can be certified (at the level of machine code) to not leak secrets, both via their outputs and certain side channels.
Furthermore, I will show how formal models of the hardware platforms can be leveraged to port programs and their correctness proofs across different hardware platforms.