Bryan Parno

Proc. ACM Program. Lang., 2024

Verus: A Practical Foundation for Systems Verification.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, 2024

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

[BibT_eX]

[DOI]

Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation, 2024

A Framework for Debugging Automated Program Verification Proofs via Proof Actions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

Leaf: Modularity for Temporary Sharing in Separation Logic.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., October, 2023

Verus: Verifying Rust Programs using Linear Ghost Types.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., April, 2023

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., January, 2023

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

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2023

WaveCert: Formal Compiler Validation for Asynchronous Dataflow Programs.

[BibT_eX]

[DOI]

Zhengyao Lin

Joshua Gancher

CoRR, 2023

Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2023

Verus: Verifying Rust Programs using Linear Ghost Types (extended version).

[BibT_eX]

[DOI]

CoRR, 2023

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

[BibT_eX]

[DOI]

Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023

No Root Store Left Behind.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM Workshop on Hot Topics in Networks, 2023

Mariposa: Measuring SMT Instability in Automated Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2023

FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores.

[BibT_eX]

[DOI]

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares.

[BibT_eX]

[DOI]

Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

2022

Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2022

Degradation Attacks on Certifiably Robust Neural Networks.

[BibT_eX]

[DOI]

Trans. Mach. Learn. Res., 2022

Linear types for large-scale systems verification.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Logic Locking - Connecting Theory and Practice.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2022

Algebraic Reductions of Knowledge.

[BibT_eX]

[DOI]

Abhiram Kothapalli

IACR Cryptol. ePrint Arch., 2022

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code.

[BibT_eX]

[DOI]

CoRR, 2022

Provably-Safe Multilingual Software Sandboxing using WebAssembly.

[BibT_eX]

[DOI]

Jay Bosamiya

Wen Shih Lim

Proceedings of the 31st USENIX Security Symposium, 2022

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

[BibT_eX]

[DOI]

Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, 2022

Self-correcting Neural Networks for Safe Classification.

[BibT_eX]

[DOI]

Proceedings of the Software Verification and Formal Methods for ML-Enabled Autonomous Systems, 2022

2021

Transparency Dictionaries with Succinct Proofs of Correct Operation.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2021

Blockchains Enable Non-Interactive MPC.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2021

Self-Repairing Neural Networks: Provable Safety for Deep Networks via Dynamic Repair.

[BibT_eX]

[DOI]

CoRR, 2021

Don't Yank My Chain: Auditable NF Service Chaining.

[BibT_eX]

[DOI]

Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation, 2021

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

[BibT_eX]

[DOI]

Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation, 2021

Fast Geometric Projections for Local Robustness Certification.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Learning Representations, 2021

HerQules: securing programs via hardware-enforced message queues.

[BibT_eX]

[DOI]

Daming D. Chen

Wen Shih Lim

Mohammad Bakhshalipour

Phillip B. Gibbons

James C. Hoe

Proceedings of the ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2021

2020

A Direct Construction for Asymptotically Optimal zkSNARKs.

[BibT_eX]

[DOI]

Abhiram Kothapalli

Elisaweta Masserova

IACR Cryptol. ePrint Arch., 2020

Storing and Retrieving Secrets on a Blockchain.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2020

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2020

Talek: Private Group Messaging with Hidden Access Patterns.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2020

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

[BibT_eX]

[DOI]

Proceedings of the Software Verification - 12th International Conference, 2020

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.

[BibT_eX]

[DOI]

Karthikeyan Bhargavan

Benjamin Beurdouche

Joonwon Choi

Christoph M. Wintersteiger

Santiago Zanella Béguelin

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Armada: low-effort verification of high-performance concurrent programs.

[BibT_eX]

[DOI]

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

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

[BibT_eX]

[DOI]

Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation, 2020

CAPS: Smoothly Transitioning to a More Resilient Web PKI.

[BibT_eX]

[DOI]

Proceedings of the ACSAC '20: Annual Computer Security Applications Conference, 2020

2019

A verified, efficient embedding of a verifiable assembly language.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.

[BibT_eX]

[DOI]

Karthikeyan Bhargavan

Benjamin Beurdouche

Joonwon Choi

Christoph M. Wintersteiger

Santiago Zanella Béguelin

IACR Cryptol. ePrint Arch., 2019

SoK: Computer-Aided Cryptography.

[BibT_eX]

[DOI]

Manuel Barbosa

Gilles Barthe

Karthikeyan Bhargavan

IACR Cryptol. ePrint Arch., 2019

2017

IronFleet: proving safety and liveness of practical distributed systems.

[BibT_eX]

[DOI]

Michael Lowell Roberts

Srinath T. V. Setty

Brian Zill

Commun. ACM, 2017

Vale: Verifying High-Performance Cryptographic Assembly Code.

[BibT_eX]

[DOI]

Proceedings of the 26th USENIX Security Symposium, 2017

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

[BibT_eX]

[DOI]

Proceedings of the 26th Symposium on Operating Systems Principles, 2017

Everest: Towards a Verified, Drop-in Replacement of HTTPS.

[BibT_eX]

[DOI]

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

2016

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

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2016

Pinocchio: nearly practical verifiable computation.

[BibT_eX]

[DOI]

Commun. ACM, 2016

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

[BibT_eX]

[DOI]

Cédric Fournet

Markulf Kohlweiss

Proceedings of the IEEE Symposium on Security and Privacy, 2016

2015

Network Adversary Attacks against Secure Encryption Schemes.

[BibT_eX]

[DOI]

Virgil D. Gligor

Ji Sun Shin

IEICE Trans. Commun., 2015

A Note on the Unsoundness of vnTinyRAM's SNARK.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2015

IronFleet: proving practical distributed systems correct.

