Rohit Sinha

GitHub rsinha

Codeplex rsinha

Email rsinha@berkeley.edu

PGPhttps://keybase.io/rohitsinha

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 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.

Publications

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

  2. Moat: Verifying Confidentiality Properties of Enclave Programs (CCS 2015)
    [slides]

  3. Automatic Rootcausing for Program Equivalence Failures (CAV 2015)
    [slides]

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

  5. Symbolic Software Model Validation (MEMOCODE 2013)
    [slides]

  6. Verification with Small and Short Worlds (FMCAD 2012)
    [slides]

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)