I work on applying mathematical proof techniques to reason about software security. My research focuses on proving that a security-critical program demonstrates end-to-end security by modeling programs in a formal system (e.g. first-order logic) and using formal analysis (e.g. theorem proving, type checking) to prove an absence of errors. Specifically, I am using these techniques to build provably correct security-critical applications to run on trusted hardware such as Intel SGX. I am being advised by Prof. Sanjit Seshia at UC Berkeley, where I am currently pursuing my PhD in Electrical Engineering and Computer Science.

In reverse chronological order:

Verification of Confidentiality Properties of Enclave Programs (EECS-TR 2015)

Automatic Rootcausing for Program Equivalence Failures (CAV 2015)

Formal Modeling and Verification of CloudProxy (VSTTE 2014)

Symbolic Software Model Validation (MEMOCODE 2013)

Verification with Small and Short Worlds (FMCAD 2012)

My undergraduate research in design automation resulted in the following publications: