Skip to Main content
Number of documents

17

אב


Journal articles3 documents

  • Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, et al.. Formal verification of a constant-time preserving C compiler. Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩. ⟨hal-02975012⟩
  • Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning, Springer Verlag, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩. ⟨hal-01243700⟩
  • Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek. Atomicity Refinement for Verified Compilation. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, pp.30. ⟨hal-01102435⟩

Conference papers12 documents

  • José Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira. Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. International Conference on Cryptology in India, Dec 2020, Bangalore, India. ⟨hal-02983256⟩
  • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, et al.. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. SP 2020 - IEEE Symposium on Security and Privacy, May 2020, San Francisco, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩. ⟨hal-02974993⟩
  • José Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, et al.. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019 - 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩. ⟨hal-02404581⟩
  • Gilles Barthe, Benjamin Grégoire, Vincent Laporte. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”. CSF 2018 - 31st IEEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom. ⟨hal-01959560⟩
  • José Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, et al.. A Fast and Verified Software Stack for Secure Function Evaluation. CCS 2017 - ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-18. ⟨hal-01649104⟩
  • Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu. Verified Translation Validation of Static Analyses. Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States. ⟨hal-01588422⟩
  • Cédric Fournet, Chantal Keller, Vincent Laporte. A Certified Compiler for Verifiable Computing. IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal. ⟨hal-01397680⟩
  • Sandrine Blazy, Vincent Laporte, David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩. ⟨hal-01339969⟩
  • Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A formally-verified C static analyzer. POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩. ⟨hal-01078386⟩
  • Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. pp.128 - 143, ⟨10.1007/978-3-319-08970-6_9⟩. ⟨hal-01102445⟩
  • Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, et al.. Plan B: A Buffered Memory Model for Java. Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Jan 2013, Rome, Italy. ⟨hal-00924716⟩
  • Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344. ⟨hal-00812515⟩

Theses1 document

Master thesis1 document

  • Vincent Laporte. Static Analysis of x86 Assembly: Certification and Robustness Analysis. Hardware Architecture [cs.AR]. 2011. ⟨dumas-00636445⟩