Research and Publications
LMTest ·
Tool to simulate experimental speculation and leakage models on real code
Testing Side-Channel Security of Cryptographic Implementations against Future Microarchitectures [ arXiv ]
Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin,
Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom
CCS '24 (Distinguished Paper!!)
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
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
USENIX '21
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 (Made it to the front page of Hacker News on 2022-10-23!)
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