I am a third year PhD student (accredited by ENS Paris) at Inria Paris-Rocquencourt under the direction of Karthikeyan Bhargavan in team Prosecco (Programming Securely with Cryptography). Our main research goal is to provide practical tools to analyze the security of sensitive web applications, especially those that use cryptographhy.
More details are available in my academic CV
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). (to appear) [Bib]
The BEAST wins again: Why TLS Keeps Failing to Protect HTTP
Briefing at Black Hat 2014. [Dedicated Website]
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]
F* language: F* is an ML-like language with a dependent type system for program verification. GitHub - Project page at Microsoft Research.
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.
I am a teaching assistant at École Poltechnique.
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.