Vincent Laporte

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