I recently joined the Programming Principles and Tools (PPT) group as a researcher at Microsoft Research Cambridge, after completing 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
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] [Slides] [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).
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]
[Dedicated website] [Github]
forestalg (current version: 1.11), a GAP package to handle forest automata, forest algebras and monadic second order logic on forests. Joint work with Howard Straubing. Dedicated page
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]
Some photos I took during my numerous travels.