ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy
Certified Programs and Proofs | January 2023
Accepted for publication, to appear
Project Everest
Building and deploying provably secure communication software
Publications
Publications
Publications by Year
-
-
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta
2022 Programming Language Design and Implementation | June 2022
-
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
IEEE Symposium on Security and Privacy | May 2021
-
HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
ACM Conference on Computer and Communications Security (CCS) | November 2020
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
25th ACM SIGPLAN International Conference on Functional Programming (ICFP) | August 2020
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
12th Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) | July 2020
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
USENIX Security | August 2019
Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martinez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
24th ACM SIGPLAN International Conference on Functional Programming (ICFP) | June 2019
Formally Verified Cryptographic Web Applications in WebAssembly
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
2019 IEEE Symposium on Security and Privacy (SP) | May 2019
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
ESOP 2019 | April 2019
Wys*: A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks
Principles of Security and Trust (POST 2019) | April 2019
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
-
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
CPP 2018 | January 2018
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages 2018 (POPL 2018) | January 2018
-
HACL*: A Verified Modern Cryptographic Library
Karthikeyan Bhargavan, Benjamin Beurdouche, Jean-Karim Zinzindohoué, Jonathan Protzenko
ACM CCS | September 2017
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
Implementing and Proving the TLS 1.3 Record Layer
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
SP ’17 38th IEEE Symposium on Security and Privacy | May 2017
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 – 2nd Summit on Advances in Programming Languages | May 2017
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
22nd International Conference on Functional Programming (ICFP 2017) | May 2017
Dijkstra monads for free
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
POPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | January 2017
Publications by Research Area
-
ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy
Certified Programs and Proofs | January 2023
Accepted for publication, to appear
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta
2022 Programming Language Design and Implementation | June 2022
HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
ACM Conference on Computer and Communications Security (CCS) | November 2020
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
25th ACM SIGPLAN International Conference on Functional Programming (ICFP) | August 2020
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
USENIX Security | August 2019
Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martinez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
24th ACM SIGPLAN International Conference on Functional Programming (ICFP) | June 2019
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
ESOP 2019 | April 2019
Wys*: A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks
Principles of Security and Trust (POST 2019) | April 2019
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
CPP 2018 | January 2018
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages 2018 (POPL 2018) | January 2018
HACL*: A Verified Modern Cryptographic Library
Karthikeyan Bhargavan, Benjamin Beurdouche, Jean-Karim Zinzindohoué, Jonathan Protzenko
ACM CCS | September 2017
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
Implementing and Proving the TLS 1.3 Record Layer
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
SP ’17 38th IEEE Symposium on Security and Privacy | May 2017
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 – 2nd Summit on Advances in Programming Languages | May 2017
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
22nd International Conference on Functional Programming (ICFP 2017) | May 2017
Dijkstra monads for free
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
POPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | January 2017
-
ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy
Certified Programs and Proofs | January 2023
Accepted for publication, to appear
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta
2022 Programming Language Design and Implementation | June 2022
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
IEEE Symposium on Security and Privacy | May 2021
HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
ACM Conference on Computer and Communications Security (CCS) | November 2020
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
12th Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) | July 2020
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
USENIX Security | August 2019
Formally Verified Cryptographic Web Applications in WebAssembly
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
2019 IEEE Symposium on Security and Privacy (SP) | May 2019
Wys*: A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks
Principles of Security and Trust (POST 2019) | April 2019
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages 2018 (POPL 2018) | January 2018
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
Implementing and Proving the TLS 1.3 Record Layer
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
SP ’17 38th IEEE Symposium on Security and Privacy | May 2017
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 – 2nd Summit on Advances in Programming Languages | May 2017
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
22nd International Conference on Functional Programming (ICFP 2017) | May 2017
-
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
Publications by Type
-
ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy
Certified Programs and Proofs | January 2023
Accepted for publication, to appear
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta
2022 Programming Language Design and Implementation | June 2022
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
IEEE Symposium on Security and Privacy | May 2021
HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
ACM Conference on Computer and Communications Security (CCS) | November 2020
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
25th ACM SIGPLAN International Conference on Functional Programming (ICFP) | August 2020
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
12th Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) | July 2020
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
USENIX Security | August 2019
Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martinez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
24th ACM SIGPLAN International Conference on Functional Programming (ICFP) | June 2019
Formally Verified Cryptographic Web Applications in WebAssembly
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
2019 IEEE Symposium on Security and Privacy (SP) | May 2019
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
ESOP 2019 | April 2019
Wys*: A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks
Principles of Security and Trust (POST 2019) | April 2019
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
CPP 2018 | January 2018
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages 2018 (POPL 2018) | January 2018
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
Implementing and Proving the TLS 1.3 Record Layer
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
SP ’17 38th IEEE Symposium on Security and Privacy | May 2017
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 – 2nd Summit on Advances in Programming Languages | May 2017
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
22nd International Conference on Functional Programming (ICFP 2017) | May 2017
Dijkstra monads for free
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
POPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | January 2017
-
HACL*: A Verified Modern Cryptographic Library
Karthikeyan Bhargavan, Benjamin Beurdouche, Jean-Karim Zinzindohoué, Jonathan Protzenko
ACM CCS | September 2017