Sunjay Cauligi


Email: first-name DOT last-name AT mpi DASH sp DOT org

Max Planck Institute for Security and Privacy (MPI-SP)
Universitätsstraße 140
44799 Bochum, Germany

About Me

I am currently a postdoc at the Max Planck Institute for Security and Privacy working with Gilles Barthe, but previously I was a PhD at UC San Diego working with Deian Stefan. My interests include semantics, type theory, and language design for creating secure systems.

I completed my undergraduate degrees in Computer Engineering and Mathematics at the University of Washington.

Research and Publications

Spectre Declassified + SelSLH · Attack abusing speculative declassification + a much more efficient form of SLH
Spectre Declassified: Reading from the Right Place at the Wrong Time   [ ePrint ]
Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi,
Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O’Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom
Oakland '23 (to appear)

Spectre semantics · there are so many papers even just in this subarea
SoK: Practical Foundations for Software Spectre Defenses   [ paper | bibtex | arXiv | presentation · (video abstract) ]
Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan
Oakland '22

Swivel formalization · (short paper)
A Turning Point for Verified Spectre Sandboxing   [ arXiv ]
Sunjay Cauligi, Marco Guarnieri, Daniel Moghimi, Deian Stefan, Marco Vassena
TECHCON '21 (Top 10 Presenter)

Swivel · Spectre protections for in-process sandbox systems
Swivel: Hardening WebAssembly against Spectre   [ paper | bibtex | arXiv ]
Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang,
Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, Deian Stefan

Spectre/Jasmin · Bringing speculation awareness to a formally verified assembly language
High-Assurance Cryptography in the Spectre Era   [ ePrint | bibtex ]
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao,
Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
Oakland '21

Blade · Algorithm + static analysis tool to efficiently insert Spectre mitigations
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade   [ paper | bibtex | arXiv ]
Marco Vassena, Craig Disselkoen, Klaus v. Gleissenthall, Sunjay Cauligi,
Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, Deian Stefan
POPL '21 (Distinguished Paper — congrats Marco!)

Pitchfork · Formal framework + symbolic analysis tool for Spectre
Constant-Time Foundations for the New Spectre Era   [ paper | bibtex | arXiv | presentation · (video abstract) | github ]
Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe
PLDI '20 (Selected for Best Video!)

FaCT · Language for constant-time crypto
FaCT: A DSL for Timing-Sensitive Computation   [ paper | bibtex | presentation · (video abstract) | slides | github ]
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner,
Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
PLDI '19

CT-Wasm · Constant-time web assembly
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem   [ paper | bibtex ]
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, Deian Stefan
POPL '19

CT-Wasm · (extended abstract)
Constant-Time WebAssembly   [ paper | bibtex ]
John Renner, Sunjay Cauligi, Deian Stefan
PriSC '18

FaCT · (short paper)
FaCT: A Flexible, Constant-Time Programming Language   [ paper | bibtex | slides · (original) | github ]
Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan
IEEE SecDev '17