Vincent Laporte

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 31

Top Venues

IACR Cryptol. ePrint Arch.

CCS

CSF

IACR Trans. Cryptogr. Hardw. Embed. Syst.

University of Rennes 1, France (PHD)

Education History

University of Rennes 1, France

PHD

Publications

Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
Preservation of Speculative Constant-time by Compilation. IACR Cryptol. ePrint Arch. 2024 (2024)
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
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024 (2024)
Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
High-assurance zeroization. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024 (1) (2024)
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
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) (2024)
Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
Protecting cryptographic code against Spectre-RSB. IACR Cryptol. ePrint Arch. 2024 (2024)
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
Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. 2023 (2023)
Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
High-assurance zeroization. IACR Cryptol. ePrint Arch. 2023 (2023)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
Typing High-Speed Cryptography against Spectre v1. SP (2023)
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
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023 (3) (2023)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Enforcing fine-grained constant-time policies. IACR Cryptol. ePrint Arch. 2022 (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Enforcing Fine-grained Constant-time Policies. CCS (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
Typing High-Speed Cryptography against Spectre v1. IACR Cryptol. ePrint Arch. 2022 (2022)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. IACR Cryptol. ePrint Arch. 2021 (2021)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS (2021)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4 (POPL) (2020)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira
Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. INDOCRYPT (2020)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. IEEE Symposium on Security and Privacy (2020)
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
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019 (2019)
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
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR (2019)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. 2019 (2019)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". CSF (2018)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
Jasmin: High-Assurance and High-Speed Cryptography. CCS (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
A Fast and Verified Software Stack for Secure Function Evaluation. IACR Cryptol. ePrint Arch. 2017 (2017)
Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu
Verified Translation Validation of Static Analyses. CSF (2017)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
Provably secure compilation of side-channel countermeasures. IACR Cryptol. ePrint Arch. 2017 (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
A Fast and Verified Software Stack for Secure Function Evaluation. CCS (2017)
Sandrine Blazy, Vincent Laporte, David Pichardie
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. J. Autom. Reason. 56 (3) (2016)
Cédric Fournet, Chantal Keller, Vincent Laporte
A Certified Compiler for Verifiable Computing. CSF (2016)
Sandrine Blazy, Vincent Laporte, David Pichardie
An abstract memory functor for verified C static analyzers. ICFP (2016)
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
A Formally-Verified C Static Analyzer. POPL (2015)
Suresh Jagannathan, Gustavo Petri, Jan Vitek, David Pichardie, Vincent Laporte
Atomicity refinement for verified compilation. PLDI (2014)
Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek
Atomicity Refinement for Verified Compilation. ACM Trans. Program. Lang. Syst. 36 (2) (2014)
Sandrine Blazy, Vincent Laporte, David Pichardie
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. ITP (2014)
Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS (2013)
Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
Formal Verification of a C Value Analysis Based on Abstract Interpretation CoRR (2013)
Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek
Plan B: a buffered memory model for Java. POPL (2013)
Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte
On the Equality of Probabilistic Terms. LPAR (Dakar) (2010)

Vincent Laporte.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Vincent Laporte