papers.md

layout	title	permalink
page	Papers	/papers/

2023
[24]	Galapagos: Developing Verified Low-Level Cryptography on Heterogeneous Hardware (Yi Zhou, Sarah Cai, Menucha Winchell, Bryan Parno) Proceedings of the ACM Conference on Computer and Communications Security (CCS) November, 2023. [pdf]
[23]	Mariposa: Measuring SMT Instability in Automated Program Verification ( Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, Bryan Parno) Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference October, 2023. [pdf] [tech-report]
[22]	Owl: Compositional Verification of Security Protocols via an Information-Flow Type System (Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, Bryan Parno) Proceedings of the IEEE Symposium on Security and Privacy May, 2023. [pdf]
2022
[21]	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) Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '22), June 13--17, 2022, San Diego, CA, USA 2022. [pdf]
2021
[20]	Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martinez, Denis Merigoux, Tahina Ramananandro) 26th ACM SIGPLAN International Conference on Functional Programming 2021. [pdf]
[19]	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) To Appear In The Proceedings of the 42nd IEEE Symposium on Security & Privacy 2021. [pdf] [eprint]
2020
[18]	HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms) (Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin) In Proceedings of the 27th ACM/SIGSAC International Conference on Computer and Communications Security (CCS) 2020. [pdf] [eprint]
[17]	SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez) In Proceedings of the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2020.
[16]	Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel) In Proceedings of the 12th Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) 2020. [pdf] [doi]
[15]	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, Cedric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, Santiago Zanella-Beguelin ) In Proceedings of the 41st IEEE Symposium on Security & Privacy 2020. [pdf] [eprint]
2019
[14]	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) In Proceedings of the 28th USENIX Security Symposium 2019.
[13]	Dijkstra Monads for All (Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019. [bibtex] [pdf]
[12]	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), In 28th European Symposium on Programming (ESOP), Springer, 2019. [bibtex] [pdf] [doi]
[11]	Formally Verified Cryptographic Web Applications in WebAssembly (J. Protzenko, B. Beurdouche, D. Merigoux, K. Bhargavan), In 2019 IEEE Symposium on Security and Privacy (SP), 2019. [bibtex] [pdf]
[10]	Wys*: A DSL for Verified Secure Multi-party Computations (Aseem Rastogi, Nikhil Swamy, Michael Hicks), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, 2019. [bibtex] [pdf] [doi]
[9]	A Verified, Efficient Embedding of a Verifiable Assembly Language (Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy) In Proceedings of the Symposium on Principles of Programming Languages (POPL) 2019.
2018
[8]	Recalling a Witness: Foundations and Applications of Monotonic State (Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy), In PACMPL, volume 2(POPL), 2018. [bibtex] [pdf]
[7]	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), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018. [bibtex] [pdf]
2017
[6]	HACL*: A Verified Modern Cryptographic Library (Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche) In Proceedings of the ACM Conference on Computer and Communications Security (CCS) 2017.
[5]	Vale: Verifying High-Performance Cryptographic Assembly Code (Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson) In Proceedings of the USENIX Security Symposium (Distinguished Paper Award) 2017.
[4]	Implementing and Proving the TLS 1.3 Record Layer (Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jiangyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Jean Karim Zinzindohoué) In 38th IEEE Symposium on Security and Privacy, IEEE Computer Society 2017. 2017. [bibtex] [pdf]
[3]	Everest: Towards a Verified, Drop-in Replacement of HTTPS (Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Cătălin Hriţcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué) In Proceedings of the Summit on Advances in Programming Languages (SNAPL). 2017 .
[2]	Verified Low-Level Programming Embedded in F* (Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy), In PACMPL, volume 1(ICFP), 2017. [bibtex] [pdf] [doi]
[1]	Dijkstra Monads for Free (Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017. [bibtex] [pdf]