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 trusted applications (e.g. secret provisioning protocols, secure chat) to run on Intel SGX platform. 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)