[BibT_eX]

[DOI]

Michael Lowell Roberts

Srinath T. V. Setty

Brian Zill

Proceedings of the 25th Symposium on Operating Systems Principles, 2015

2014

Geppetto: Versatile Verifiable Computation.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2014

Missive: Fast Application Launch From an Untrusted Buffer Cache.

[BibT_eX]

[DOI]

Proceedings of the 2014 USENIX Annual Technical Conference, 2014

Permacoin: Repurposing Bitcoin Work for Data Preservation.

[BibT_eX]

[DOI]

Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014

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

[BibT_eX]

[DOI]

Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014

Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers (dissertation, updated version).

[BibT_eX]

[DOI]

ACM Books 2, ACM / Morgan & Claypool, ISBN: 978-1-62705-477-5, 2014

2013

The 10-Kilobyte Web Browser.

[BibT_eX]

[DOI]

Jon Howell

John R. Douceur

How to Run POSIX Apps in a Minimal Picoprocess.

[BibT_eX]

[DOI]

Jon Howell

John R. Douceur

Proceedings of the 2013 USENIX Annual Technical Conference, 2013

Embassies: Radically Refactoring the Web.

[BibT_eX]

[DOI]

Jon Howell

John R. Douceur

Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, 2013

Shroud: ensuring private access to large-scale data in the data center.

[BibT_eX]

[DOI]

Proceedings of the 11th USENIX conference on File and Storage Technologies, 2013

Fifth ACM cloud computing security workshop (CCSW 2013).

[BibT_eX]

[DOI]

Ari Juels

Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

The first workshop on language support for privacy-enhancing technologies (PETShop'13).

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

Pinocchio coin: building zerocoin from a succinct pairing-based proof system.

[BibT_eX]

[DOI]

Proceedings of the PETShop'13, 2013

2012

Resolving the conflict between generality and plausibility in verified computation.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2012

Toward Practical Private Access to Data Centers via Parallel ORAM.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2012

Quadratic Span Programs and Succinct NIZKs without PCPs.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2012

Trust extension for commodity computers.

[BibT_eX]

[DOI]

Commun. ACM, 2012

Lockdown: Towards a Safe and Practical Architecture for Security Applications on Commodity Platforms.

[BibT_eX]

[DOI]

Proceedings of the Trust and Trustworthy Computing - 5th International Conference, 2012

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

[BibT_eX]

[DOI]

Proceedings of the IEEE Symposium on Security and Privacy, 2012

2011

Bootstrapping Trust in Modern Computers.

[BibT_eX]

[DOI]

Jonathan M. McCune

Springer Briefs in Computer Science 10, Springer, ISBN: 978-1-4614-1460-5, 2011

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

[BibT_eX]

[DOI]

Mariana Raykova

Vinod Vaikuntanathan

IACR Cryptol. ePrint Arch., 2011

Memoir: Practical State Continuity for Protected Modules.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE Symposium on Security and Privacy, 2011

The web interface should be radically refactored.

[BibT_eX]

[DOI]

Proceedings of the Tenth ACM Workshop on Hot Topics in Networks (HotNets-X), 2011

2010

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

[BibT_eX]

[DOI]

PhD thesis, 2010

Bootstrapping Trust in Commodity Computers.

[BibT_eX]

[DOI]

Jonathan M. McCune

Proceedings of the 31st IEEE Symposium on Security and Privacy, 2010

2009

Non-Interactive Verifiable Computing: Outsourcing Computation to Untrusted Workers.

[BibT_eX]

[DOI]

Rosario Gennaro

Craig Gentry

IACR Cryptol. ePrint Arch., 2009

CLAMP: Practical Prevention of Large-Scale Data Leaks.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE Symposium on Security and Privacy (SP 2009), 2009

2008

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

[BibT_eX]

[DOI]

Ari Juels

Ravikanth Pappu

IACR Cryptol. ePrint Arch., 2008

Bootstrapping Trust in a "Trusted" Platform.

[BibT_eX]

[DOI]

Proceedings of the 3rd USENIX Workshop on Hot Topics in Security, 2008

Countermeasures against Government-Scale Monetary Forgery.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security, 12th International Conference, 2008

Flicker: an execution infrastructure for tcb minimization.

[BibT_eX]

[DOI]

Proceedings of the 2008 EuroSys Conference, Glasgow, Scotland, UK, April 1-4, 2008, 2008

SNAPP: stateless network-authenticated path pinning.

[BibT_eX]

[DOI]

Dave G. Andersen

Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, 2008

How low can you go?: recommendations for hardware-supported minimal TCB code execution.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, 2008

2007

Minimal TCB Code Execution.

[BibT_eX]

[DOI]

Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), 2007

Portcullis: protecting connection setup from denial-of-capability attacks.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGCOMM 2007 Conference on Applications, 2007

2006

Phoolproof Phishing Prevention.

[BibT_eX]

[DOI]

Cynthia Kuo

Proceedings of the Financial Cryptography and Data Security, 2006

Secure sensor network routing: a clean-slate approach.

[BibT_eX]

[DOI]

Proceedings of the 2006 ACM Conference on Emerging Network Experiment and Technology, 2006

2005

Distributed Detection of Node Replication Attacks in Sensor Networks.

[BibT_eX]

[DOI]

Virgil D. Gligor

Proceedings of the 2005 IEEE Symposium on Security and Privacy (S&P 2005), 2005

2004

Defending a P2P Digital Preservation System.

[BibT_eX]

[DOI]

Mema Roussopoulos

IEEE Trans. Dependable Secur. Comput., 2004

2003

An Analysis of Database-Driven Mail Servers.

[BibT_eX]

[DOI]

Nick Elprin