I work on language-based security. Broadly, my research seeks to specify and build provably secure systems using hardware assisted security mechanisms and formal techniques. During my Ph.D, I worked on principles and techniques for enforcing strong security guarantees against powerful attackers using Trusted Execution Environments such as Intel SGX and ARM TrustZone.