Bryan Parno

Bryan Parno, Faculty, Computer Science Department

Associate Professor

Office Room 2121 Mehrabian Collaborative Innovation Center

Email parno@cmu.edu

Phone (412) 268-2033

Department
Computer Science Department

Website
http://www.andrew.cmu.edu/user/bparno/

Administrative Support Person
Rosemary Battenfelder

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 Practice

To 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 Systems

While 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), working to expand formal software verification to provide end-to-end guarantees about the security and reliability of complex systems.  By creating a set of new tools and methodologies, Ironclad produced the first complete stack of verified-secure software.  We also recently developed the first methodology for verifying both the safety and liveness of complex distributed systems implementations.  Many interesting challenges remain, including verifying concurrent or probabilistic programs, 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.

Recent Publications

Bryan Parno ( 2022 ) ACM Transactions on Programming Languages and Systems, Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility , Vol.: 44 Issue: ( 2 )

Bryan Parno ( 2022 ) Proceedings of the ACM on Programming Languages, Linear types for large-scale systems verification , Vol.: 6 Issue: ( OOPSLA1 )

Tzialla I, Kothapalli A, Parno B, Setty S ( 2022 ) Transparency Dictionaries with Succinct Proofs of Correct Operation

Delignat-Lavaud A, Fournet C, Parno B, Protzenko J, Ramananandro T, Bosamiya J, Lallemand J, Rakotonirina I, Zhou Y ( 2021 ) Proceedings - IEEE Symposium on Security and Privacy, A security model and fully verified implementation for the IETF QUIC record layer Vol: 2021-May , Page(s): 1162 - 1178