I build provably-secure cloud services using trusted hardware primitives, such as Intel SGX instructions. Specifically, I work on a combination of static program analyzers, languages, and compilers to guarantee that security-critical programs satisfy important properties (e.g. confidentiality: sensitive data is never leaked in the clear), even in the presence of powerful adversaries that can compromise large parts of your computing stack, such as the OS and Hypervisor layers. I am being advised by Prof. Sanjit Seshia at UC Berkeley, where I am currently pursuing my PhD in Electrical Engineering and Computer Science.
A Formal Foundation for Secure Remote Execution of Enclaves (CCS 2017 - Best Paper Award)
Formal Modeling and Verification of CloudProxy (VSTTE 2014)
My undergraduate research in design automation resulted in the following publications: