Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2025 Computer and Communications Security | October 2025
Tahina Ramananandro
Principal Research Software Development Engineer
论文与出版物
-
-
-
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
2025 Programming Language Design and Implementation | June 2025
-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
-
-
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
-
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
Certified Programs and Proofs | January 2023
-
-
-
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
-
-
-
Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro
26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021) | August 2021
-
FastVer: Making Data Integrity a Commodity
Arvind Arasu, Aseem Rastogi, Badrish Chandramouli, Donald Kossmann, Esha Ghosh, Johannes Gehrke, Nikhil Swamy, Jonathan Protzenko, Ravi Ramamurthy, Srinath Setty, Tahina Ramananandro, Alexander van Renen, Min Xu
SIGMOD | June 2021
-
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
-
-
-
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
-
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martinez, 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
European Symposium On Programming | April 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
-
-
-
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
-
-
-
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2025 Computer and Communications Security | October 2025
-
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
2025 Programming Language Design and Implementation | June 2025
-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
Certified Programs and Proofs | January 2023
-
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
-
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
-
Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro
26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021) | August 2021
-
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
-
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martinez, 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
European Symposium On Programming | April 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
-
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
-
-
-
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2025 Computer and Communications Security | October 2025
-
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
Certified Programs and Proofs | January 2023
-
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
-
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
-
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
-
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
-
-
-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
-
-
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
Certified Programs and Proofs | January 2023
-
FastVer: Making Data Integrity a Commodity
Arvind Arasu, Aseem Rastogi, Badrish Chandramouli, Donald Kossmann, Esha Ghosh, Johannes Gehrke, Nikhil Swamy, Jonathan Protzenko, Ravi Ramamurthy, Srinath Setty, Tahina Ramananandro, Alexander van Renen, Min Xu
SIGMOD | June 2021
-
-
-
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
-
-
-
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2025 Computer and Communications Security | October 2025
-
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
2025 Programming Language Design and Implementation | June 2025
-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
Certified Programs and Proofs | January 2023
-
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
-
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
-
Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro
26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021) | August 2021
-
FastVer: Making Data Integrity a Commodity
Arvind Arasu, Aseem Rastogi, Badrish Chandramouli, Donald Kossmann, Esha Ghosh, Johannes Gehrke, Nikhil Swamy, Jonathan Protzenko, Ravi Ramamurthy, Srinath Setty, Tahina Ramananandro, Alexander van Renen, Min Xu
SIGMOD | June 2021
-
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
-
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
-
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martinez, 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
European Symposium On Programming | April 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
-
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
-