Vincent Laporte

According to our database, Vincent Laporte authored at least 28 papers between 2010 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

High-assurance zeroization.

Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe

IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024

Protecting cryptographic code against Spectre-RSB.

Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang

IACR Cryptol. ePrint Arch., 2024

Preservation of Speculative Constant-time by Compilation.

Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte

IACR Cryptol. ePrint Arch., 2024

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.

José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2024

2023

Formally verifying Kyber Episode IV: Implementation correctness.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub

IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023

Formally verifying Kyber Part I: Implementation Correctness.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2023

2022

Enforcing fine-grained constant-time policies.

Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya

IACR Cryptol. ePrint Arch., 2022

Typing High-Speed Cryptography against Spectre v1.

Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean

IACR Cryptol. ePrint Arch., 2022

2021

Structured Leakage and Applications to Cryptographic Constant-Time and Cost.

Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya

IACR Cryptol. ePrint Arch., 2021

2020

Formal verification of a constant-time preserving C compiler.

Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu

Proc. ACM Program. Lang., 2020

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira

Proceedings of the Progress in Cryptology - INDOCRYPT 2020, 2020

2019

Machine-Checked Proofs for Cryptographic Standards.

José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.

José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time".

Gilles Barthe, Benjamin Grégoire, Vincent Laporte

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017

Provably secure compilation of side-channel countermeasures.

Gilles Barthe, Benjamin Grégoire, Vincent Laporte

IACR Cryptol. ePrint Arch., 2017

A Fast and Verified Software Stack for Secure Function Evaluation.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira

IACR Cryptol. ePrint Arch., 2017

Verified Translation Validation of Static Analyses.

Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

Jasmin: High-Assurance and High-Speed Cryptography.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2016

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code.

Sandrine Blazy, Vincent Laporte, David Pichardie

J. Autom. Reason., 2016

An abstract memory functor for verified C static analyzers.

Sandrine Blazy, Vincent Laporte, David Pichardie

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

A Certified Compiler for Verifiable Computing.

Cédric Fournet, Chantal Keller, Vincent Laporte

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015

Verified static analyzes for low-level languages. (Vérification d'analyses statiques pour langages de bas niveau).

Vincent Laporte

PhD thesis, 2015

A Formally-Verified C Static Analyzer.

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014

Atomicity Refinement for Verified Compilation.

Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek

ACM Trans. Program. Lang. Syst., 2014

2013

Formal Verification of a C Value Analysis Based on Abstract Interpretation.

Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie

Proceedings of the Static Analysis - 20th International Symposium, 2013

Plan B: a buffered memory model for Java.

Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

2010

On the Equality of Probabilistic Terms.

Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010