Rohit Sinha

GitHub rsinha

Codeplex rsinha


Research Interests

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:

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

  2. Automatic Rootcausing for Program Equivalence Failures (CAV 2015)

  3. Formal Modeling and Verification of CloudProxy (VSTTE 2014)

  4. Symbolic Software Model Validation (MEMOCODE 2013)

  5. Verification with Small and Short Worlds (FMCAD 2012)