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
Nikhil Swamy
Senior Principal Researcher
论文与出版物
-
-
-
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
-
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
-
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 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
-
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
-
-
-
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
-
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
-
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
-
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
-
-
-
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
MSR-TR-2018-33 | July 2018
作者：Microsoft
-
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
-
-
-
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
-
-
-
Formal Verification of Smart Contracts: Short Paper
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
PLAS '16 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security | October 2016
ISBN: 978-1-4503-4574-3
-
Towards a Provably Secure Implementation of TLS 1.3
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin
TRON Workshop | July 2016
-
Dependent Types and Multi-Monadic Effects in F*
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin
POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2016
ISBN: 978-1-4503-3549-2
-
-
-
Safe & Efficient Gradual Typing for TypeScript
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, Panagiotis Vekris
POPL '15 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
ISBN: 978-1-4503-3300-9
-
-
-
Safe & Efficient Gradual Typing for TypeScript
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, Panagiotis Vekris
MSR-TR-2014-99 | July 2014
-
Gradual Typing Embedded Securely in JavaScript
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin Bierman
POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2014
ISBN: 978-1-4503-2544-8
-
Probabilistic Relational Verification for Cryptographic Implementations
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Santiago Zanella-Béguelin, Nikhil Swamy
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 | January 2014
To appear
-
-
-
Increasing Human-Tool Interaction via the Web
Thomas Ball, Jonathan "Peli" de Halleux, Daan Leijen, Nikhil Swamy
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering | June 2013
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering
-
Verifying Higher-order Programs with the Dijkstra Monad
Nikhil Swamy, Juan Chen, Ben Livshits
ACM Programming Language Design and Implementation (PLDI) 2013 | June 2013
ACM Programming Language Design and Implementation (PLDI) 2013
-
DKAL*: Constructing Executable Specifications of Authorization Protocols
Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
MSR-TR-2012-24 | March 2013
International Symposium on Engineering Secure Software and Systems (ESSOS 13)
-
Fully Abstract Compilation to JavaScript
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, Ben Livshits
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013 | January 2013
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013
-
-
-
Probabilistic Relational Verification for Cryptographic Implementations
Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
November 2012
-
Verification Condition Generation with the Dijkstra State Monad
Cole Schlesinger, Nikhil Swamy
MSR-TR-2012-45 | April 2012
-
Monadic Reï¬nement Types for Verifying JavaScript Programs
Nikhil Swamy, Joel Weinberger, Juan Chen, Ben Livshits, Cole Schlesinger
MSR-TR-2012-37 | March 2012
-
Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
To appear
-
-
-
Secure Distributed Programming with Value-dependent Types
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011) | September 2011
-
Lightweight Monadic Programming in ML
Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks
Proceedings of the International Conference of Functional Programming (ICFP'11) | July 2011
Proceedings of the International Conference of Functional Programming (ICFP'11)
-
Modular Protections against Non-Control Data Attacks
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Ben Zorn
IEEE Symposium on Computer Security Foundations | June 2011
-
Verified Security for Browser Extensions
Arjun Guha, Matthew Fredrikson, Benjamin Livshits, Nikhil Swamy, Ben Livshits
Proceedings of the IEEE Symposium on Security and Privacy (Oakland) | May 2011
-
Lightweight Monadic Programming in ML
Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks
MSR-TR-2011-39 | March 2011
-
Secure Distributed Programming with Value-Dependent Types
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, Jean Yang
MSR-TR-2011-37 | March 2011
This is an extended version of the conference paper (ICFP '11) with the same title. A final version of this full technical report is forthcoming.
-
Verifying Stateful Programs with Substructural State and Hoare Types
Juan Chen, Nikhil Swamy
Programming Language meets Program Verification (PLPV 2011) | January 2011
-
-
-
Modular Protections against Non-Control Data Attacks
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Ben Zorn
MSR-TR-2010-158 | November 2010
-
Verified Security for Browser Extensions
Nikhil Swamy, Benjamin Livshits, Arjun Guha, Matthew Fredrikson, Ben Livshits
MSR-TR-2010-157 | November 2010
-
Verified Stateful Programs with Substructural State and Hoare Types
Juan Chen, Nikhil Swamy
MSR-TR-2010-95 | July 2010
-
Type-preserving compilation for end-to-end verification of security enforcement
Juan Chen, Nikhil Swamy, Ravi Chugh
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
-
Enforcing Stateful Authorization and Information Flow Policies in Fine
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-164 | March 2010
ESOP 2010: 19th European Symposium on Programming
-
-
-
End-to-end Verification of Security Enforcement is Fine (Extended version)
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-98 | August 2009
-
Collaborative End-to-end Enforcement of Security Policies in Distributed Systems
MSR-TR-2009-72 | June 2009
-
A Theory of Typed Coercions and its Applications
Nikhil Swamy, Michael Hicks, Gavin Bierman
MSR-TR-2009-69 | June 2009
SPIE Astronomy Telescopes and Instruments
-
-
-
Verified Implementations of the Information Card Federated Identity-Management Protocol
Karthik Bhargavan, Cédric Fournet, Andy Gordon, Nikhil Swamy
ASIACCS '08 Proceedings of the 2008 ACM symposium on Information, computer and communications security | March 2008
ISBN: 978-1-59593-979-1
-
-
-
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
-
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 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
-
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
-
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
-
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
-
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
-
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
-
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
MSR-TR-2018-33 | July 2018
作者：Microsoft
-
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
-
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
-
Formal Verification of Smart Contracts: Short Paper
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
PLAS '16 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security | October 2016
ISBN: 978-1-4503-4574-3
-
Towards a Provably Secure Implementation of TLS 1.3
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin
TRON Workshop | July 2016
-
Dependent Types and Multi-Monadic Effects in F*
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin
POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2016
ISBN: 978-1-4503-3549-2
-
Safe & Efficient Gradual Typing for TypeScript
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, Panagiotis Vekris
POPL '15 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
ISBN: 978-1-4503-3300-9
-
Safe & Efficient Gradual Typing for TypeScript
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, Panagiotis Vekris
MSR-TR-2014-99 | July 2014
-
Gradual Typing Embedded Securely in JavaScript
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin Bierman
POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2014
ISBN: 978-1-4503-2544-8
-
Probabilistic Relational Verification for Cryptographic Implementations
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Santiago Zanella-Béguelin, Nikhil Swamy
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 | January 2014
To appear
-
Increasing Human-Tool Interaction via the Web
Thomas Ball, Jonathan "Peli" de Halleux, Daan Leijen, Nikhil Swamy
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering | June 2013
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering
-
DKAL*: Constructing Executable Specifications of Authorization Protocols
Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
MSR-TR-2012-24 | March 2013
International Symposium on Engineering Secure Software and Systems (ESSOS 13)
-
Fully Abstract Compilation to JavaScript
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, Ben Livshits
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013 | January 2013
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013
-
Monadic Reï¬nement Types for Verifying JavaScript Programs
Nikhil Swamy, Joel Weinberger, Juan Chen, Ben Livshits, Cole Schlesinger
MSR-TR-2012-37 | March 2012
-
Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
To appear
-
Secure Distributed Programming with Value-dependent Types
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011) | September 2011
-
Lightweight Monadic Programming in ML
Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks
Proceedings of the International Conference of Functional Programming (ICFP'11) | July 2011
Proceedings of the International Conference of Functional Programming (ICFP'11)
-
Modular Protections against Non-Control Data Attacks
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Ben Zorn
IEEE Symposium on Computer Security Foundations | June 2011
-
Lightweight Monadic Programming in ML
Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks
MSR-TR-2011-39 | March 2011
-
Secure Distributed Programming with Value-Dependent Types
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, Jean Yang
MSR-TR-2011-37 | March 2011
This is an extended version of the conference paper (ICFP '11) with the same title. A final version of this full technical report is forthcoming.
-
Verifying Stateful Programs with Substructural State and Hoare Types
Juan Chen, Nikhil Swamy
Programming Language meets Program Verification (PLPV 2011) | January 2011
-
Modular Protections against Non-Control Data Attacks
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Ben Zorn
MSR-TR-2010-158 | November 2010
-
Type-preserving compilation for end-to-end verification of security enforcement
Juan Chen, Nikhil Swamy, Ravi Chugh
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
-
Enforcing Stateful Authorization and Information Flow Policies in Fine
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-164 | March 2010
ESOP 2010: 19th European Symposium on Programming
-
End-to-end Verification of Security Enforcement is Fine (Extended version)
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-98 | August 2009
-
A Theory of Typed Coercions and its Applications
Nikhil Swamy, Michael Hicks, Gavin Bierman
MSR-TR-2009-69 | June 2009
SPIE Astronomy Telescopes and Instruments
-
-
-
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
-
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
-
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
-
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
-
Probabilistic Relational Verification for Cryptographic Implementations
Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
November 2012
-
Monadic Reï¬nement Types for Verifying JavaScript Programs
Nikhil Swamy, Joel Weinberger, Juan Chen, Ben Livshits, Cole Schlesinger
MSR-TR-2012-37 | March 2012
-
Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
To appear
-
Type-preserving compilation for end-to-end verification of security enforcement
Juan Chen, Nikhil Swamy, Ravi Chugh
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
-
End-to-end Verification of Security Enforcement is Fine (Extended version)
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-98 | August 2009
-
Verified Implementations of the Information Card Federated Identity-Management Protocol
Karthik Bhargavan, Cédric Fournet, Andy Gordon, Nikhil Swamy
ASIACCS '08 Proceedings of the 2008 ACM symposium on Information, computer and communications security | March 2008
ISBN: 978-1-59593-979-1
-
-
-
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
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 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
-
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
-
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
-
Collaborative End-to-end Enforcement of Security Policies in Distributed Systems
MSR-TR-2009-72 | June 2009
-
-
-
Increasing Human-Tool Interaction via the Web
Thomas Ball, Jonathan "Peli" de Halleux, Daan Leijen, Nikhil Swamy
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering | June 2013
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering
-
-
-
Verifying Higher-order Programs with the Dijkstra Monad
Nikhil Swamy, Juan Chen, Ben Livshits
ACM Programming Language Design and Implementation (PLDI) 2013 | June 2013
ACM Programming Language Design and Implementation (PLDI) 2013
-
Verification Condition Generation with the Dijkstra State Monad
Cole Schlesinger, Nikhil Swamy
MSR-TR-2012-45 | April 2012
-
Verified Security for Browser Extensions
Arjun Guha, Matthew Fredrikson, Benjamin Livshits, Nikhil Swamy, Ben Livshits
Proceedings of the IEEE Symposium on Security and Privacy (Oakland) | May 2011
-
Verified Security for Browser Extensions
Nikhil Swamy, Benjamin Livshits, Arjun Guha, Matthew Fredrikson, Ben Livshits
MSR-TR-2010-157 | November 2010
-
Verified Stateful Programs with Substructural State and Hoare Types
Juan Chen, Nikhil Swamy
MSR-TR-2010-95 | July 2010
-
-
-
Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
To appear
-
Type-preserving compilation for end-to-end verification of security enforcement
Juan Chen, Nikhil Swamy, Ravi Chugh
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
-
End-to-end Verification of Security Enforcement is Fine (Extended version)
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-98 | August 2009
-
-
-
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
-
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 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
-
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
-
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
-
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
-
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
-
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
-
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
-
Formal Verification of Smart Contracts: Short Paper
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
PLAS '16 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security | October 2016
ISBN: 978-1-4503-4574-3
-
Towards a Provably Secure Implementation of TLS 1.3
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin
TRON Workshop | July 2016
-
Dependent Types and Multi-Monadic Effects in F*
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin
POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2016
ISBN: 978-1-4503-3549-2
-
Safe & Efficient Gradual Typing for TypeScript
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, Panagiotis Vekris
POPL '15 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
ISBN: 978-1-4503-3300-9
-
Gradual Typing Embedded Securely in JavaScript
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin Bierman
POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2014
ISBN: 978-1-4503-2544-8
-
Probabilistic Relational Verification for Cryptographic Implementations
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Santiago Zanella-Béguelin, Nikhil Swamy
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 | January 2014
To appear
-
Increasing Human-Tool Interaction via the Web
Thomas Ball, Jonathan "Peli" de Halleux, Daan Leijen, Nikhil Swamy
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering | June 2013
11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering
-
Verifying Higher-order Programs with the Dijkstra Monad
Nikhil Swamy, Juan Chen, Ben Livshits
ACM Programming Language Design and Implementation (PLDI) 2013 | June 2013
ACM Programming Language Design and Implementation (PLDI) 2013
-
Fully Abstract Compilation to JavaScript
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, Ben Livshits
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013 | January 2013
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013
-
Probabilistic Relational Verification for Cryptographic Implementations
Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
November 2012
-
Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
To appear
-
Secure Distributed Programming with Value-dependent Types
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011) | September 2011
-
Lightweight Monadic Programming in ML
Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks
Proceedings of the International Conference of Functional Programming (ICFP'11) | July 2011
Proceedings of the International Conference of Functional Programming (ICFP'11)
-
Modular Protections against Non-Control Data Attacks
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Ben Zorn
IEEE Symposium on Computer Security Foundations | June 2011
-
Verified Security for Browser Extensions
Arjun Guha, Matthew Fredrikson, Benjamin Livshits, Nikhil Swamy, Ben Livshits
Proceedings of the IEEE Symposium on Security and Privacy (Oakland) | May 2011
-
Verifying Stateful Programs with Substructural State and Hoare Types
Juan Chen, Nikhil Swamy
Programming Language meets Program Verification (PLPV 2011) | January 2011
-
Type-preserving compilation for end-to-end verification of security enforcement
Juan Chen, Nikhil Swamy, Ravi Chugh
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
-
Verified Implementations of the Information Card Federated Identity-Management Protocol
Karthik Bhargavan, Cédric Fournet, Andy Gordon, Nikhil Swamy
ASIACCS '08 Proceedings of the 2008 ACM symposium on Information, computer and communications security | March 2008
ISBN: 978-1-59593-979-1
-
-
-
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
MSR-TR-2018-33 | July 2018
作者：Microsoft
-
Safe & Efficient Gradual Typing for TypeScript
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, Panagiotis Vekris
MSR-TR-2014-99 | July 2014
-
DKAL*: Constructing Executable Specifications of Authorization Protocols
Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
MSR-TR-2012-24 | March 2013
International Symposium on Engineering Secure Software and Systems (ESSOS 13)
-
Verification Condition Generation with the Dijkstra State Monad
Cole Schlesinger, Nikhil Swamy
MSR-TR-2012-45 | April 2012
-
Monadic Reï¬nement Types for Verifying JavaScript Programs
Nikhil Swamy, Joel Weinberger, Juan Chen, Ben Livshits, Cole Schlesinger
MSR-TR-2012-37 | March 2012
-
Lightweight Monadic Programming in ML
Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks
MSR-TR-2011-39 | March 2011
-
Secure Distributed Programming with Value-Dependent Types
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, Jean Yang
MSR-TR-2011-37 | March 2011
This is an extended version of the conference paper (ICFP '11) with the same title. A final version of this full technical report is forthcoming.
-
Modular Protections against Non-Control Data Attacks
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Ben Zorn
MSR-TR-2010-158 | November 2010
-
Verified Security for Browser Extensions
Nikhil Swamy, Benjamin Livshits, Arjun Guha, Matthew Fredrikson, Ben Livshits
MSR-TR-2010-157 | November 2010
-
Verified Stateful Programs with Substructural State and Hoare Types
Juan Chen, Nikhil Swamy
MSR-TR-2010-95 | July 2010
-
Enforcing Stateful Authorization and Information Flow Policies in Fine
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-164 | March 2010
ESOP 2010: 19th European Symposium on Programming
-
End-to-end Verification of Security Enforcement is Fine (Extended version)
Nikhil Swamy, Juan Chen, Ravi Chugh
MSR-TR-2009-98 | August 2009
-
Collaborative End-to-end Enforcement of Security Policies in Distributed Systems
MSR-TR-2009-72 | June 2009
-
A Theory of Typed Coercions and its Applications
Nikhil Swamy, Michael Hicks, Gavin Bierman
MSR-TR-2009-69 | June 2009
SPIE Astronomy Telescopes and Instruments
-