Vincent Laporte

Research Engineer at Inria, working on the Coq proof assistant.

E-mail: Vincent [dot] Laporte [at] mailbox [dot] org

PGP: EBD582AD DDB1F81F

Phone: 0 (033) 2 99 84 74 54

Work address:

Curriculum vitæ (pdf, 67 Kio).

Publications

See dblp for a complete list.

Selected publications

• Barthe, Gilles, Benjamin Grégoire, and Vincent Laporte “Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic ‘Constant-Time’.” In 31^st IEEE Computer Security Foundations Symposium, (CSF), 2018. pdf slides

• 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 24^th ACM Conference on Computer and Communications Security, (CCS), 2017. pdf from HAL slides

• Blazy, Sandrine, Vincent Laporte, and David Pichardie “Verified Abstract Interpretation Techniques for Disassembling Low-Level Self-Modifying Code.” Journal of Automated Reasoning 56, no. 3 (2016): 283–308. doi:10.1007/s10817-015-9359-8. pdf from HAL

Research projects

Jasmin

Jasmin is a programming language to write high-assurance, high-speed cryptographic implementations.

Its compiler is correct — formally verified in Coq.

Verasco

Verasco is a formally-verified static analyzer for C.