I am a researcher in the Confidential Computing group at Microsoft Research Cambridge. I completed my PhD at Inria Paris-Rocquencourt under the direction of Karthikeyan Bhargavan in team Prosecco (Programming Securely with Cryptography).
More details are available in my academic CV
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer
(with C. Fournet, B. Parno, J. Protzenko, T. Ramananandro, J. Bosamiya, J. Lallemand, I. Rakotonirina, Y. Zhou)
In proceedings of the 41st IEEE Symposium on Security and Privacy, 2021.
[PDF]
[Bib]
[Github]
Toward confidential cloud computing (Position Paper)
(with M. Russinovich, M. Costa, C. Fournet, D. Chisnall, S. Clebsch, K. Vaswani, V. Bhatia)
In Communications of the ACM, 2021
[PDF]
[Bib]
EverCrypt: A fast, verified, cross-platform cryptographic provider
(with J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, C. Fournet, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. Wintersteiger, S. Zanella-Beguelin)
In proceedings of the 40th IEEE Symposium on Security and Privacy, 2020.
[PDF]
[Bib]
[Github]
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
(with T. Ramananandro, C. Fournet, N. Swamy, T. Chajed, N. Kobeissi, J. Protzenko)
In proceedings of the 26th USENIX Security Symposium, 2019.
[PDF]
[Bib]
[Github]
State Separation for Code-Based Game-Playing Proofs
(with C. Brzuska, C. Fournet, K. Kohbrok, M. Kohlweiss)
In proceedings of Advances in Cryptology (ASIACRYPT'18), 2018.
[PDF]
[Bib]
[Slides]
A Formal Treatment of Accountable Proxying over TLS
(with K. Bhargavan, I. Boureanu, P.-A. Fouque, C. Onete)
In proceedings of the 38th IEEE Symposium on Security and Privacy (Oakland'18).
[PDF]
[Bib]
Implementing and Proving the TLS 1.3 Record Layer
(with K. Bhargavan, C. Fournet, M. Kohlweiss, J. Pan, J. Protzenko, A. Rastogi, N. Swamy, S. Zanella-Béguelin, J.-K. Zinzindohoué)
In proceedings of the 37th IEEE Symposium on Security and Privacy (Oakland'17).
[PDF]
[Bib]
Verified Low-Level Programming Embedded in F*
(with J. Protzenko, J.-K. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Béguelin, C. Hriţcu, K. Bhargavan, C. Fournet, N. Swamy)
In Proceedings of the ACM on Programming Languages (ICFP'17).
[PDF]
[Bib]
A Formal Model for ACME: Analyzing Domain Validation over Insecure Channels
(with K. Bhargavan, N. Kobeissi).
In proceedings of the 21st International Conference on Financial Cryptography and Data Security (FC'17).
[PDF]
[Bib]
Formal verification of smart contracts: Short paper
(with K. Bhargavan, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, S. Zanella-Béguelin).
In proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS'16).
[PDF]
[Bib]
Cinderella: Turning Shabby X.509 Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation
(with C. Fournet, M. Kohlweiss, B. Parno),
In proceedings of the 37th IEEE Symposium on Security and Privacy (Oakland'16).
[PDF]
[Bib]
Dependent Types and Multi-Monadic Effects in F*
(with N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoue, S. Zanella-Béguelin).
In 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16).
[PDF]
[Bib]
A Messy State of the Union: Taming the Composite State Machines of TLS
(with B. Beurdouche, K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P.-Y. Strub, J. K. Zinzindohoue),
In proceedings of the 36th IEEE Symposium on Security and Privacy (Oakland'15).
Distinguished Paper Award.
[PDF]
[Slides]
[Bib]
SMACK: State Machine AttaCKs
Website dedicated to the attacks from the paper, including FREAK.
FlexTLS: A Tool for Testing TLS Implementations
(with K. Bhargavan, B. Beurdouche, N. Kobeissi, A. Pironti).
9th USENIX Workshop on Offensive Technologies (WOOT'15).
Best paper award.
Network-based Origin Confusion Attacks against HTTPS Virtual Hosting
(with K. Bhargavan),
In proceedings of the 24th International Conference on World Wide Web (WWW'15).
[PDF]
[Slides]
[Bib]
Verified Contributive Channel Bindings for Compound Authentication
(with K. Bhargavan and A. Pironti),
In proceedings of the 22nd Annual Network and Distributed System Security Symposium (NDSS'15).
[PDF]
[Slides]
[Bib]
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS
(with K. Bhargavan, C. Fournet, A. Pironti and P. Strub),
In proceedings of the 35th IEEE Symposium on Security and Privacy (Oakland'14).
[PDF]
[Slides]
[Bib]
[Supporting Website]
Discovering Concrete Attacks on Website Authorization by Formal Analysis
(with C. Bansal, K. Bhargavan and S. Maffeis),
In Journal of Computer Security, special issue on Web Application Security - Web @ 25, IOS Press, 2014.
[Editor Website]
[Bib]
Web PKI: Closing the Gap between Guidelines and Practices
(with M. Abadi, A. Birrell, I. Mironov, T. Wobber and Y. Xie),
In proceedings of the 21st Annual Network and Distributed System Security Symposium (NDSS'14).
[PDF]
[Slides]
[Bib]
[Totient Project at MSR]
Language-Based Defenses Against Untrusted Browser Origins
(with K. Bhargavan and S. Maffeis),
In proceedings of the 22th USENIX Security Symposium, 2013.
[PDF]
[Slides]
[Bib]
[Presentation]
[Supporting Website]
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage
(with C. Bansal, K. Bhargavan and S. Maffeis),
In 2nd Conference on Principles of Security and Trust (POST'13)
(David Basin, John Mitchell, eds.), Springer Verlag, 2013.
[PDF]
[Slides]
[Bib]
Web-based Attacks on Host-Proof Encrypted Storage
(with K. Bhargavan),
In 6th USENIX Workshop on Offensive Technologies (WOOT'12), 2012.
[PDF]
[Slides]
[Bib]
On the security of Authentication Protocols for the Web
(supervised by Karthikeyan Bhargavan)
Defended on March 14, 2016 at Inria Paris.
[PDF]
F* language: F* is an ML-like language with a dependent type system for program verification.
[Dedicated website]
[Github]
[Project page at Microsoft Research]
miTLS and Hacl*: Verified implementation of TLS 1.3 and its cryptographic algorithms in F*.
[Dedicated website]
[Github]
DJS and DJCL: defensive (totally memory isolated) JavaScript, and the defensive JavaScript crypto library.
[Dedicated website]
[Github]
My research sometimes leads to the discovery of browser bugs. I found multiple attacks against Chrome, Firefox and Safari; most of which are listed on my OSVDB profile.
Security Types for Web Applications, master thesis, under the supervision of Karthikeyan Bhargavan, August 2012. [PDF] [Slides]
An automaton model for forest algebras, internship report, under the supervision of Howard Straubing, August 2010. [PDF] [BibTeX entry] [Extended abstract] [Slides]
Partial commutation closures of recognizable languages, internship report, under the supervision of Anca Muscholl and Marc Zeitoun, July 2009. [PDF] [BibTeX entry] [Slides]
An introduction to dependent types, a presentation given for the categories and lambda-calculus course, 2009. [Slides]
Collisions in MD5, a presentation given for an english course, 2009. [Slides]
(in french) Algèbres tropicales et plus court chemin, rapport de TIPE publié dans Quadrature n°72, pp. 22-28, avril 2009. [Version TIPE, PDF] [Errata] [BibTeX] [Version journal]
(in french) Une introduction aux automates cellulaires, 2009. [PDF]
(in french) Précis et formulaire de physique pour la prépa MP, 2008. [PDF]