Tej Chajed

tchajed@mit.edu

Hello! I'm Tej Chajed, a fifth-year PhD student in PDOS at MIT CSAIL, advised by Frans Kaashoek and Nickolai Zeldovich. I work on formal verification of systems software — I implement systems and prove they do what they're supposed to.

Before coming to MIT I was at UIUC, where I got undergraduate degrees in Electrical Engineering and Computer Science.

Research

Even critical systems software has bugs — for example, file systems have bugs that occasionally lead to users losing data. My research aims to write systems software that always does what it's supposed to. We've written several verified systems, where we wrote a specification of what the system should do, then used the Coq proof assistant to prove that the implementation meets the specification. So far my work has centered around a theme of storage systems, including a verified file system (FSCQ) and a framework that combines concurrency and crash-safety reasoning.

I do a lot of work on Coq-related things, including maintaining a list of Coq tricks for the advanced user.

Publications

Verifying concurrent, crash-safe systems with Perennial   (SOSP 2019)

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich

EverParse: Verified Secure Zero-Copy Parsers for
Authenticated Message Formats   (USENIX Security 2019)

Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko

Argosy: Verifying Layered Storage Systems with Recovery Refinement   (PLDI 2019)

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich

Verifying concurrent software using movers in CSPEC   (OSDI 2018)

Tej Chajed, M. Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich

Proving confidentiality in a file system using DiskSec   (OSDI 2018)

Atalay İleri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Verifying a high-performance crash-safe file system
using a tree specification   (SOSP 2017)

Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Extending a verified file system with concurrency   (SOSP 2017 SRC)

Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Certifying a file system using Crash Hoare Logic:
Correctness in the presence of crashes   (CACM 2017)

Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, and Daniel Ziegler

Using Crash Hoare Logic for certifying the FSCQ file system   (SOSP 2015)

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Amber: Decoupling user data from web applications   (HotOS 2015)

Tej Chajed, Jon Gjengset, Jelle van den Hooff, M. Frans Kaashoek, James Mickens, Robert Morris, and Nickolai Zeldovich

How to pronounce my name