Bryan Parno Professor Website ORCiD Google Scholars Link Office 2121 Mehrabian Collaborative Innovation Center Email parno@cmu.edu Phone (412) 268-2033 Department Computer Science Department CIT - Electrical and Computer Engineering Research Interests Cryptography Distributed Systems Formal Methods Operating Systems Programming Languages Security Security and Privacy Software Verification Systems Advisees Zhengyao Lin Michael McLoughlin Pratap Singh Yi Zhou Amar Shah Elanor Tang CSD Courses Taught 15330 - Fall, 2024 Biography Bryan Parno is the Kavčić-Moura Professor of Electrical & Computer Engineering and Professor of Computer Science at Carnegie Mellon University, and a Senior Member of ACM and IEEE. After receiving a Bachelor's degree from Harvard College, he completed his PhD working with Adrian Perrig at Carnegie Mellon University, where his dissertation won the 2010 ACM Doctoral Dissertation Award. He then spent six years as a Researcher in Microsoft Research before returning to CMU.Bryan's research is primarily focused on investigating long-term, fundamental improvements in how to design and build secure systems. In 2011, he was selected for Forbes' 30-Under-30 Science List. He formalized and worked to optimize verifiable computation, receiving a Best Paper Award (and later a Test-of-Time Award) at the IEEE Symposium on Security and Privacy for his advances. He coauthored a book on Bootstrapping Trust in Modern Computers, and his work in that area has been incorporated into the latest security enhancements in Intel CPUs. His research into security for new application models was incorporated into Windows and iOS and received Best Paper Awards at the IEEE Symposium on Security and Privacy and the USENIX Symposium on Networked Systems Design and Implementation. He then extended his interest in bootstrapping trust to the problem of building practical, formally verified secure systems, for which he received three Distinguished Paper Awards. Research Statement My research is primarily focused on investigating long-term, fundamental improvements in how to design and build secure systems. As a result, my work combines theory and practice to provide formal, rigorous security guarantees about concrete systems, with an emphasis on creating solid foundations for practical solutions. In the past, I have worked on topics such as network and system security, applied cryptography, usable security, and data privacy.Below are two of my long-running research directions, both focused on providing users with strong guarantees about the security of remote services.Securely Outsourcing Computation to the Cloud: From Cryptographic Theory to PracticeTo provide strong guarantees for outsourced computations, we developed a new cryptographic framework, Verifiable Computation, which allows clients to outsource general computations to completely untrusted services and efficiently verify the correctness of each returned result. Through improvements to the theory and the underlying systems over the last few years, we reduced the costs of verification by over twenty orders of magnitude. As a result, verifiable computation is now a thriving research area that has produced several startups, as well as enhancements to the security and privacy of X.509, MapReduce, and Bitcoin. We are continuing to explore improvements and applications in this space, as well as other settings where cryptographic advances can be deployed to create fundamentally more secure services.Building Provably Secure SystemsWhile verifiable computation provides strong guarantees, even the best cryptographic system is useless if implemented badly, applied incorrectly, or used in a vulnerable system. Thus, I have led a team of researchers and engineers in the Ironclad project (https://github.com/Microsoft/Ironclad), Everest project (https://project-everest.github.io/), and Verus project (https://github.com/verus-lang/verus), working to expand formal software verification to provide end-to-end guarantees about the security and reliability of complex systems. Many interesting challenges remain, including improving the performance of verifiers and verified code, and enhancing the stability of automated proofs. Nonetheless, I expect that verification will fundamentally improve the software that underpins our digital and physical infrastructure. Publications Chapter A Framework for Debugging Automated Program Verification Proofs via Proof Actions 2024 • Lecture Notes in Computer Science • 14681:348-361 Cho C, Zhou Y, Bosamiya J, Parno B Journal Article FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions 2024 • Proceedings of the ACM on Programming Languages • 8(OOPSLA2):499-526 Lin Z, Gancher J, Parno B Conference Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs 2024 • PROCEEDINGS OF THE 18TH USENIX SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION, OSDI 2024 • 837-853 Zhang TN, Hance T, Kapritsos M, Chajed T, Parno B Conference Algebraic Reductions of Knowledge 2023 • Lecture Notes in Computer Science • 14084:669-701 Kothapalli A, Parno B Conference FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores 2023 30-46 Arasu A, Ramananandro T, Rastogi A, Swamy N, Fromherz A, Hietala K, Parno B, Ramamurthy R
Chapter A Framework for Debugging Automated Program Verification Proofs via Proof Actions 2024 • Lecture Notes in Computer Science • 14681:348-361 Cho C, Zhou Y, Bosamiya J, Parno B
Journal Article FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions 2024 • Proceedings of the ACM on Programming Languages • 8(OOPSLA2):499-526 Lin Z, Gancher J, Parno B
Conference Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs 2024 • PROCEEDINGS OF THE 18TH USENIX SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION, OSDI 2024 • 837-853 Zhang TN, Hance T, Kapritsos M, Chajed T, Parno B
Conference Algebraic Reductions of Knowledge 2023 • Lecture Notes in Computer Science • 14084:669-701 Kothapalli A, Parno B
Conference FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores 2023 30-46 Arasu A, Ramananandro T, Rastogi A, Swamy N, Fromherz A, Hietala K, Parno B, Ramamurthy R