Filter by type:

Sort by year:

Verus: A Practical Foundation for Systems Verification

Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, and Bryan Parno
Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), November, 2024
Conference
@inproceedings{verus-sys,
  author    = {Lattuada, Andrea and Hance, Travis and Bosamiya, Jay and Brun, Matthias and Cho, Chanhee and LeBlanc, Hayley and Srinivasan, Pranav and Achermann, Reto and Chajed, Tej and Hawblitzel, Chris and Howell, Jon and Lorch, Jay and Padon, Oded and Parno, Bryan},
  booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
  code      = {https://github.com/verus-lang/verus},
  month     = {November},
  title     = {Verus: A Practical Foundation for Systems Verification},
  year      = {2024}
}

FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions

Zhengyao Lin, Joshua Gancher, and Bryan Parno
Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), October, 2024
Conference
@inproceedings{flowcert,
  author    = {Lin, Zhengyao and Gancher, Joshua and Parno, Bryan},
  booktitle = {Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
  month     = {October},
  title     = {FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions},
  year      = {2024}
}

Context Pruning for More Robust SMT-based Program Verification

Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule, and Bryan Parno
Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference, October, 2024
Conference
@inproceedings{shake,
  author    = {Zhou, Yi and Bosamiya, Jay and Li, Jessica and Heule, Marijn and Parno, Bryan},
  booktitle = {Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference},
  month     = {October},
  title     = {Context Pruning for More Robust SMT-based Program Verification},
  year      = {2024}
}

Distributed Cryptography as a Service

Elisaweta Masserova
Carnegie Mellon University, September, 2024
PhD Thesis
@phdthesis{masserova-thesis,
  author    = {Masserova, Elisaweta},
  month     = {September},
  school    = {Carnegie Mellon University},
  title     = {Distributed Cryptography as a Service},
  year      = {2024}
}

Verifying Concurrent Systems Code

Travis Hance
Carnegie Mellon University, August, 2024
PhD Thesis
@phdthesis{hance-thesis,
  author    = {Hance, Travis},
  month     = {August},
  school    = {Carnegie Mellon University},
  title     = {Verifying Concurrent Systems Code},
  year      = {2024}
}

HyperNova: Recursive Arguments for Customizable Constraint Systems

Abhiram Kothapalli and Srinath Setty
Proceedings of the IACR CRYPTO Conference, August, 2024
Conference
@inproceedings{hypernova,
  author    = {Kothapalli, Abhiram and Setty, Srinath},
  booktitle = {Proceedings of the IACR CRYPTO Conference},
  month     = {August},
  title     = {HyperNova: Recursive Arguments for Customizable Constraint Systems},
  year      = {2024}
}

Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs

Tony Nuda Zhang, Travis Hance, Tej Chajed, Manos Kapritsos, and Bryan Parno
Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July, 2024
Conference
@inproceedings{kondo,
  author    = {Zhang, Tony Nuda and Hance, Travis and Chajed, Tej and Kapritsos, Manos and Parno, Bryan},
  booktitle = {Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)},
  code      = {https://github.com/GLaDOS-Michigan/Kondo-Artifact-OSDI24},
  month     = {July},
  title     = {Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs},
  year      = {2024}
}

A Framework for Debugging Automated Program Verification Proofs via Proof Actions

Chanhee Cho, Yi Zhou, Jay Bosamiya, and Bryan Parno
Proceedings of the Conference on Computer Aided Verification (CAV), July, 2024
Distinguished Paper Award
Conference Award
@inproceedings{proof-plumber,
  author    = {Cho, Chanhee and Zhou, Yi and Bosamiya, Jay and Parno, Bryan},
  booktitle = {Proceedings of the Conference on Computer Aided Verification (CAV)},
  code      = {https://github.com/verus-lang/verus-analyzer},
  month     = {July},
  title     = {A Framework for Debugging Automated Program Verification Proofs via Proof Actions},
  year      = {2024}
}

A Theory of Composition for Proofs of Knowledge

Abhiram Kothapalli
Carnegie Mellon University, May, 2024
PhD Thesis
@phdthesis{kothapalli-thesis,
  author    = {Kothapalli, Abhiram},
  month     = {May},
  school    = {Carnegie Mellon University},
  title     = {A Theory of Composition for Proofs of Knowledge},
  year      = {2024}
}

A Principled Approach Towards Unapologetic Security

Jay Bosamiya
Carnegie Mellon University, May, 2024
PhD Thesis
@phdthesis{bosamiya-thesis,
  author    = {Bosamiya, Jay},
  month     = {May},
  school    = {Carnegie Mellon University},
  title     = {A Principled Approach Towards Unapologetic Security},
  year      = {2024}
}

Improved YOSO Randomness Generation with Worst-Case Corruptions

Chen-Da Liu-Zhang, Elisaweta Masserova, João Ribeiro, Pratik Soni, and Sri AravindaKrishnan Thyagarajan
Proceedings of the Financial Cryptography and Data Security Conference (FC), March, 2024
Conference
@inproceedings{yoso-rnd,
  author    = {Liu-Zhang, Chen-Da and Masserova, Elisaweta and Ribeiro, João and Soni, Pratik and Thyagarajan, Sri AravindaKrishnan},
  booktitle = {Proceedings of the Financial Cryptography and Data Security Conference (FC)},
  month     = {March},
  title     = {Improved {YOSO} Randomness Generation with Worst-Case Corruptions},
  year      = {2024}
}

No Root Store Left Behind

James Larisch, Waqar Aqeel, Taejoong Chung, Eddie Kohler, Dave Levin, Bruce Maggs, Bryan Parno, and Christo Wilson
Proceedings of the ACM Workshop on Hot Topics in Networks (HotNets), November, 2023
Workshop
@inproceedings{root-stores,
  author    = {Larisch, James and Aqeel, Waqar and Chung, Taejoong and Kohler, Eddie and Levin, Dave and Maggs, Bruce and Parno, Bryan and Wilson, Christo},
  booktitle = {Proceedings of the ACM Workshop on Hot Topics in Networks (HotNets)},
  month     = {November},
  title     = {No Root Store Left Behind},
  year      = {2023}
}

Galápagos: Developing Verified Low-Level Cryptography on Heterogeneous Hardware

Yi Zhou, Sydney Gibson, Sarah Cai, Menucha Winchell, and Bryan Parno
Proceedings of the ACM Conference on Computer and Communications Security (CCS), November, 2023
Conference
@inproceedings{galapagos,
  author    = {Zhou, Yi and Gibson, Sydney and Cai, Sarah and Winchell, Menucha and Parno, Bryan},
  booktitle = {Proceedings of the ACM Conference on Computer and Communications Security (CCS)},
  code      = {https://github.com/secure-foundations/veri-titan},
  month     = {November},
  title     = {Galápagos: Developing Verified Low-Level Cryptography on Heterogeneous Hardware},
  year      = {2023}
}

Leaf: Modularity for Temporary Sharing in Separation Logic

Travis Hance, Jon Howell, Oded Padon, and Bryan Parno
Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), October, 2023
Conference
@inproceedings{leaf,
  author    = {Hance, Travis and Howell, Jon and Padon, Oded and Parno, Bryan},
  booktitle = {Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
  code      = {https://github.com/secure-foundations/leaf},
  month     = {October},
  title     = {Leaf: Modularity for Temporary Sharing in Separation Logic},
  year      = {2023}
}

Mariposa: Measuring SMT Instability in Automated Program Verification

Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, and Bryan Parno
Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference, October, 2023
Full version available as a CMU technical report.
Conference
@inproceedings{mariposa,
  author    = {Zhou, Yi and Bosamiya, Jay and Takashima, Yoshiki and Li, Jessica and Heule, Marijn and Parno, Bryan},
  booktitle = {Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference},
  code      = {https://github.com/secure-foundations/mariposa},
  month     = {October},
  title     = {Mariposa: Measuring {SMT} Instability in Automated Program Verification},
  year      = {2023}
}

Verus: Verifying Rust Programs using Linear Ghost Types

Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel
Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), October, 2023
Conference
@inproceedings{verus-ghost,
  author    = {Lattuada, Andrea and Hance, Travis and Cho, Chanhee and Brun, Matthias and Subasinghe, Isitha and Zhou, Yi and Howell, Jon and Parno, Bryan and Hawblitzel, Chris},
  booktitle = {Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
  code      = {https://github.com/verus-lang/verus},
  month     = {October},
  title     = {Verus: Verifying {Rust} Programs using Linear Ghost Types},
  year      = {2023}
}

Algebraic Reductions of Knowledge

Abhiram Kothapalli and Bryan Parno
Proceedings of the IACR CRYPTO Conference, August, 2023
Full version available as Cryptology ePrint Archive, Report 2022/009, January, 2022
Conference
@inproceedings{roks,
  author    = {Kothapalli, Abhiram and Parno, Bryan},
  booktitle = {Proceedings of the IACR CRYPTO Conference},
  month     = {August},
  title     = {Algebraic Reductions of Knowledge},
  year      = {2023}
}

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems

Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno
Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July, 2023
Conference
@inproceedings{ironsync,
  author    = {Hance, Travis and Zhou, Yi and Lattuada, Andrea and Achermann, Reto and Conway, Alex and Stutsman, Ryan and Zellweger, Gerd and Hawblitzel, Chris and Howell, Jon and Parno, Bryan},
  booktitle = {Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)},
  code      = {https://github.com/secure-foundations/ironsync-osdi2023},
  month     = {July},
  title     = {Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems},
  year      = {2023}
}

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System

Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, and Bryan Parno
Proceedings of the IEEE Symposium on Security and Privacy, May, 2023
Conference
@inproceedings{owl,
  author    = {Gancher, Joshua and Gibson, Sydney and Singh, Pratap and Dharanikota, Samvid and Parno, Bryan},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  code      = {https://github.com/secure-foundations/owl},
  month     = {May},
  title     = {Owl: Compositional Verification of Security Protocols via an Information-Flow Type System},
  year      = {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, and Ravi Ramamurthy
Proceedings of the ACM Conference on Certified Programs and Proofs (CPP), January, 2023
Conference
@inproceedings{fastver2,
  author    = {Arasu, Arvind and Ramananandro, Tahina and Rastogi, Aseem and Swamy, Nikhil and Fromherz, Aymeric and Hietala, Kesha and Parno, Bryan and Ramamurthy, Ravi},
  booktitle = {Proceedings of the ACM Conference on Certified Programs and Proofs (CPP)},
  month     = {January},
  title     = {{FastVer2}: A Provably Correct Monitor for Concurrent, Key-Value Stores},
  year      = {2023}
}

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan
Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), January, 2023
Conference
@inproceedings{mswasm,
  author    = {Michael, Alexandra E. and Gollamudi, Anitha and Bosamiya, Jay and Johnson, Evan and Denlinger, Aidan and Disselkoen, Craig and Watt, Conrad and Parno, Bryan and Patrignani, Marco and Vassena, Marco and Stefan, Deian},
  booktitle = {Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)},
  code      = {https://github.com/PLSysSec/ms-wasm/tree/main},
  month     = {January},
  title     = {{MSWasm}: Soundly Enforcing Memory-Safe Execution of Unsafe Code},
  year      = {2023}
}

Linear Types for Large-Scale Systems Verification

Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), December, 2022
Distinguished Paper Award
Conference Award
@inproceedings{linear-dafny,
  author    = {Li, Jialin and Lattuada, Andrea and Zhou, Yi and Cameron, Jonathan and Howell, Jon and Parno, Bryan and Hawblitzel, Chris},
  booktitle = {Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
  code      = {https://github.com/jialin-li/linear-veribetrkv-artifact},
  month     = {December},
  title     = {Linear Types for Large-Scale Systems Verification},
  year      = {2022}
}

Degradation Attacks on Certifiably Robust Neural Networks

Klas Leino, Chi Zhang, Ravi Mangal, Matt Fredrikson, Bryan Parno, and Corina Pasareanu
Transactions of Machine Learning Research, Vol. 1(1), November, 2022
Journal
@article{degradation-attacks,
  author    = {Leino, Klas and Zhang, Chi and Mangal, Ravi and Fredrikson, Matt and Parno, Bryan and Pasareanu, Corina},
  code      = {https://github.com/ravimangal/degradation-attacks},
  journal   = {Transactions of Machine Learning Research},
  month     = {November},
  number    = {1},
  title     = {Degradation Attacks on Certifiably Robust Neural Networks},
  volume    = {1},
  xurl      = {https://openreview.net/forum?id=P0XO5ZE98j},
  year      = {2022}
}

Hammurabi: A Framework for Pluggable, Logic-based X.509 Certificate Validation Policies

James Larisch, Waqar Aqeel, Christo Wilson, Alan Mislove, Taejoong Chung, Dave Levin, Bryan Parno, and Bruce Maggs
Proceedings of the ACM Conference on Computer and Communications Security (CCS), November, 2022
Best Paper Honorable Mention
Conference Award
@inproceedings{hammurabi,
  author    = {Larisch, James and Aqeel, Waqar and Wilson, Christo and Mislove, Alan and Chung, Taejoong and Levin, Dave and Parno, Bryan and Maggs, Bruce},
  booktitle = {Proceedings of the ACM Conference on Computer and Communications Security (CCS)},
  code      = {https://github.com/semaj/hammurabi},
  month     = {November},
  title     = {Hammurabi: A Framework for Pluggable, Logic-based {X.509} Certificate Validation Policies},
  year      = {2022}
}

Self-correcting Neural Networks for Safe Classification

Klas Leino, Aymeric Fromherz, Ravi Mangal, Matt Fredrikson, Bryan Parno, and Corina Pasareanu
Proceedings of the Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), August, 2022
Workshop
@inproceedings{self-correcting-ml,
  author    = {Leino, Klas and Fromherz, Aymeric and Mangal, Ravi and Fredrikson, Matt and Parno, Bryan and Pasareanu, Corina},
  booktitle = {Proceedings of the Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS)},
  month     = {August},
  title     = {Self-correcting Neural Networks for Safe Classification},
  year      = {2022}
}

Nova: Recursive Zero-Knowledge Arguments from Folding Schemes

Abhiram Kothapalli, Srinath Setty, and Ioanna Tzialla
Proceedings of the IACR CRYPTO Conference, August, 2022
Conference
@inproceedings{nova,
  author    = {Kothapalli, Abhiram and Setty, Srinath and Tzialla, Ioanna},
  booktitle = {Proceedings of the IACR CRYPTO Conference},
  code      = {https://github.com/microsoft/Nova},
  month     = {August},
  title     = {Nova: Recursive Zero-Knowledge Arguments from Folding Schemes},
  year      = {2022}
}

Provably-Safe Multilingual Software Sandboxing using WebAssembly

Jay Bosamiya, Wen Shih Lim, and Bryan Parno
Proceedings of the USENIX Security Symposium, August, 2022
Distinguished Paper Award and the Second Prize in the 2022 USENIX Security Internet Defense Prize Competition
Conference Award
@inproceedings{wasm-sandboxing,
  author    = {Bosamiya, Jay and Lim, Wen Shih and Parno, Bryan},
  booktitle = {Proceedings of the USENIX Security Symposium},
  code      = {https://github.com/secure-foundations/provably-safe-sandboxing-wasm-usenix22},
  month     = {August},
  title     = {Provably-Safe Multilingual Software Sandboxing using {WebAssembly}},
  year      = {2022}
}

Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility

Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Haojun Ma, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao
ACM Transactions on Programming Languages and Systems, Vol. 44(2), June, 2022
Journal
@article{armada-toplas,
  author    = {Lorch, Jacob R. and Chen, Yixuan and Kapritsos, Manos and Ma, Haojun and Parno, Bryan and Qadeer, Shaz and Sharma, Upamanyu and Wilcox, James R. and Zhao, Xueyuan},
  code      = {https://github.com/microsoft/armada},
  journal   = {ACM Transactions on Programming Languages and Systems},
  month     = {June},
  number    = {2},
  title     = {Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility},
  volume    = {44},
  year      = {2022}
}

Storing and Retrieving Secrets on a Blockchain

Vipul Goyal, Abhiram Kothapalli, Elisaweta Masserova, Bryan Parno, and Yifan Song
Proceedings of the IACR Conference on Practice and Theory of Public-Key Cryptography (PKC), March, 2022
Conference
@inproceedings{eweb,
  author    = {Goyal, Vipul and Kothapalli, Abhiram and Masserova, Elisaweta and Parno, Bryan and Song, Yifan},
  booktitle = {Proceedings of the IACR Conference on Practice and Theory of Public-Key Cryptography (PKC)},
  code      = {https://github.com/abhiramkothapalli/extweexperiments},
  month     = {March},
  title     = {Storing and Retrieving Secrets on a Blockchain},
  year      = {2022}
}

Transparency Dictionaries with Succinct Proofs of Correct Operation

Ioanna Tzialla, Abhiram Kothapalli, Bryan Parno, and Srinath Setty
Proceedings of the ISOC Network and Distributed System Security Symposium (NDSS), February, 2022
Conference
@inproceedings{verdict,
  author    = {Tzialla, Ioanna and Kothapalli, Abhiram and Parno, Bryan and Setty, Srinath},
  booktitle = {Proceedings of the ISOC Network and Distributed System Security Symposium (NDSS)},
  month     = {February},
  title     = {Transparency Dictionaries with Succinct Proofs of Correct Operation},
  year      = {2022}
}

A Proof-Oriented Approach to Low-Level, High-Assurance Programming

Aymeric Fromherz
Carnegie Mellon University, December, 2021
A.G. Milnes Award and the ACM SIGSAC Dissertation Award
PhD Thesis Award
@phdthesis{fromherz-thesis,
  author    = {Fromherz, Aymeric},
  month     = {December},
  school    = {Carnegie Mellon University},
  title     = {A Proof-Oriented Approach to Low-Level, High-Assurance Programming},
  year      = {2021}
}

Blockchains Enable Non-Interactive MPC

Vipul Goyal, Elisaweta Masserova, Bryan Parno, and Yifan Song
Proceedings of the IACR Theory of Cryptography Conference (TCC), November, 2021
Conference
@inproceedings{one-round-mpc,
  author    = {Goyal, Vipul and Masserova, Elisaweta and Parno, Bryan and Song, Yifan},
  booktitle = {Proceedings of the IACR Theory of Cryptography Conference (TCC)},
  month     = {November},
  title     = {Blockchains Enable Non-Interactive {MPC}},
  year      = {2021}
}

Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic

Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martinez, Denis Merigoux, and Tahina Ramananandro
Proceedings of the ACM International Conference on Functional Programming (ICFP), August, 2021
Conference
@inproceedings{steel,
  author    = {Fromherz, Aymeric and Rastogi, Aseem and Swamy, Nikhil and Gibson, Sydney and Martinez, Guido and Merigoux, Denis and Ramananandro, Tahina},
  booktitle = {Proceedings of the ACM International Conference on Functional Programming (ICFP)},
  month     = {August},
  title     = {Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic},
  year      = {2021}
}

Fast Geometric Projections for Local Robustness Certification

Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, and Corina Pasareanu
Proceedings of the International Conference on Learning Representations (ICLR), Spotlight Presentation, May, 2021
Conference
@inproceedings{fgp,
  author    = {Fromherz, Aymeric and Leino, Klas and Fredrikson, Matt and Parno, Bryan and Pasareanu, Corina},
  booktitle = {Proceedings of the International Conference on Learning Representations (ICLR), Spotlight Presentation},
  code      = {https://github.com/klasleino/fast-geometric-projections},
  month     = {May},
  title     = {Fast Geometric Projections for Local Robustness Certification},
  year      = {2021}
}

SoK: Computer-Aided Cryptography

Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno
Proceedings of the IEEE Symposium on Security and Privacy, May, 2021
Conference
@inproceedings{cac-sok,
  author    = {Barbosa, Manuel and Barthe, Gilles and Bhargavan, Karthik and Blanchet, Bruno and Cremers, Cas and Liao, Kevin and Parno, Bryan},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  month     = {May},
  title     = {{SoK}: Computer-Aided Cryptography},
  year      = {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, and Yi Zhou
Proceedings of the IEEE Symposium on Security and Privacy, May, 2021
Conference
@inproceedings{quic-record,
  author    = {Delignat-Lavaud, Antoine and Fournet, Cédric and Parno, Bryan and Protzenko, Jonathan and Ramananandro, Tahina and Bosamiya, Jay and Lallemand, Joseph and Rakotonirina, Itsaka and Zhou, Yi},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  code      = {https://github.com/secure-foundations/everquic-dafny},
  month     = {May},
  title     = {A Security Model and Fully Verified Implementation for the {IETF QUIC} Record Layer},
  year      = {2021}
}

HerQules: Securing Programs via Hardware-Enforced Message Queues

Daming Chen, Wen Shih Lim, Mohammad Bakhshalipour, Phillip Gibbons, James C. Hoe, and Bryan Parno
Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April, 2021
Conference
@inproceedings{herqules,
  author    = {Chen, Daming and Lim, Wen Shih and Bakhshalipour, Mohammad and Gibbons, Phillip and Hoe, James C. and Parno, Bryan},
  booktitle = {Proceedings of the ACM Conference on Architectural Support for  Programming Languages and Operating Systems (ASPLOS)},
  code      = {https://github.com/secure-foundations/herqules},
  month     = {April},
  title     = {{HerQules}: Securing Programs via Hardware-Enforced Message Queues},
  year      = {2021}
}

Finding Invariants of Distributed Systems: It's a Small (Enough) World After All

Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno
Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), April, 2021
Conference
@inproceedings{swiss,
  author    = {Hance, Travis and Heule, Marijn and Martins, Ruben and Parno, Bryan},
  booktitle = {Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)},
  code      = {https://github.com/secure-foundations/SWISS},
  month     = {April},
  title     = {Finding Invariants of Distributed Systems: It's a Small (Enough) World After All},
  year      = {2021}
}

Don't Yank My Chain: Auditable NF Service Chaining

Guyue Liu, Hugo Sadok, Anne Kohlbrenner, Bryan Parno, Vyas Sekar, and Justine Sherry
Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), April, 2021
Conference
@inproceedings{auditbox,
  author    = {Liu, Guyue and Sadok, Hugo and Kohlbrenner, Anne and Parno, Bryan and Sekar, Vyas and Sherry, Justine},
  booktitle = {Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)},
  month     = {April},
  title     = {Don't Yank My Chain: Auditable {NF} Service Chaining},
  year      = {2021}
}

CAPS: Smoothly Transitioning to a More Resilient Web PKI

Stephanos Matsumoto, Jay Bosamiya, Yucheng Dai, Paul van Oorschot, and Bryan Parno
Proceedings of the ACSA Annual Computer Security Applications Conference (ACSAC), December, 2020
Conference
@inproceedings{caps,
  author    = {Matsumoto, Stephanos and Bosamiya, Jay and Dai, Yucheng and van Oorschot, Paul and Parno, Bryan},
  booktitle = {Proceedings of the ACSA Annual Computer Security Applications Conference (ACSAC)},
  code      = {https://github.com/syclops/caps},
  month     = {December},
  title     = {{CAPS}: Smoothly Transitioning to a More Resilient Web {PKI}},
  year      = {2020}
}

Talek: Private Group Messaging with Hidden Access Patterns

Raymond Cheng, William Scott, Elisaweta Masserova, Irene Zhang, Vipul Goyal, Thomas Anderson, Arvind Krishnamurthy, and Bryan Parno
Proceedings of the ACSA Annual Computer Security Applications Conference (ACSAC), December, 2020
Conference
@inproceedings{talek,
  author    = {Cheng, Raymond and Scott, William and Masserova, Elisaweta and Zhang, Irene and Goyal, Vipul and Anderson, Thomas and Krishnamurthy, Arvind and Parno, Bryan},
  booktitle = {Proceedings of the ACSA Annual Computer Security Applications Conference (ACSAC)},
  month     = {December},
  title     = {Talek: Private Group Messaging with Hidden Access Patterns},
  year      = {2020}
}

Storage Systems are Distributed Systems (So Verify Them That Way!)

Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno
Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), November, 2020
Conference
@inproceedings{veribetrkv,
  author    = {Hance, Travis and Lattuada, Andrea and Hawblitzel, Chris and Howell, Jon and Johnson, Rob and Parno, Bryan},
  booktitle = {Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)},
  code      = {https://github.com/secure-foundations/veribetrkv-osdi2020},
  month     = {November},
  title     = {Storage Systems are Distributed Systems (So Verify Them That Way!)},
  year      = {2020}
}

HACL×N: Verified Generic SIMD Crypto (For All Your Favorite Platforms)

Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, and Santiago Zanella-Béguelin
Proceedings of the ACM Conference on Computer and Communications Security (CCS), October, 2020
Conference
@inproceedings{hacln,
  author    = {Polubelova, Marina and Bhargavan, Karthikeyan and Protzenko, Jonathan and Beurdouche, Benjamin and Fromherz, Aymeric and Kulatova, Natalia and Zanella-Béguelin, Santiago},
  booktitle = {Proceedings of the ACM Conference on Computer and Communications Security (CCS)},
  month     = {October},
  title     = {{HACL×N}: Verified Generic {SIMD} Crypto (For All Your Favorite Platforms)},
  year      = {2020}
}

SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs

Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martinez
Proceedings of the ACM International Conference on Functional Programming (ICFP), August, 2020
Conference
@inproceedings{steelcore,
  author    = {Swamy, Nikhil and Rastogi, Aseem and Fromherz, Aymeric and Merigoux, Denis and Ahman, Danel and Martinez, Guido},
  booktitle = {Proceedings of the ACM International Conference on Functional Programming (ICFP)},
  month     = {August},
  title     = {{SteelCore}: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs},
  year      = {2020}
}

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language

Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, and Chris Hawblitzel
In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), July, 2020
Conference
@inproceedings{transformers,
  author    = {Bosamiya, Jay and Gibson, Sydney and Li, Yao and Parno, Bryan and Hawblitzel, Chris},
  booktitle = {In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE)},
  month     = {July},
  title     = {Verified Transformations and {Hoare} Logic: Beautiful Proofs for Ugly Assembly Language},
  year      = {2020}
}

Armada: Low-Effort Verification of High-Performance Concurrent Programs

Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao
Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), June, 2020
Distinguished Paper Award
Conference Award
@inproceedings{armada,
  author    = {Lorch, Jacob R. and Chen, Yixuan and Kapritsos, Manos and Parno, Bryan and Qadeer, Shaz and Sharma, Upamanyu and Wilcox, James R. and Zhao, Xueyuan},
  booktitle = {Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI)},
  code      = {https://github.com/microsoft/armada},
  month     = {June},
  title     = {Armada: Low-Effort Verification of High-Performance Concurrent Programs},
  year      = {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 Wintersteiger, and Santiago Zanella-Beguelin
Proceedings of the IEEE Symposium on Security and Privacy (Oakland), May, 2020
Conference
@inproceedings{evercrypt,
  author    = {Protzenko, Jonathan and Parno, Bryan and Fromherz, Aymeric and Hawblitzel, Chris and Polubelova, Marina and Bhargavan, Karthikeyan and Beurdouche, Benjamin and Choi, Joonwon and Delignat-Lavaud, Antoine and Fournet, Cédric and Kulatova, Natalia and Ramananandro, Tahina and Rastogi, Aseem and Swamy, Nikhil and Wintersteiger, Christoph and Zanella-Beguelin, Santiago},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy (Oakland)},
  code      = {https://github.com/project-everest/hacl-star/tree/master/providers/evercrypt},
  month     = {May},
  title     = {{EverCrypt}: A Fast, Verified, Cross-Platform Cryptographic Provider},
  year      = {2020}
}

Talek: Private Group Messaging with Hidden Access Patterns

Raymond Cheng, William Scott, Elisaweta Masserova, Irene Zhang, Vipul Goyal, Thomas Anderson, Arvind Krishnamurthy, and Bryan Parno
ePrint 2020/066, January, 2020
Tech Report
@techreport{talek-tr,
  author      = {Cheng, Raymond and Scott, William and Masserova, Elisaweta and Zhang, Irene and Goyal, Vipul and Anderson, Thomas and Krishnamurthy, Arvind and Parno, Bryan},
  institution = {ePrint},
  month       = {January},
  number      = {2020/066},
  title       = {Talek: Private Group Messaging with Hidden Access Patterns},
  year        = {2020}
}

Effective and Practical Improvements to the Web Public-Key Infrastructure

Stephanos Y. Matsumoto
Carnegie Mellon University, May, 2019
PhD Thesis
@phdthesis{masutmoto-thesis,
  author    = {Matsumoto, Stephanos Y.},
  month     = {May},
  school    = {Carnegie Mellon University},
  title     = {Effective and Practical Improvements to the Web Public-Key Infrastructure},
  year      = {2019}
}

Symbolic Pathfinder for SV-COMP (Competition Contribution)

Yannic Noller, Corina S. Păsăreanu, Aymeric Fromherz, Xuan-Bach D. Le, and Willem Visser
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April, 2019
Conference
@inproceedings{pathfinder,
  author    = {Noller, Yannic and Păsăreanu, Corina S. and Fromherz, Aymeric and Le, Xuan-Bach D. and Visser, Willem},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  month     = {April},
  title     = {Symbolic Pathfinder for {SV-COMP} (Competition Contribution)},
  year      = {2019}
}

A Verified, Efficient Embedding of a Verifiable Assembly Language

Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), January, 2019
Conference
@inproceedings{vale-popl,
  author    = {Fromherz, Aymeric and Giannarakis, Nick and Hawblitzel, Chris and Parno, Bryan and Rastogi, Aseem and Swamy, Nikhil},
  booktitle = {Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)},
  code      = {https://github.com/project-everest/vale},
  month     = {January},
  title     = {A Verified, Efficient Embedding of a Verifiable Assembly Language},
  year      = {2019}
}

Komodo: Using verification to disentangle secure-enclave hardware from software

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno
Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October, 2017
Conference
@inproceedings{komodo,
  author    = {Ferraiuolo, Andrew and Baumann, Andrew and Hawblitzel, Chris and Parno, Bryan},
  booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
  code      = {https://github.com/Microsoft/Komodo},
  month     = {October},
  title     = {Komodo: Using verification to disentangle secure-enclave hardware from software},
  year      = {2017}
}

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, and Laure Thompson
Proceedings of the USENIX Security Symposium, August, 2017
Distinguished Paper Award
Conference Award
@inproceedings{vale,
  author    = {Bond, Barry and Hawblitzel, Chris and Kapritsos, Manos and Leino, K. Rustan M. and Lorch, Jacob R. and Parno, Bryan and Rane, Ashay and Setty, Srinath and Thompson, Laure},
  booktitle = {Proceedings of the USENIX Security Symposium},
  code      = {https://github.com/project-everest/vale},
  month     = {August},
  title     = {Vale: Verifying High-Performance Cryptographic Assembly Code},
  year      = {2017}
}

IronFleet: Proving Practical Distributed Systems Correct

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill
Communications of the ACM, Vol. 60(7), July, 2017
Research Highlight
Journal Award
@article{ironfleetCACM,
  author    = {Hawblitzel, Chris and Howell, Jon and Kapritsos, Manos and Lorch, Jacob R. and Parno, Bryan and Roberts, Michael L. and Setty, Srinath and Zill, Brian},
  code      = {https://github.com/Microsoft/Ironclad/blob/master/ironfleet/README.md},
  journal   = {Communications of the ACM},
  month     = {July},
  number    = {7},
  title     = {{IronFleet}: Proving Practical Distributed Systems Correct},
  volume    = {60},
  year      = {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-Beguelin, and Jean-Karim Zinzindohoué
Summit on Advances in Programming Languages (SNAPL), May, 2017
Conference
@inproceedings{everest-snapl,
  author    = {Bhargavan, Karthikeyan and Bond, Barry and Delignat-Lavaud, Antoine and Fournet, Cédric and Hawblitzel, Chris and Hritcu, Catalin and Ishtiaq, Samin and Kohlweiss, Markulf and Leino, Rustan and Lorch, Jay and Maillard, Kenji and Pang, Jinyang and Parno, Bryan and Protzenko, Jonathan and Ramananandro, Tahina and Rane, Ashay and Rastogi, Aseem and Swamy, Nikhil and Thompson, Laure and Wang, Peng and Zanella-Beguelin, Santiago and Zinzindohoué, Jean-Karim},
  booktitle = {Summit on Advances in Programming Languages (SNAPL)},
  code      = {https://project-everest.github.io/},
  month     = {May},
  title     = {Everest: Towards a Verified, Drop-In Replacement of {HTTPS}},
  year      = {2017}
}

Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data

Dario Fiore, Cédric Fournet, Esha Ghosh, Markulf Kohlweiss, Olya Ohrimenko, and Bryan Parno
Proceedings of the ACM Conference on Computer and Communications Security (CCS), October, 2016
Full version on the Cryptology ePrint Archive, Report 2016/985
Conference
@inproceedings{hashArgue,
  author    = {Fiore, Dario and Fournet, Cédric and Ghosh, Esha and Kohlweiss, Markulf and Ohrimenko, Olya and Parno, Bryan},
  booktitle = {Proceedings of the ACM Conference on Computer and Communications Security (CCS)},
  month     = {October},
  title     = {Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data},
  year      = {2016}
}

Cinderella: Turning Shabby X.509 Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation

Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, and Bryan Parno
Proceedings of the IEEE Symposium on Security and Privacy (Oakland), May, 2016
Conference
@inproceedings{cinderella,
  author    = {Delignat-Lavaud, Antoine and Fournet, Cédric and Kohlweiss, Markulf and Parno, Bryan},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy (Oakland)},
  month     = {May},
  title     = {Cinderella: Turning Shabby {X.509} Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation},
  year      = {2016}
}

Pinocchio: Nearly Practical Verifiable Computation

Bryan Parno, Craig Gentry, Jon Howell, and Mariana Raykova
Communications of the ACM, Vol. 59(2), February, 2016
Research Highlight
Journal Award
@article{pinocchioCACM,
  author    = {Parno, Bryan and Gentry, Craig and Howell, Jon and Raykova, Mariana},
  code      = {https://github.com/secure-foundations/verifiable-computation/},
  journal   = {Communications of the ACM},
  month     = {February},
  number    = {2},
  title     = {Pinocchio: Nearly Practical Verifiable Computation},
  volume    = {59},
  year      = {2016}
}

IronFleet: Proving Practical Distributed Systems Correct

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill
Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October, 2015
Conference
@inproceedings{hawblitzel2015ironfleet,
  author    = {Hawblitzel, Chris and Howell, Jon and Kapritsos, Manos and Lorch, Jacob R. and Parno, Bryan and Roberts, Michael L. and Setty, Srinath and Zill, Brian},
  booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
  code      = {https://github.com/Microsoft/Ironclad/blob/master/ironfleet/README.md},
  month     = {October},
  title     = {{IronFleet}: Proving Practical Distributed Systems Correct},
  year      = {2015}
}

Geppetto: Versatile Verifiable Computation

Craig Costello, Cédric Fournet, Jon Howell, Markulf Kohlweiss, Benjamin Kreuter, Michael Naehrig, Bryan Parno, and Samee Zahur
Proceedings of the IEEE Symposium on Security and Privacy (Oakland), May, 2015
Conference
@inproceedings{costello2015geppetto,
  author    = {Costello, Craig and Fournet, Cédric and Howell, Jon and Kohlweiss, Markulf and Kreuter, Benjamin and Naehrig, Michael and Parno, Bryan and Zahur, Samee},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy (Oakland)},
  code      = {https://github.com/secure-foundations/verifiable-computation/},
  month     = {May},
  title     = {Geppetto: Versatile Verifiable Computation},
  year      = {2015}
}

A Note on the Unsoundness of vnTinyRAM's SNARK

Bryan Parno
ePrint 2015/437, May, 2015
Tech Report
@techreport{vnTinyRAMnote,
  author      = {Parno, Bryan},
  institution = {ePrint},
  month       = {May},
  number      = {2015/437},
  title       = {A Note on the Unsoundness of vnTinyRAM's SNARK},
  year        = {2015}
}

Network Adversary Attacks against Secure Encryption Schemes

Virgil D. Gligor, Bryan Parno, and Ji Sun Shin
IEICE Transactions on Communications, Vol. E98.B(2), February, 2015
Journal
@article{networkAdversary2015,
  author    = {Gligor, Virgil D. and Parno, Bryan and Shin, Ji Sun},
  journal   = {IEICE Transactions on Communications},
  month     = {February},
  number    = {2},
  title     = {Network Adversary Attacks against Secure Encryption Schemes},
  volume    = {E98.B},
  year      = {2015}
}

Ironclad Apps: End-to-End Security via Automated Full-System Verification

Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill
Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), October, 2014
Conference
@inproceedings{ironclad,
  author    = {Hawblitzel, Chris and Howell, Jon and Lorch, Jacob R. and Narayan, Arjun and Parno, Bryan and Zhang, Danfeng and Zill, Brian},
  booktitle = {Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)},
  code      = {https://github.com/Microsoft/Ironclad/blob/master/ironclad-apps/README.md},
  month     = {October},
  title     = {Ironclad {Apps}: End-to-End Security via Automated Full-System Verification},
  year      = {2014}
}

Missive: Fast Application Launch From an Untrusted Buffer Cache

Jon Howell, Jeremy Elson, Bryan Parno, and John R. Douceur
Proceedings of the USENIX Annual Technical Conference (ATC), June, 2014
Conference
@inproceedings{howell2013missive,
  author    = {Howell, Jon and Elson, Jeremy and Parno, Bryan and Douceur, John R.},
  booktitle = {Proceedings of the USENIX Annual Technical Conference (ATC)},
  month     = {June},
  title     = {Missive: Fast Application Launch From an Untrusted Buffer Cache},
  year      = {2014}
}

Permacoin: Repurposing Bitcoin Work for Data Preservation

Andrew Miller, Elaine Shi, Ari Juels, Bryan Parno, and Jonathan Katz
Proceedings of the IEEE Symposium on Security and Privacy, May, 2014
Conference
@inproceedings{permacoin2014,
  author    = {Miller, Andrew and Shi, Elaine and Juels, Ari and Parno, Bryan and Katz, Jonathan},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  month     = {May},
  title     = {Permacoin: Repurposing Bitcoin Work for Data Preservation},
  year      = {2014}
}

Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers

Bryan Parno
ACM, 2014
Book
@book{thesisBook,
  author    = {Parno, Bryan},
  publisher = {ACM},
  title     = {Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers},
  year      = {2014}
}

Pinocchio Coin: Building Zerocoin from a Succinct Pairing-based Proof System

George Danezis, Cédric Fournet, Markulf Kohlweiss, and Bryan Parno
ACM PETShop, November, 2013
Conference
@inproceedings{pinocchioCoin,
  author    = {Danezis, George and Fournet, Cédric and Kohlweiss, Markulf and Parno, Bryan},
  booktitle = {ACM PETShop},
  month     = {November},
  title     = {Pinocchio Coin: Building {Zerocoin} from a Succinct Pairing-based Proof System},
  year      = {2013}
}

How to Run POSIX Apps in a Minimal Picoprocess

Jon Howell, Bryan Parno, and John R. Douceur
Proceedings of the USENIX Annual Technical Conference (ATC), June, 2013
Conference
@inproceedings{howell2013posix,
  author    = {Howell, Jon and Parno, Bryan and Douceur, John R.},
  booktitle = {Proceedings of the USENIX Annual Technical Conference (ATC)},
  month     = {June},
  title     = {How to Run {POSIX} Apps in a Minimal Picoprocess},
  year      = {2013}
}

Pinocchio: Nearly Practical Verifiable Computation

Bryan Parno, Craig Gentry, Jon Howell, and Mariana Raykova
Proceedings of the IEEE Symposium on Security and Privacy, May, 2013
Best Paper Award, Test-of-Time Award
Conference Award
@inproceedings{parno2013pinocchio,
  author    = {Parno, Bryan and Gentry, Craig and Howell, Jon and Raykova, Mariana},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  code      = {https://github.com/secure-foundations/verifiable-computation/},
  month     = {May},
  title     = {Pinocchio: Nearly Practical Verifiable Computation},
  year      = {2013}
}

Quadratic Span Programs and Succinct NIZKs without PCPs

Rosario Gennaro, Craig Gentry, Bryan Parno, and Mariana Raykova
Proceedings of the IACR EuroCrypt Conference, May, 2013
Originally published as Cryptology ePrint Archive, Report 2012/215, April, 2012
Conference
@inproceedings{GGPR2013,
  author    = {Gennaro, Rosario and Gentry, Craig and Parno, Bryan and Raykova, Mariana},
  booktitle = {Proceedings of the IACR EuroCrypt Conference},
  month     = {May},
  title     = {Quadratic Span Programs and Succinct {NIZKs} without {PCPs}},
  year      = {2013}
}

Embassies: Radically Refactoring the Web

Jon Howell, Bryan Parno, and John R. Douceur
Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), April, 2013
Best Paper Award
Conference Award
@inproceedings{howell2013embassies,
  author    = {Howell, Jon and Parno, Bryan and Douceur, John R.},
  booktitle = {Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)},
  code      = {https://embassies.codeplex.com/},
  month     = {April},
  title     = {Embassies: Radically Refactoring the Web},
  year      = {2013}
}

Resolving the conflict between generality and plausibility in verified computation

Srinath Setty, Ben Braun, Victor Vu, Andrew J. Blumberg, Bryan Parno, and Michael Walfish
Proceedings of the ACM European Conference on Computer Systems (EuroSys), April, 2013
Conference
@inproceedings{setty13resolving,
  author    = {Setty, Srinath and Braun, Ben and Vu, Victor and Blumberg, Andrew J. and Parno, Bryan and Walfish, Michael},
  booktitle = {Proceedings of the ACM European Conference on Computer Systems (EuroSys)},
  month     = {April},
  title     = {Resolving the conflict between generality and plausibility in verified computation},
  year      = {2013}
}

Shroud: Enabling Private Access to Large-Scale Data in the Data Center

Jacob R. Lorch, Bryan Parno, James Mickens, Mariana Raykova, and Joshua Schiffman
Proceedings of the USENIX Conference on File and Storage Technologies (FAST), February, 2013
Conference
@inproceedings{shroud,
  author    = {Lorch, Jacob R. \ and Parno, Bryan and Mickens, James and Raykova, Mariana and Schiffman, Joshua},
  booktitle = {Proceedings of the USENIX Conference on File and Storage Technologies (FAST)},
  month     = {February},
  title     = {Shroud: Enabling Private Access to Large-Scale Data in the Data Center},
  year      = {2013}
}

The Web Interface Should Be Radically Refactored

John R. Douceur, Jon Howell, Bryan Parno, Michael Walfish, and Xi Xiong
Proceedings of the Workshop on Hot Topics in Networks (HotNets), November, 2012
Workshop
@inproceedings{refactored2012,
  author    = {Douceur, John R. and Howell, Jon and Parno, Bryan and Walfish, Michael and Xiong, Xi},
  booktitle = {Proceedings of the Workshop on Hot Topics in Networks (HotNets)},
  month     = {November},
  title     = {The Web Interface Should Be Radically Refactored},
  year      = {2012}
}

Using Trustworthy Host-Based Information in the Network

Bryan Parno, Zongwei Zhou, and Adrian Perrig
Proceedings of the Workshop on Scalable Trusted Computing (STC), October, 2012
Invited Paper
Workshop Award
@inproceedings{host2012,
  author    = {Parno, Bryan and Zhou, Zongwei and Perrig, Adrian},
  booktitle = {Proceedings of the Workshop on Scalable Trusted Computing (STC)},
  month     = {October},
  title     = {Using Trustworthy Host-Based Information in the Network},
  year      = {2012}
}

Lockdown: A Safe and Practical Environment for Security Applications

Amit Vasudevan, Bryan Parno, Ning Qu, Virgil D. Gligor, and Adrian Perrig
Proceedings of the Conference on Trust and Trustworthy Computing (TRUST), June, 2012
Conference
@inproceedings{lockdown,
  author    = {Vasudevan, Amit and Parno, Bryan and Qu, Ning and Gligor, Virgil D. and Perrig, Adrian},
  booktitle = {Proceedings of the Conference on Trust and Trustworthy Computing (TRUST)},
  month     = {June},
  title     = {Lockdown: A Safe and Practical Environment for Security Applications},
  year      = {2012}
}

Trust Extension for Commodity Computers

Bryan Parno
Communications of the ACM, Vol. 55(6), June, 2012
Journal
@article{thesisCACM,
  author    = {Parno, Bryan},
  journal   = {Communications of the ACM},
  month     = {June},
  number    = {6},
  title     = {Trust Extension for Commodity Computers},
  volume    = {55},
  year      = {2012}
}

User-Driven Access Control: Rethinking Permission Granting in Modern Operating Systems

Franziska Roesner, Tadayoshi Kohno, Alexander Moshchuk, Bryan Parno, Helen J. Wang, and Crispin Cowan
Proceedings of the IEEE Symposium on Security and Privacy (Oakland), May, 2012
Best Practical Paper Award
Conference Award
@inproceedings{roesner2012udac,
  author    = {Roesner, Franziska and Kohno, Tadayoshi and Moshchuk, Alexander and Parno, Bryan and Wang, Helen J. and Cowan, Crispin},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy (Oakland)},
  month     = {May},
  title     = {User-Driven Access Control: Rethinking Permission Granting in Modern Operating Systems},
  year      = {2012}
}

Monetary Forgery in the Digital Age: Will Physical-Digital Cash Be a Solution?

Nicolas Christin, Alessandro Acquisti, Bryan Parno, and Adrian Perrig
I/S: A Journal of Law and Policy for the Information Society, Vol. 7(2), 2012
Journal
@article{physicalDigitalCash2012,
  author    = {Christin, Nicolas and Acquisti, Alessandro and Parno, Bryan and Perrig, Adrian},
  journal   = {I/S: A Journal of Law and Policy for the Information Society},
  number    = {2},
  title     = {Monetary Forgery in the Digital Age: Will Physical-Digital Cash Be a Solution?},
  volume    = {7},
  year      = {2012}
}

How to Delegate and Verify in Public: Verifiable Computation from Attribute-based Encryption

Bryan Parno, Mariana Raykova, and Vinod Vaikuntanathan
IACR Theory of Cryptography Conference (TCC), 2012
Conference
@inproceedings{PRV12,
  author    = {Parno, Bryan and Raykova, Mariana and Vaikuntanathan, Vinod},
  booktitle = {IACR Theory of Cryptography Conference (TCC)},
  title     = {How to Delegate and Verify in Public: Verifiable Computation
from Attribute-based Encryption},
  year      = {2012}
}

Memoir: Practical State Continuity for Protected Modules

Bryan Parno, Jacob R. Lorch, John R. Douceur, James Mickens, and Jonathan M. McCune
Proceedings of the IEEE Symposium on Security and Privacy, May, 2011
Conference
@inproceedings{parno2011memoir,
  author    = {Parno, Bryan and Lorch, Jacob R. and Douceur, John R. and Mickens, James and McCune, Jonathan M.},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  day       = {22--25},
  location  = {Oakland, CA, USA},
  month     = {May},
  title     = {Memoir: Practical State Continuity for Protected Modules},
  year      = {2011}
}

Memoir---Formal Specs and Correctness Proofs

John R. Douceur, Jacob R. Lorch, Bryan Parno, James Mickens, and Jonathan M. McCune
Microsoft Research MSR-TR-2011-19, February, 2011
Tech Report
@techreport{memoirTR,
  author      = {Douceur, John R. and Lorch, Jacob R. \ and Parno, Bryan and Mickens, James and McCune, Jonathan M.},
  institution = {Microsoft Research},
  month       = {February},
  number      = {MSR-TR-2011-19},
  title       = {Memoir---Formal Specs and Correctness Proofs},
  year        = {2011}
}

Bootstrapping Trust in Modern Computers

Bryan Parno, Jonathan M. McCune, and Adrian Perrig
Springer, 2011
Book
@book{parno2011bootstrapping,
  author    = {Parno, Bryan and McCune, Jonathan M. and Perrig, Adrian},
  publisher = {Springer},
  title     = {Bootstrapping Trust in Modern Computers},
  year      = {2011}
}

Non-Interactive Verifiable Computation: Outsourcing Computation to Untrusted Workers

Rosario Gennaro, Craig Gentry, and Bryan Parno
Proceedings of the IACR CRYPTO Conference, August, 2010
Conference
@inproceedings{GGP2010,
  author    = {Gennaro, Rosario and Gentry, Craig and Parno, Bryan},
  booktitle = {Proceedings of the IACR CRYPTO Conference},
  month     = {August},
  title     = {Non-Interactive Verifiable Computation: Outsourcing Computation to Untrusted Workers},
  year      = {2010}
}

Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers

Bryan Parno
Carnegie Mellon University, May, 2010
ACM Dissertation Award
PhD Thesis Award
@phdthesis{parno2010thesis,
  author    = {Parno, Bryan},
  month     = {May},
  school    = {Carnegie Mellon University},
  title     = {Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers},
  year      = {2010}
}

Bootstrapping Trust in Commodity Computers

Bryan Parno, Jonathan M. McCune, and Adrian Perrig
Proceedings of the IEEE Symposium on Security and Privacy, May, 2010
Conference
@inproceedings{PaMcPe2010,
  author    = {Parno, Bryan and McCune, Jonathan M. and Perrig, Adrian},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  day       = {16--19},
  location  = {Oakland, CA, USA},
  month     = {May},
  title     = {Bootstrapping Trust in Commodity Computers},
  year      = {2010}
}

Don't Talk to Zombies: Mitigating DDoS Attacks via Attestation

Bryan Parno, Zongwei Zhou, and Adrian Perrig
Carnegie Mellon University, CyLab CMU-CyLab-09-009, June, 2009
Tech Report
@techreport{PaZhPe2009,
  author      = {Parno, Bryan and Zhou, Zongwei and Perrig, Adrian},
  institution = {Carnegie Mellon University, CyLab},
  month       = {June},
  number      = {CMU-CyLab-09-009},
  title       = {Don't Talk to Zombies: Mitigating {DDoS} Attacks via Attestation},
  year        = {2009}
}

CLAMP: Practical Prevention of Large-Scale Data Leaks

Bryan Parno, Jonathan M. McCune, Dan Wendlandt, David G. Andersen, and Adrian Perrig
Proceedings of the IEEE Symposium on Security and Privacy, May, 2009
Conference
@inproceedings{PMWAP2009,
  author    = {Parno, Bryan and McCune, Jonathan M. and Wendlandt, Dan and Andersen, David G. and Perrig, Adrian},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  day       = {17--20},
  location  = {Oakland, CA, USA},
  month     = {May},
  title     = {{CLAMP}: Practical Prevention of Large-Scale Data Leaks},
  year      = {2009}
}

Bootstrapping Trust in a ``Trusted'' Platform

Bryan Parno
Proceedings of the USENIX Workshop on Hot Topics in Security (HotSec), July, 2008
Workshop
@inproceedings{Parno2008,
  author     = {Parno, Bryan},
  booktitle  = {Proceedings of the USENIX Workshop on Hot Topics in
Security (HotSec)},
  location   = {San Jose, CA},
  month      = {July},
  title      = {Bootstrapping Trust in a ``Trusted'' Platform},
  xbooktitle = {USENIX Workshop on Hot Topics in Security},
  year       = {2008}
}

Unidirectional Key Distribution Across Time and Space with Applications to RFID Security

Ari Juels, Ravikanth Pappu, and Bryan Parno
Proceedings of the USENIX Security Symposium, July, 2008
Conference
@inproceedings{JuPaPa2008,
  author    = {Juels, Ari and Pappu, Ravikanth and Parno, Bryan},
  booktitle = {Proceedings of the USENIX Security Symposium},
  location  = {San Jose, CA},
  month     = {July},
  title     = {Unidirectional Key Distribution Across Time and Space with
Applications to {RFID} Security},
  year      = {2008}
}

Flicker: An Execution Infrastructure for TCB Minimization

Jonathan M. McCune, Bryan Parno, Adrian Perrig, Michael K. Reiter, and Hiroshi Isozaki
Proceedings of the ACM European Conference on Computer Systems (EuroSys), April, 2008
Intel's Hardware Security Academic Test-of-Time Award
Conference Award
@inproceedings{MPPRI2008,
  author    = {McCune, Jonathan M. and Parno, Bryan and Perrig, Adrian and Reiter, Michael K. and Isozaki, Hiroshi},
  booktitle = {Proceedings of the ACM European Conference on Computer Systems (EuroSys)},
  code      = {https://sourceforge.net/p/flickertcb/wiki/Home/},
  day       = {1--4},
  month     = {April},
  title     = {Flicker: An Execution Infrastructure for {TCB} Minimization},
  year      = {2008}
}

How Low Can You Go? Recommendations for Hardware-Supported Minimal TCB Code Execution

Jonathan M. McCune, Bryan Parno, Adrian Perrig, Michael K. Reiter, and Arvind Seshadri
Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March, 2008
Conference
@inproceedings{MPPRS2008,
  author    = {McCune, Jonathan M. and Parno, Bryan and Perrig, Adrian and Reiter, Michael K. and Seshadri, Arvind},
  booktitle = {Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)},
  day       = {1--5},
  month     = {March},
  title     = {How Low Can You Go? {Recommendations} for Hardware-Supported Minimal {TCB} Code Execution},
  year      = {2008}
}

SNAPP: Stateless Network-Authenticated Path Pinning

Bryan Parno, Adrian Perrig, and David Andersen
Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS), March, 2008
Conference
@inproceedings{snapp,
  author    = {Parno, Bryan and Perrig, Adrian and Andersen, David},
  booktitle = {Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS)},
  month     = {March},
  title     = {SNAPP: Stateless Network-Authenticated Path Pinning},
  year      = {2008}
}

Countermeasures against Government-Scale Monetary Forgery

Alessandro Acquisti, Nicolas Christin, Bryan Parno, and Adrian Perrig
Proceedings of the Financial Cryptography and Data Security Conference (FC), January, 2008
Conference
@inproceedings{forgery2008,
  author    = {Acquisti, Alessandro and Christin, Nicolas and Parno, Bryan and Perrig, Adrian},
  booktitle = {Proceedings of the Financial Cryptography and Data Security Conference (FC)},
  month     = {January},
  title     = {Countermeasures against Government-Scale Monetary Forgery},
  year      = {2008}
}

Portcullis: Protecting Connection Setup from Denial-of-Capability Attacks

Bryan Parno, Dan Wendlandt, Elaine Shi, Adrian Perrig, Bruce Maggs, and Yih-Chun Hu
Proceedings of ACM SIGCOMM, August, 2007
Conference
@inproceedings{PWSPMH2007,
  author    = {Parno, Bryan and Wendlandt, Dan and Shi, Elaine and Perrig, Adrian and Maggs, Bruce and Hu, Yih-Chun},
  booktitle = {Proceedings of ACM SIGCOMM},
  day       = {27--31},
  month     = {August},
  title     = {Portcullis: Protecting Connection Setup from Denial-of-Capability Attacks},
  year      = {2007}
}

Minimal TCB Code Execution (Extended Abstract)

Jonathan M. McCune, Bryan Parno, Adrian Perrig, Michael K. Reiter, and Arvind Seshadri
Proceedings of the IEEE Symposium on Security and Privacy, May, 2007
Conference
@inproceedings{McPaPeReSe2007,
  author    = {McCune, Jonathan M. and Parno, Bryan and Perrig, Adrian and Reiter, Michael K. and Seshadri, Arvind},
  booktitle = {Proceedings of the IEEE Symposium on Security and
Privacy},
  month     = {May},
  title     = {Minimal {TCB} Code Execution (Extended Abstract)},
  xurl      = {http://www.ece.cmu.edu/~jmmccune/papers/mccune_parno_perrig_reiter_seshadri_mintcb.pdf},
  year      = {2007}
}

Secure Sensor Network Routing: A Clean-Slate Approach

Bryan Parno, Mark Luk, Evan Gaustad, and Adrian Perrig
Proceedings of the Conference on Future Networking Technologies (CoNEXT), December, 2006
Conference
@inproceedings{PaLuGaPe2006,
  author    = {Parno, Bryan and Luk, Mark and Gaustad, Evan and Perrig, Adrian},
  booktitle = {Proceedings of the Conference on Future Networking Technologies (CoNEXT)},
  day       = {4--7},
  location  = {Lisboa, Portugal},
  month     = {December},
  title     = {Secure Sensor Network Routing: A Clean-Slate Approach},
  year      = {2006}
}

Phoolproof Phishing Prevention

Bryan Parno, Cynthia Kuo, and Adrian Perrig
Proceedings of the Financial Cryptography and Data Security Conference, February, 2006
Conference
@inproceedings{PaKuPe2006,
  author    = {Parno, Bryan and Kuo, Cynthia and Perrig, Adrian},
  booktitle = {Proceedings of the Financial Cryptography and Data Security Conference},
  day       = {27},
  location  = {Anguilla, British West Indies},
  month     = {February},
  title     = {Phoolproof Phishing Prevention},
  year      = {2006}
}

Browser Enhancements for Preventing Phishing Attacks

Bryan Parno, Cynthia Kuo, and Adrian Perrig
In Phishing and Counter-Measures: Understanding the Increasing Problem of Electronic Identity Theft, Markus Jakobsson and Steven Myers, Ed. Wiley-Interscience, , 2006
Book Chapter
@incollection{phishing2006,
  author    = {Parno, Bryan and Kuo, Cynthia and Perrig, Adrian},
  booktitle = {Phishing and Counter-Measures: Understanding the Increasing Problem of Electronic Identity Theft},
  editor    = {Markus Jakobsson and Steven Myers},
  publisher = {Wiley-Interscience},
  title     = {Browser Enhancements for Preventing Phishing Attacks},
  year      = {2006}
}

Challenges in Securing Vehicular Networks

Bryan Parno and Adrian Perrig
Proceedings of the Fourth Workshop on Hot Topics in Networks (HotNets), November, 2005
Workshop
@inproceedings{ParPer2005,
  author    = {Parno, Bryan and Perrig, Adrian},
  booktitle = {Proceedings of the Fourth Workshop on Hot Topics in Networks (HotNets)},
  day       = {14--15},
  location  = {College Park, MD, USA},
  month     = {November},
  title     = {Challenges in Securing Vehicular Networks},
  year      = {2005}
}

Distributed Detection of Node Replication Attacks in Sensor Networks

Bryan Parno
Carnegie Mellon University, May, 2005
Masters Thesis
@mastersthesis{parno2005thesis,
  author    = {Parno, Bryan},
  month     = {May},
  school    = {Carnegie Mellon University},
  title     = {Distributed Detection of Node Replication Attacks in Sensor Networks},
  year      = {2005}
}

Distributed Detection of Node Replication Attacks in Sensor Networks

Bryan Parno, Adrian Perrig, and Virgil Gligor
Proceedings of the IEEE Symposium on Security and Privacy, May, 2005
Test-of-Time Award
Conference Award
@inproceedings{PaPeGl2005,
  author    = {Parno, Bryan and Perrig, Adrian and Gligor, Virgil},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  month     = {May},
  title     = {Distributed Detection of Node Replication Attacks in Sensor Networks},
  year      = {2005}
}

FANFARE for the Common Flow

Elaine Shi, Bryan Parno, Adrian Perrig, Yih-Chun Hu, and Bruce Maggs
Carnegie Mellon University CMU-CS-05-148, February, 2005
Tech Report
@techreport{SPPHM2005,
  author      = {Shi, Elaine and Parno, Bryan and Perrig, Adrian and Hu, Yih-Chun and Maggs, Bruce},
  institution = {Carnegie Mellon University},
  month       = {February},
  number      = {CMU-CS-05-148},
  title       = {{FANFARE} for the Common Flow},
  year        = {2005}
}

Defending a P2P Digital Preservation System

Bryan Parno and Mema Rousoppoulos
IEEE Transactions on Dependable and Secure Computing (IEEE TDSC), Vol. 1(4), December, 2004
Journal
@article{lockss2004,
  author    = {Parno, Bryan and Rousoppoulos, Mema},
  journal   = {IEEE Transactions on Dependable and Secure Computing (IEEE TDSC)},
  month     = {December},
  number    = {4},
  title     = {Defending a P2P Digital Preservation System},
  volume    = {1},
  year      = {2004}
}

How to Subvert LOCKSS and What the LOCKSSmith Can Do About It

Bryan Parno
Harvard University, April, 2004
Undergraduate Thesis
@mastersthesis{parno2004thesis,
  author    = {Parno, Bryan},
  month     = {April},
  school    = {Harvard University},
  title     = {How to Subvert {LOCKSS} and What the {LOCKSSmith} Can Do About It},
  type      = {bachelor's thesis},
  year      = {2004}
}

An Analysis of Database-Driven Mail Servers

Nick Elprin and Bryan Parno
Proceedings of the Large Installation Systems Administration Conference (LISA), October, 2003
Conference
@inproceedings{lisa2003,
  author    = {Elprin, Nick and Parno, Bryan},
  booktitle = {Proceedings of the Large Installation Systems Administration Conference (LISA)},
  month     = {October},
  title     = {An Analysis of Database-Driven Mail Servers},
  year      = {2003}
}