“Secure Compilation of Counter-Measures to Spectre Attacks.” Team Prosecco, Inria, Paris, November 7, 2024. pdf.
“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.
Jasmin is a programming language to write high-assurance, high-speed cryptographic implementations.
Its compiler is correct — formally verified in Coq.
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.
Verasco is a formally-verified static analyzer for C.
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.
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.