An Analysis of Database-Driven Mail Servers. - Nick Elprin; Bryan Parno (LISA, 2003)

Defending a P2P Digital Preservation System. - Bryan Parno; Mema Roussopoulos (IEEE Trans. Dependable Secur. Comput., 2004)

Distributed Detection of Node Replication Attacks in Sensor Networks. - Bryan Parno; Adrian Perrig; Virgil D. Gligor (S&P, 2005)

Secure sensor network routing: a clean-slate approach. - Bryan Parno; Mark Luk; Evan Gaustad; Adrian Perrig (CoNEXT, 2006)

Phoolproof Phishing Prevention. - Bryan Parno; Cynthia Kuo; Adrian Perrig (Financial Cryptography, 2006)

Portcullis: protecting connection setup from denial-of-capability attacks. - Bryan Parno; Dan Wendlandt; Elaine Shi; Adrian Perrig; Bruce M. Maggs; Yih-Chun Hu (SIGCOMM, 2007)

Minimal TCB Code Execution. - Jonathan M. McCune; Bryan Parno; Adrian Perrig; Michael K. Reiter; Arvind Seshadri (S&P, 2007)

How low can you go?: recommendations for hardware-supported minimal TCB code execution. - Jonathan M. McCune; Bryan Parno; Adrian Perrig; Michael K. Reiter; Arvind Seshadri (ASPLOS, 2008)

SNAPP: stateless network-authenticated path pinning. - Bryan Parno; Adrian Perrig; Dave G. Andersen (AsiaCCS, 2008)

Flicker: an execution infrastructure for tcb minimization. - Jonathan M. McCune; Bryan Parno; Adrian Perrig; Michael K. Reiter; Hiroshi Isozaki (EuroSys, 2008)

Countermeasures against Government-Scale Monetary Forgery. - Alessandro Acquisti; Nicolas Christin; Bryan Parno; Adrian Perrig (Financial Cryptography, 2008)

Bootstrapping Trust in a "Trusted" Platform. - Bryan Parno (HotSec, 2008)

Unidirectional Key Distribution Across Time and Space with Applications to RFID Security. - Ari Juels; Ravikanth Pappu; Bryan Parno (IACR Cryptol. ePrint Arch., 2008)

CLAMP: Practical Prevention of Large-Scale Data Leaks. - Bryan Parno; Jonathan M. McCune; Dan Wendlandt; David G. Andersen; Adrian Perrig (SP, 2009)

Non-Interactive Verifiable Computing: Outsourcing Computation to Untrusted Workers. - Rosario Gennaro; Craig Gentry; Bryan Parno (IACR Cryptol. ePrint Arch., 2009)

Bootstrapping Trust in Commodity Computers. - Bryan Parno; Jonathan M. McCune; Adrian Perrig (IEEE Symposium on Security and Privacy, 2010)

Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers. - Bryan Parno (2010)

The web interface should be radically refactored. - John R. Douceur; Jon Howell; Bryan Parno; Michael Walfish; Xi Xiong (HotNets, 2011)

Memoir: Practical State Continuity for Protected Modules. - Bryan Parno; Jacob R. Lorch; John R. Douceur; James W. Mickens; Jonathan M. McCune (IEEE Symposium on Security and Privacy, 2011)

How to Delegate and Verify in Public: Verifiable Computation from Attribute-based Encryption. - Bryan Parno; Mariana Raykova 001; Vinod Vaikuntanathan (IACR Cryptol. ePrint Arch., 2011)

Bootstrapping Trust in Modern Computers. - Bryan Parno; Jonathan M. McCune; Adrian Perrig (Springer, 2011)

User-Driven Access Control: Rethinking Permission Granting in Modern Operating Systems. - Franziska Roesner; Tadayoshi Kohno; Alexander Moshchuk; Bryan Parno; Helen J. Wang; Crispin Cowan (IEEE Symposium on Security and Privacy, 2012)

Lockdown: Towards a Safe and Practical Architecture for Security Applications on Commodity Platforms. - Amit Vasudevan; Bryan Parno; Ning Qu; Virgil D. Gligor; Adrian Perrig (TRUST, 2012)

Trust extension for commodity computers. - Bryan Parno (Commun. ACM, 2012)

Quadratic Span Programs and Succinct NIZKs without PCPs. - Rosario Gennaro; Craig Gentry; Bryan Parno; Mariana Raykova 001 (IACR Cryptol. ePrint Arch., 2012)

