Chapter A Framework for Debugging Automated Program Verification Proofs via Proof Actions 2024 • Lecture Notes in Computer Science • 14681 LNCS:348-361 Cho C, Zhou Y, Bosamiya J, Parno B
Conference Algebraic Reductions of Knowledge 2023 • Lecture Notes in Computer Science • 14084 LNCS:669-701 Kothapalli A, Parno B
Conference FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores 2023 • CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023 • 30-46 Arasu A, Ramananandro T, Rastogi A, Swamy N, Fromherz A, Hietala K, Parno B, Ramamurthy R
Conference Galapagos: Developing Verified Low-Level Cryptography on Heterogeneous Hardware 2023 • PROCEEDINGS OF THE 2023 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, CCS 2023 • 2113-2127 Zhou Y, Gibson S, Cai S, Winchell M, Parno B
Journal Article Leaf: Modularity for Temporary Sharing in Separation Logic 2023 • Proceedings of the ACM on Programming Languages • 7(OOPSLA): Hance T, Howell J, Padon O, Parno B
Preprint Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version) 2023 Hance T, Howell J, Padon O, Parno B
Conference Mariposa: Measuring SMT Instability in Automated Program Verification 2023 • Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023 • 178-188 Zhou Y, Bosamiya J, Takashima Y, Li J, Heule M, Parno B
Journal Article MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code 2023 • Proceedings of the ACM on Programming Languages • 7(POPL): Michael AE, Gollamudi A, Bosamiya J, Johnson E, Denlinger A, Disselkoen C, Watt C, Parno B, Patrignani M, Vassena M, Stefan D
Conference No Root Store Left Behind 2023 • PROCEEDINGS OF THE 22ND ACM WORKSHOP ON HOT TOPICS IN NETWORKS, HOTNETS 2023 • 295-301 Larisch J, Aqeel W, Chung T, Kohler E, Levin D, Maggs BM, Parno B, Wilson C
Conference Owl: Compositional Verification of Security Protocols via an Information-Flow Type System 2023 • IEEE Symposium on Security and Privacy: Proceedings • 2023-May:1130-1147 Gancher J, Gibson S, Singh P, Dharanikota S, Parno B
Conference Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems 2023 • PROCEEDINGS OF THE 17TH USENIX SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION, OSDI 2023 • 911-929 Hance T, Zhou Y, Lattuada A, Achermann R, Conway A, Stutsman R, Zellweger G, Hawblitzel C, Howell J, Parno B
Journal Article Verus: Verifying Rust Programs using Linear Ghost Types 2023 • Proceedings of the ACM on Programming Languages • 7(OOPSLA): Lattuada A, Hance T, Cho C, Brun M, Subasinghe I, Zhou Y, Howell J, Parno B, Hawblitzel C
Preprint Verus: Verifying Rust Programs using Linear Ghost Types (extended version) 2023 Lattuada A, Hance T, Cho C, Brun M, Subasinghe I, Zhou Y, Howell J, Parno B, Hawblitzel C
Journal Article Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility 2022 • ACM Transactions on Programming Languages and Systems • 44(2): Lorch JR, Chen Y, Kapritsos M, Ma H, Parno B, Qadeer S, Sharma U, Wilcox JR, Zhao X
Journal Article Degradation Attacks on Certifiably Robust Neural Networks 2022 • Transactions of Machine Learning Research • 1(1): Leino K, Zhang C, Mangal R, Fredrikson M, Parno B, Pasareanu C
Conference Hammurabi: A Framework for Pluggable, Logic-Based X.509 Certificate Validation Policies 2022 • Proceedings of the ACM Conference on Computer and Communications Security • 1857-1870 Larisch J, Aqeel W, Lum M, Goldschlag Y, Kannan L, Torshizi K, Wang Y, Chung T, Levin D, Maggs BM, Mislove A, Parno B, Wilson C
Journal Article Linear Types for Large-Scale Systems Verification 2022 • Proceedings of the ACM on Programming Languages • 6(OOPSLA): Li J, Lattuada A, Zhou Y, Cameron J, Howell J, Parno B, Hawblitzel C
Preprint MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code 2022 Michael AE, Gollamudi A, Bosamiya J, Disselkoen C, Denlinger A, Watt C, Parno B, Patrignani M, Vassena M, Stefan D
Conference Provably-Safe Multilingual Software Sandboxing using WebAssembly 2022 • PROCEEDINGS OF THE 31ST USENIX SECURITY SYMPOSIUM • 1975-1992 Bosamiya J, Lim WS, Parno B
Chapter Self-correcting Neural Networks for Safe Classification 2022 • Lecture Notes in Computer Science • 13466:96-130 Leino K, Fromherz A, Mangal R, Fredrikson M, Parno B, Pasareanu C
Chapter Storing and Retrieving Secrets on a Blockchain 2022 • Lecture Notes in Computer Science • 13177:252-282 Goyal V, Kothapalli A, Masserova E, Parno B, Song Y
Conference Transparency Dictionaries with Succinct Proofs of Correct Operation 2022 • 29th Annual Network and Distributed System Security Symposium, NDSS 2022 Tzialla I, Kothapalli A, Parno B, Setty S
Conference A security model and fully verified implementation for the IETF QUIC record layer 2021 • IEEE Symposium on Security and Privacy: Proceedings • 2021-May:1162-1178 Delignat-Lavaud A, Fournet C, Parno B, Protzenko J, Ramananandro T, Bosamiya J, Lallemand J, Rakotonirina I, Zhou Y
Chapter Blockchains Enable Non-interactive MPC 2021 • Lecture Notes in Computer Science • 13043:162-193 Goyal V, Masserova E, Parno B, Song Y
Conference Don't Yank My Chain: Auditable NF Service Chaining 2021 • PROCEEDINGS OF THE 18TH USENIX SYMPOSIUM ON NETWORKED SYSTEM DESIGN AND IMPLEMENTATION • 155-174 Liu G, Sadok H, Kohlbrenner A, Parno B, Sekar V, Sherry J
