I currently run Symbolic Software, a Paris-based applied cryptography consulting office. As its director, I manage a small team that offers security audits, cryptographic protocol design and formal verification services. Therefore the main focus of my professional work currently is auditing cryptography and also developing Verifpal, an automated cryptographic protocol modeling, analysis and verification framework and a project that I am very passionate about.
Since its founding in 2018, Symbolic Software has completed and delivered over 200 software and cryptographic audits for clients all around the world.
In 2018, I defended my Ph.D. thesis, Formal Verification for Real-World Cryptographic Protocols and Implementations, at Inria Paris, after 3½ years of research with team PROSECCO.
In 2018 and 2019, I also designed and taught the computer security course at New York University's Paris campus, where I served as an adjunct professor.
Publications and Podcast
Publications aside, I also host Cryptography FM, a weekly podcast with news and a featured interview covering the latest developments in theoretical and applied cryptography. Whether it's a new innovative paper on lattice-based cryptography or a novel attack on a secure messaging protocol, we'll get the people behind it on Cryptography FM to talk about it.
- Verifpal: Cryptographic Protocol Analysis for the Real World (with G. Nicolas, M. Tiwari), 21st International Conference on Cryptology in India, 2020
- EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats (with A. Delignat-Lavaud, C. Fournet, T. Ramananandro, N. Swamy, T. Chahed), 28th USENIX Security Symposium, 2019
- Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols (with G. Nicolas, K. Bhargavan), 4th IEEE European Symposium on Security and Privacy, 2019
- Ledger Design Language: Designing and Deploying Formally Verified Public Ledgers (with N. Kulatova), Workshop on Security Protocol Implementations, 2018
- Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate (with K. Bhargavan, B. Blanchet), 38th IEEE Symposium on Security and Privacy, 2017
- Formal Modeling and Verification for Domain Validation and ACME (with K. Bhargavan, A. Delignat-Lavaud), Financial Cryptography and Data Security, 2017
- Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach (with K. Bhargavan, B. Blanchet), 2nd IEEE European Symposium on Security and Privacy, 2017
- Formal Verification of Smart Contracts (with K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, A. Rastogi, T. Sibut-Pinote, N. Swamy, S. Zanella-Beguelin), 11th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, 2016
- FlexTLS: A Tool for Testing TLS Implementations (with B. Beurdouche, A. Delignat-Lavaud, A. Pironti, K. Bhargavan), 9th USENIX Workshop on Offensive Technologies, 2015
- 2020-11-26: On the Apple Silicon M1 MacBook Pro
- 2020-09-07: Fear and Loathing in Protocol Analysis
- 2020-05-27: Why StopCOVID Fails as a Privacy-Preserving Design
- 2020-04-25: iPhone SE and the Commodification of the Pocket Computer
- 2020-04-17: An Investigation Into PEPP-PT
- 2020-03-29: Thoughts on 'Half-Life: Alyx' and G-Man
- 2019-04-11: Selfie's Reflections on Formal Verification for TLS 1.3: Largely Opaque
- 2018-10-26: Repairing a ThinkPad with a Corrupt Thunderbolt Firmware Chip
- 2015-11-25: On Encryption and Terrorists
Verifpal is new software for verifying the security of cryptographic protocols. Building upon contemporary research in symbolic formal verification, Verifpal’s main aim is to appeal more to real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. Verifpal is really cool!
Piccolo is an AI that plays the Japanese Othello strategy game at a strong and competitive level. Piccolo uses Negamax Depth-First-Search with Alpha-Beta pruning combined with heuristics to evaluate position strength, and features an elegant user interface. It is written in Go and compiled into WebAssembly.
Kyber-K2SO is a clean implementation of the Kyber IND-CCA2-secure key encapsulation mechanism (KEM), whose security is based on the hardness of solving the learning-with-errors (LWE) problem over module lattices. Kyber is one of the candidate algorithms submitted to the NIST post-quantum cryptography project.
Noise Explorer is an online engine for designing, reasoning about, formally verifying and implementing arbitrary Noise Handshake Patterns. Based on our formal treatment of the Noise Protocol Framework, Noise Explorer can validate any Noise Handshake Pattern and then translate it into a model ready for automated verification and also into a production-ready software implementation written in Go or in Rust.
FormatForest is a simple and elegant blogging engine written in Go. It was originally developed as a personal project to run my own blog, but has now been rendered open source. Simplicity and elegance in the FormatForest design and functionality allow you to focus on growing your writing and personal web presence. Complete Markdown support allows you to draft posts quickly and without fuss. Secure sync over rsync allows you to publish your website quickly from your local machine.
DiskGem is software for secure file transfer over SFTP. DiskGem currently offers an easy to use, stable command-line user interface that supports parallel file transfers and other useful features. DiskGem will soon also support creating encrypted archives on the server which offer encryption of stored files as well as metadata obfuscation.