Vincent Laporte

Recent communications

  • “Fine-Grained Constant-Time Policies with Jasmin & EasyCrypt.” Le génie logiciel au service de la sécurité des systèmes, logiciels et réseaux, CNAM, Paris, November 24, 2022. https://glsec22.sciencesconf.org/. pdf.

  • “High-Assurance Cryptography in Jasmin & Spectre Security.” Team Cambium, Inria, Paris, September 26, 2022. https://cambium.inria.fr/seminaires/annonces/20220926.Vincent.Laporte.txt. pdf.

  • Barthe, Gilles, Benjamin Grégoire, Vincent Laporte, and Swarn Priya “Structured Leakage and Applications to Cryptographic Constant-Time and Cost.” In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, (CCS), 2021. pdf.

  • “Jasmin: A Certified Workbench for High-Assurance and High-Speed Cryptography.” The Coq Workshop 2021 (online), July 2, 2021. https://coq-workshop.gitlab.io/2021/. slides.

  • “Modèle de Fuite Structurée & Applications à La Compilation Sécurisée.” Journées AFADL 2021 (online), June 16, 2021. https://www.lirmm.fr/afadl2021/?page=programme. eprint; slides.

  • 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

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.

  • 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.

  • Shivakumar, Basavesh Ammanaghatta, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, and Lucas Tabary-Maujean “Typing High-Speed Cryptography Against Spectre v1.” Cryptology ePrint Archive, Paper 2022/1270, 2022. https://eprint.iacr.org/2022/1270.

  • Shivakumar, Basavesh Ammanaghatta, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya “Enforcing Fine-Grained Constant-Time Policies.” In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, (CCS), 2022. doi:10.1145/3548606.3560689.

Lectures

Verasco

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.

PinocchioQ

This is thee first certified, semantics-preserving compiler for verifiable computing. Based on CompCert and developed in Coq, this compiler targets an architecture whose instructions consist solely of quadratic equations over a large finite field, amenable to succinct verification using the Pinocchio cryptographic scheme.

Downloads

Relevant publication

  • Fournet, Cédric, Chantal Keller, and Vincent Laporte “A Certified Compiler for Verifiable Computing.” In 29th IEEE Computer Security Foundations Symposium, (CSF), 268–80, 2016. doi:10.1109/CSF.2016.26. pdf slides