Rohit Sinha

GitHub rsinha

Codeplex rsinha



Research Interests

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.


  1. A Formal Foundation for Secure Remote Execution of Enclaves (CCS 2017 - Best Paper Award)

  2. A Compiler and Verifier for Page Access Oblivious Computation (FSE 2017)

  3. A Design and Verification Methodology for Secure Isolated Regions (PLDI 2016)
    [slides] [tool]

  4. Moat: Verifying Confidentiality Properties of Enclave Programs (CCS 2015)

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

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

  7. Symbolic Software Model Validation (MEMOCODE 2013)

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

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

  1. Parallel Simulation of Mixed-abstraction SystemC Models on GPUs and Multicore CPUs (ASPDAC 2012)

  2. Abstract State Machines as an Intermediate Representation for High-level Synthesis (DATE 2011)