Vincent Laporte

Recent communications

  • Almeida, José Bacelar, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub “The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.” In 41st Ieee Symposium on Security and Privacy, (S&P), 2020.

  • Barthe, Gilles, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu “Formal Verification of a Constant-Time Preserving C Compiler.” Proceedings of the ACM on Programming Languages (POPL), 2020.

  • Barthe, Gilles, Benjamin Grégoire, and Vincent Laporte “Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic ‘Constant-Time’.” In 31st IEEE Computer Security Foundations Symposium, (CSF), 2018. pdf slides

Research projects


Jasmin is a programming language to write high-assurance, high-speed cryptographic implementations.

Its compiler is correct — formally verified in Coq.

Relevant publications

  • Almeida, José Bacelar, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub “Jasmin: High-Assurance and High-Speed Cryptography.” In Proceedings of the 24th ACM Conference on Computer and Communications Security, (CCS), 2017. pdf from HAL slides

  • Almeida, José Bacelar, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub “Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of Sha-3.” In Proceedings of the 2019 Acm Sigsac Conference on Computer and Communications Security, (CCS), 2019.


Verasco is a formally-verified static analyzer for C.

Relevant publications

  • Blazy, Sandrine, Vincent Laporte, and David Pichardie “An Abstract Memory Functor for Verified C Static Analyzers.” In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, (ICFP), 325–37, 2016.

  • Jourdan, Jacques-Henri, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie “A Formally-Verified C Static Analyzer.” In Proc. Of the 42th Symp. On Princ. Of Prog. Languages (POPL). ACM, 2015.

  • Blazy, Sandrine, Vincent Laporte, André Maroneze, and David Pichardie “Formal Verification of a C Value Analysis Based on Abstract Interpretation.” In Proc. Of the 20th Static Analysis Symposium (SAS). Lecture Notes in Computer Science. Springer-Verlag, 2013.