{"id":56,"date":"2015-06-16T13:44:07","date_gmt":"2015-06-16T11:44:07","guid":{"rendered":"http:\/\/members.loria.fr\/thierrygartiser\/?page_id=56"},"modified":"2022-11-25T14:21:11","modified_gmt":"2022-11-25T12:21:11","slug":"accueil","status":"publish","type":"page","link":"https:\/\/members.loria.fr\/VLaporte\/","title":{"rendered":"Vincent Laporte"},"content":{"rendered":"<h2 id=\"recent-communications\">Recent communications<\/h2>\n<ul>\n<li>\n<p><span class=\"citation\" data-cites=\"GLSEC22\"><span>\u201cFine-Grained Constant-Time Policies with Jasmin &amp; EasyCrypt.\u201d<\/span> Le g\u00e9nie logiciel au service de la s\u00e9curit\u00e9 des syst\u00e8mes<span>,<\/span> logiciels et r\u00e9seaux, CNAM, Paris, November 24, 2022. <a href=\"https:\/\/glsec22.sciencesconf.org\/\" role=\"doc-biblioref\">https:\/\/glsec22.sciencesconf.org\/<\/a>.<\/span> <a href=\"\/VLaporte\/files\/GLSEC22_FineGrainedConstantTimePolicies.pdf\">pdf<\/a>.<\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"Cambium2022\"><span>\u201cHigh-Assurance Cryptography in Jasmin &amp; Spectre Security.\u201d<\/span> Team <span class=\"smallcaps\">Cambium<\/span>, Inria, Paris, September 26, 2022. <a href=\"https:\/\/cambium.inria.fr\/seminaires\/annonces\/20220926.Vincent.Laporte.txt\" role=\"doc-biblioref\">https:\/\/cambium.inria.fr\/seminaires\/annonces\/20220926.Vincent.Laporte.txt<\/a>.<\/span> <a href=\"\/VLaporte\/files\/Cambium2022_JasminAndSpectre.pdf\">pdf<\/a>.<\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"CCS2021\">Barthe, Gilles, Benjamin Gr\u00e9goire, Vincent Laporte, and Swarn Priya <span>\u201cStructured Leakage and Applications to Cryptographic Constant-Time and Cost.\u201d<\/span> In <em>Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, <em>(<\/em><span>CCS<\/span><em>)<\/em><\/em>, 2021.<\/span> <a href=\"\/VLaporte\/files\/CCS2021_StructuredLeakage.pdf\">pdf<\/a>.<\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"CW2021\"><span>\u201cJasmin: A Certified Workbench for High-Assurance and High-Speed Cryptography.\u201d<\/span> The Coq Workshop 2021 (online), July 2, 2021. <a href=\"https:\/\/coq-workshop.gitlab.io\/2021\/\" role=\"doc-biblioref\">https:\/\/coq-workshop.gitlab.io\/2021\/<\/a>.<\/span> <a href=\"\/VLaporte\/files\/CW2021_Jasmin+presentation.pdf\">slides<\/a>.<\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"AFADL2021\"><span>\u201cMod\u00e8le de Fuite Structur\u00e9e &amp; Applications \u00e0 La Compilation S\u00e9curis\u00e9e.\u201d<\/span> Journ\u00e9es AFADL 2021 (online), June 16, 2021. <a href=\"https:\/\/www.lirmm.fr\/afadl2021\/?page=programme\" role=\"doc-biblioref\">https:\/\/www.lirmm.fr\/afadl2021\/?page=programme<\/a>.<\/span> <a href=\"https:\/\/eprint.iacr.org\/2021\/650\">eprint<\/a>; <a href=\"\/VLaporte\/files\/AFADL2021_LeakTransformers+presentation.pdf\">slides<\/a>.<\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"SP2020:Jasmin\">Almeida, Jos\u00e9 Bacelar, Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9goire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub <span>\u201cThe Last Mile: High-Assurance and High-Speed Cryptographic Implementations.\u201d<\/span> In <em>41<sup>st<\/sup> IEEE Symposium on Security and Privacy, <em>(<\/em>s&amp;p<em>)<\/em><\/em>, 2020.<\/span><\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"POPL20:CompCert-CT\">Barthe, Gilles, Sandrine Blazy, Benjamin Gr\u00e9goire, R\u00e9mi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu <span>\u201cFormal Verification of a Constant-Time Preserving <span>C<\/span> Compiler.\u201d<\/span> <em>Proceedings of the ACM on Programming Languages <em>(<\/em>POPL<em>)<\/em><\/em>, 2020.<\/span><\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"CSF18:Pintarda\">Barthe, Gilles, Benjamin Gr\u00e9goire, and Vincent Laporte <span>\u201cSecure Compilation of Side-Channel Countermeasures: The Case of Cryptographic <span>\u2018Constant-Time\u2019<\/span>.\u201d<\/span> In <em>31<sup>st<\/sup> <span>IEEE<\/span> Computer Security Foundations Symposium, <em>(<\/em><span>CSF<\/span><em>)<\/em><\/em>, 2018.<\/span> <a href=\"\/VLaporte\/files\/CSF2018_ConstantTimePreservation.pdf\">pdf<\/a>; <a href=\"\/VLaporte\/files\/CSF2018_ConstantTimePreservation+presentation.pdf\">slides<\/a>.<\/p>\n<\/li>\n<\/ul>\n<h2 id=\"research-projects\">Research projects<\/h2>\n<h3 id=\"jasmin\">Jasmin<\/h3>\n<p><a href=\"https:\/\/github.com\/jasmin-lang\/jasmin\">Jasmin<\/a> is a programming language to write <em>high-assurance<\/em>, <em>high-speed<\/em> cryptographic implementations.<\/p>\n<p>Its compiler is correct \u2014 formally verified in <a href=\"https:\/\/coq.inria.fr\/\">Coq<\/a>.<\/p>\n<h4 id=\"relevant-publications\">Relevant publications<\/h4>\n<ul>\n<li>\n<p><span class=\"citation\" data-cites=\"CCS17:Jasmin\">Almeida, Jos\u00e9 Bacelar, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Gr\u00e9goire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub <span>\u201cJasmin: High-Assurance and High-Speed Cryptography.\u201d<\/span> In <em>Proceedings of the 24<sup>th<\/sup> <span>ACM<\/span> Conference on Computer and Communications Security, <em>(<\/em><span>CCS<\/span><em>)<\/em><\/em>, 2017.<\/span> <a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-01649140\/file\/main.pdf\">pdf from HAL<\/a>; <a href=\"\/VLaporte\/files\/CCS2017_Jasmin+presentation.pdf\">slides<\/a>.<\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"CCS19:SHA3\">Almeida, Jos\u00e9 Bacelar, C\u00e9cile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub <span>\u201cMachine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.\u201d<\/span> In <em>Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, <em>(<\/em><span>CCS<\/span><em>)<\/em><\/em>, 2019.<\/span><\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"SP2020:Jasmin\">Almeida, Jos\u00e9 Bacelar, Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9goire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub <span>\u201cThe Last Mile: High-Assurance and High-Speed Cryptographic Implementations.\u201d<\/span> In <em>41<sup>st<\/sup> IEEE Symposium on Security and Privacy, <em>(<\/em>s&amp;p<em>)<\/em><\/em>, 2020.<\/span><\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"cryptoeprint:2022\/1270\">Shivakumar, Basavesh Ammanaghatta, Gilles Barthe, Benjamin Gr\u00e9goire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, and Lucas Tabary-Maujean <span>\u201cTyping High-Speed Cryptography Against <span class=\"nocase\">Spectre v1<\/span>.\u201d<\/span> Cryptology ePrint Archive, Paper 2022\/1270, 2022. <a href=\"https:\/\/eprint.iacr.org\/2022\/1270\" role=\"doc-biblioref\">https:\/\/eprint.iacr.org\/2022\/1270<\/a>.<\/span><\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"CCS2022\">Shivakumar, Basavesh Ammanaghatta, Gilles Barthe, Benjamin Gr\u00e9goire, Vincent Laporte, and Swarn Priya <span>\u201cEnforcing Fine-Grained Constant-Time Policies.\u201d<\/span> In <em>Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, <em>(<\/em><span>CCS<\/span><em>)<\/em><\/em>, 2022. doi:<a href=\"https:\/\/doi.org\/10.1145\/3548606.3560689\" role=\"doc-biblioref\">10.1145\/3548606.3560689<\/a>.<\/span><\/p>\n<\/li>\n<\/ul>\n<h4 id=\"lectures\">Lectures<\/h4>\n<ul>\n<li><a href=\"\/VLaporte\/files\/CyberIn2022.html\">Cyber In Nancy 2022<\/a><\/li>\n<li><a href=\"\/VLaporte\/files\/sac2021.html\">SAC 2021 Summer School<\/a><\/li>\n<\/ul>\n<h3 id=\"verasco\">Verasco<\/h3>\n<p><a href=\"http:\/\/compcert.inria.fr\/verasco\/\">Verasco<\/a> is a formally-verified static analyzer for C.<\/p>\n<h4 id=\"relevant-publications-1\">Relevant publications<\/h4>\n<ul>\n<li>\n<p><span class=\"citation\" data-cites=\"ICFP16\">Blazy, Sandrine, Vincent Laporte, and David Pichardie <span>\u201cAn Abstract Memory Functor for Verified <span>C<\/span> Static Analyzers.\u201d<\/span> In <em>Proceedings of the 21<sup>st<\/sup> <span>ACM<\/span> <span>SIGPLAN<\/span> International Conference on Functional Programming, <em>(<\/em><span>ICFP<\/span><em>)<\/em><\/em>, 325\u201337, 2016.<\/span><\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"POPL15:Verasco\">Jourdan, Jacques-Henri, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie <span>\u201cA Formally-Verified <span>C<\/span> Static Analyzer.\u201d<\/span> In <em>Proc. Of the 42<sup>th<\/sup> Symp. On Princ. Of Prog. Languages\u00a0<em>(<\/em><span>POPL<\/span><em>)<\/em><\/em>. ACM, 2015.<\/span><\/p>\n<\/li>\n<li>\n<p><span class=\"citation\" data-cites=\"SAS13:Blazy:al\">Blazy, Sandrine, Vincent Laporte, Andr\u00e9 Maroneze, and David Pichardie <span>\u201cFormal Verification of a <span>C<\/span> Value Analysis Based on Abstract Interpretation.\u201d<\/span> In <em>Proc. Of the 20<sup>th<\/sup> Static Analysis Symposium <em>(<\/em><span>SAS<\/span><em>)<\/em><\/em>. Lecture Notes in Computer Science. Springer-Verlag, 2013.<\/span><\/p>\n<\/li>\n<\/ul>\n<h3 id=\"pinocchioq\">PinocchioQ<\/h3>\n<p>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.<\/p>\n<h4 id=\"downloads\">Downloads<\/h4>\n<ul>\n<li><a href=\"\/VLaporte\/files\/PinocchioQ-v1.0.tgz\">Original source code<\/a> for CompCert 2.4, Coq 8.4pl6, OCaml 4.02.<\/li>\n<li><a href=\"\/VLaporte\/files\/PinocchioQ-for-CompCert-3.6.tgz\">Port to CompCert 3.6<\/a> for Coq 8.9.1, OCaml 4.08.<\/li>\n<\/ul>\n<h4 id=\"relevant-publication\">Relevant publication<\/h4>\n<ul>\n<li><span class=\"citation\" data-cites=\"CSF16:Pinocchioq\">Fournet, C\u00e9dric, Chantal Keller, and Vincent Laporte <span>\u201cA Certified Compiler for Verifiable Computing.\u201d<\/span> In <em>29<sup>th<\/sup> <span>IEEE<\/span> Computer Security Foundations Symposium, <em>(<\/em><span>CSF<\/span><em>)<\/em><\/em>, 268\u201380, 2016. doi:<a href=\"https:\/\/doi.org\/10.1109\/CSF.2016.26\" role=\"doc-biblioref\">10.1109\/CSF.2016.26<\/a>.<\/span> <a href=\"\/VLaporte\/files\/CSF2016_PinocchioQ.pdf\">pdf<\/a> <a href=\"\/VLaporte\/files\/CSF2016_PinocchioQ+presentation.pdf\">slides<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Recent communications \u201cFine-Grained Constant-Time Policies with Jasmin &amp; EasyCrypt.\u201d Le g\u00e9nie logiciel au service de la s\u00e9curit\u00e9 des syst\u00e8mes, logiciels et r\u00e9seaux, CNAM, Paris, November 24, 2022. https:\/\/glsec22.sciencesconf.org\/. pdf. \u201cHigh-Assurance Cryptography in Jasmin &amp; Spectre Security.\u201d Team Cambium, Inria, Paris, September 26, 2022. https:\/\/cambium.inria.fr\/seminaires\/annonces\/20220926.Vincent.Laporte.txt. pdf. Barthe, Gilles, Benjamin Gr\u00e9goire, Vincent Laporte, and Swarn Priya \u201cStructured [&hellip;]<\/p>\n","protected":false},"author":5,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-56","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/pages\/56","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/users\/5"}],"replies":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/comments?post=56"}],"version-history":[{"count":27,"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/pages\/56\/revisions"}],"predecessor-version":[{"id":270,"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/pages\/56\/revisions\/270"}],"wp:attachment":[{"href":"https:\/\/members.loria.fr\/VLaporte\/wp-json\/wp\/v2\/media?parent=56"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}