Toward Practical Private Access to Data Centers via Parallel ORAM. - Jacob R. Lorch; James W. Mickens; Bryan Parno; Mariana Raykova 001; Joshua Schiffman (IACR Cryptol. ePrint Arch., 2012)

Resolving the conflict between generality and plausibility in verified computation. - Srinath T. V. Setty; Benjamin Braun; Victor Vu; Andrew J. Blumberg; Bryan Parno; Michael Walfish (IACR Cryptol. ePrint Arch., 2012)

Pinocchio coin: building zerocoin from a succinct pairing-based proof system. - George Danezis; Cédric Fournet; Markulf Kohlweiss; Bryan Parno (PETShop@CCS, 2013)

The first workshop on language support for privacy-enhancing technologies (PETShop'13). - Martin Franz; Andreas Holzer; Rupak Majumdar; Bryan Parno; Helmut Veith (CCS, 2013)

Fifth ACM cloud computing security workshop (CCSW 2013). - Ari Juels; Bryan Parno (CCS, 2013)

Shroud: ensuring private access to large-scale data in the data center. - Jacob R. Lorch; Bryan Parno; James W. Mickens; Mariana Raykova 001; Joshua Schiffman (FAST, 2013)

Embassies: Radically Refactoring the Web. - Jon Howell; Bryan Parno; John R. Douceur (NSDI, 2013)

How to Run POSIX Apps in a Minimal Picoprocess. - Jon Howell; Bryan Parno; John R. Douceur (USENIX ATC, 2013)

The 10-Kilobyte Web Browser. - Jon Howell; Bryan Parno; John R. Douceur (login Usenix Mag., 2013)

Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers (dissertation, updated version). - Bryan Parno (ACM / Morgan & Claypool, 2014)

Ironclad Apps: End-to-End Security via Automated Full-System Verification. - Chris Hawblitzel; Jon Howell; Jacob R. Lorch; Arjun Narayan; Bryan Parno; Danfeng Zhang; Brian Zill (OSDI, 2014)

Permacoin: Repurposing Bitcoin Work for Data Preservation. - Andrew Miller 001; Ari Juels; Elaine Shi; Bryan Parno; Jonathan Katz (IEEE Symposium on Security and Privacy, 2014)

Missive: Fast Application Launch From an Untrusted Buffer Cache. - Jon Howell; Jeremy Elson; Bryan Parno; John R. Douceur (USENIX ATC, 2014)

Geppetto: Versatile Verifiable Computation. - Craig Costello; Cédric Fournet; Jon Howell; Markulf Kohlweiss; Benjamin Kreuter; Michael Naehrig; Bryan Parno; Samee Zahur (IACR Cryptol. ePrint Arch., 2014)

IronFleet: proving practical distributed systems correct. - Chris Hawblitzel; Jon Howell; Manos Kapritsos; Jacob R. Lorch; Bryan Parno; Michael Lowell Roberts; Srinath T. V. Setty; Brian Zill (SOSP, 2015)

A Note on the Unsoundness of vnTinyRAM's SNARK. - Bryan Parno (IACR Cryptol. ePrint Arch., 2015)

Network Adversary Attacks against Secure Encryption Schemes. - Virgil D. Gligor; Bryan Parno; Ji Sun Shin (IEICE Trans. Commun., 2015)

Cinderella: Turning Shabby X.509 Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation. - Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Bryan Parno (IEEE Symposium on Security and Privacy, 2016)

Pinocchio: nearly practical verifiable computation. - Bryan Parno; Jon Howell; Craig Gentry; Mariana Raykova 001 (Commun. ACM, 2016)

Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data. - Dario Fiore 001; Cédric Fournet; Esha Ghosh; Markulf Kohlweiss; Olga Ohrimenko; Bryan Parno (IACR Cryptol. ePrint Arch., 2016)

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; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Komodo: Using verification to disentangle secure-enclave hardware from software. - Andrew Ferraiuolo; Andrew Baumann; Chris Hawblitzel; Bryan Parno (SOSP, 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 T. V. Setty; Laure Thompson (USENIX Security Symposium, 2017)

IronFleet: proving safety and liveness of practical distributed systems. - Chris Hawblitzel; Jon Howell; Manos Kapritsos; Jacob R. Lorch; Bryan Parno; Michael Lowell Roberts; Srinath T. V. Setty; Brian Zill (Commun. ACM, 2017)

SoK: Computer-Aided Cryptography. - Manuel Barbosa; Gilles Barthe; Karthikeyan Bhargavan; Bruno Blanchet; Cas Cremers; Kevin Liao; Bryan Parno (IACR Cryptol. ePrint Arch., 2019)

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; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

A verified, efficient embedding of a verifiable assembly language. - Aymeric Fromherz; Nick Giannarakis; Chris Hawblitzel; Bryan Parno; Aseem Rastogi; Nikhil Swamy (Proc. ACM Program. Lang., 2019)

CAPS: Smoothly Transitioning to a More Resilient Web PKI. - Stephanos Matsumoto; Jay Bosamiya; Yucheng Dai; Paul C. van Oorschot; Bryan Parno (ACSAC, 2020)

Storage Systems are Distributed Systems (So Verify Them That Way!). - Travis Hance; Andrea Lattuada 001; Chris Hawblitzel; Jon Howell; Rob Johnson 001; Bryan Parno (OSDI, 2020)

Armada: low-effort verification of high-performance concurrent programs. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (PLDI, 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; et al. (SP, 2020)

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. - Jay Bosamiya; Sydney Gibson; Yao Li 004; Bryan Parno; Chris Hawblitzel (VSTTE, 2020)

Talek: Private Group Messaging with Hidden Access Patterns. - Raymond Cheng 001; William Scott 002; Elisaweta Masserova; Irene Zhang; Vipul Goyal; Thomas E. Anderson; Arvind Krishnamurthy; Bryan Parno (IACR Cryptol. ePrint Arch., 2020)

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. - Antoine Delignat-Lavaud; Cédric Fournet; Bryan Parno; Jonathan Protzenko; Tahina Ramananandro; Jay Bosamiya; Joseph Lallemand; Itsaka Rakotonirina; Yi Zhou 025 (IACR Cryptol. ePrint Arch., 2020)

Storing and Retrieving Secrets on a Blockchain. - Vipul Goyal; Abhiram Kothapalli; Elisaweta Masserova; Bryan Parno; Yifan Song 001 (IACR Cryptol. ePrint Arch., 2020)

A Direct Construction for Asymptotically Optimal zkSNARKs. - Abhiram Kothapalli; Elisaweta Masserova; Bryan Parno (IACR Cryptol. ePrint Arch., 2020)

HerQules: securing programs via hardware-enforced message queues. - Daming D. Chen; Wen Shih Lim; Mohammad Bakhshalipour; Phillip B. Gibbons; James C. Hoe; Bryan Parno (ASPLOS, 2021)

Fast Geometric Projections for Local Robustness Certification. - Aymeric Fromherz; Klas Leino; Matt Fredrikson; Bryan Parno; Corina S. Pasareanu (ICLR, 2021)

Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. - Travis Hance; Marijn Heule; Ruben Martins; Bryan Parno (NSDI, 2021)

Don't Yank My Chain: Auditable NF Service Chaining. - Guyue Liu; Hugo Sadok; Anne Kohlbrenner; Bryan Parno; Vyas Sekar; Justine Sherry (NSDI, 2021)

Self-Repairing Neural Networks: Provable Safety for Deep Networks via Dynamic Repair. - Klas Leino; Aymeric Fromherz; Ravi Mangal; Matt Fredrikson; Bryan Parno; Corina S. Pasareanu (CoRR, 2021)

Blockchains Enable Non-Interactive MPC. - Vipul Goyal; Elisaweta Masserova; Bryan Parno; Yifan Song 001 (IACR Cryptol. ePrint Arch., 2021)

Transparency Dictionaries with Succinct Proofs of Correct Operation. - Ioanna Tzialla; Abhiram Kothapalli; Bryan Parno; Srinath T. V. Setty (IACR Cryptol. ePrint Arch., 2021)

Self-correcting Neural Networks for Safe Classification. - Klas Leino; Aymeric Fromherz; Ravi Mangal; Matt Fredrikson; Bryan Parno; Corina S. Pasareanu (NSV/FoMLAS@CAV, 2022)

Hammurabi: A Framework for Pluggable, Logic-Based X.509 Certificate Validation Policies. - James Larisch; Waqar Aqeel; Michael Lum; Yaelle Goldschlag; Leah Kannan; Kasra Torshizi; Yujie Wang; Taejoong Chung; Dave Levin; Bruce M. Maggs; Alan Mislove; Bryan Parno; et al. (CCS, 2022)

Provably-Safe Multilingual Software Sandboxing using WebAssembly. - Jay Bosamiya; Wen Shih Lim; Bryan Parno (USENIX Security Symposium, 2022)

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code. - Alexandra E. Michael; Anitha Gollamudi; Jay Bosamiya; Craig Disselkoen; Aidan Denlinger; Conrad Watt; Bryan Parno; Marco Patrignani; Marco Vassena; Deian Stefan (CoRR, 2022)

Algebraic Reductions of Knowledge. - Abhiram Kothapalli; Bryan Parno (IACR Cryptol. ePrint Arch., 2022)

Logic Locking - Connecting Theory and Practice. - Elisaweta Masserova; Deepali Garg; Ken Mai; Lawrence T. Pileggi; Vipul Goyal; Bryan Parno (IACR Cryptol. ePrint Arch., 2022)

Linear types for large-scale systems verification. - Jialin Li 001; Andrea Lattuada 001; Yi Zhou 025; Jonathan Cameron; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2022)

Degradation Attacks on Certifiably Robust Neural Networks. - Klas Leino; Chi Zhang; Ravi Mangal; Matt Fredrikson; Bryan Parno; Corina S. Pasareanu (Trans. Mach. Learn. Res., 2022)

Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Haojun Ma; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (ACM Trans. Program. Lang. Syst., 2022)

Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares. - Yi Zhou 025; Sydney Gibson; Sarah Cai; Menucha Winchell; Bryan Parno (CCS, 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 (CPP, 2023)

Mariposa: Measuring SMT Instability in Automated Program Verification. - Yi Zhou 025; Jay Bosamiya; Yoshiki Takashima; Jessica Li; Marijn Heule; Bryan Parno (FMCAD, 2023)

No Root Store Left Behind. - James Larisch; Waqar Aqeel; Taejoong Chung; Eddie Kohler; Dave Levin; Bruce M. Maggs; Bryan Parno; Christo Wilson (HotNets, 2023)

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. - Travis Hance; Yi Zhou 025; Andrea Lattuada 001; Reto Achermann; Alex Conway 001; Ryan Stutsman; Gerd Zellweger; Chris Hawblitzel; Jon Howell; Bryan Parno (OSDI, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types (extended version). - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (CoRR, 2023)

Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version). - Travis Hance; Jon Howell; Oded Padon; Bryan Parno (CoRR, 2023)

WaveCert: Formal Compiler Validation for Asynchronous Dataflow Programs. - Zhengyao Lin; Joshua Gancher; Bryan Parno (CoRR, 2023)

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System. - Joshua Gancher; Sydney Gibson; Pratap Singh; Samvid Dharanikota; Bryan Parno (IACR Cryptol. ePrint Arch., 2023)

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code. - Alexandra E. Michael; Anitha Gollamudi; Jay Bosamiya; Evan Johnson 001; Aidan Denlinger; Craig Disselkoen; Conrad Watt; Bryan Parno; Marco Patrignani; Marco Vassena; Deian Stefan (Proc. ACM Program. Lang., 2023)

Verus: Verifying Rust Programs using Linear Ghost Types. - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2023)

Leaf: Modularity for Temporary Sharing in Separation Logic. - Travis Hance; Jon Howell; Oded Padon; Bryan Parno (Proc. ACM Program. Lang., 2023)

A Framework for Debugging Automated Program Verification Proofs via Proof Actions. - Chanhee Cho; Yi Zhou 025; Jay Bosamiya; Bryan Parno (CAV (1), 2024)

Context Pruning for More Robust SMT-based Program Verification. - Yi Zhou 025; Jay Bosamiya; Jessica Li; Marijn J. H. Heule; Bryan Parno (FMCAD, 2024)

Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs. - Tony Nuda Zhang; Travis Hance; Manos Kapritsos; Tej Chajed; Bryan Parno (OSDI, 2024)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)

AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement. - Pranjal Aggarwal; Bryan Parno; Sean Welleck (CoRR, 2024)

FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions. - Zhengyao Lin; Joshua Gancher; Bryan Parno (Proc. ACM Program. Lang., 2024)

Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification. - Yi Zhou 025; Amar Shah; Zhengyao Lin; Marijn Heule; Bryan Parno (CADE, 2025)

Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. - Tony Nuda Zhang; Keshav Singh; Tej Chajed; Manos Kapritsos; Bryan Parno (OSDI, 2025)

OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries. - Pratap Singh; Joshua Gancher; Bryan Parno (IACR Cryptol. ePrint Arch., 2025)