Bryan Parno
Office 2121 Mehrabian Collaborative Innovation Center
Email parno@cmu.edu
Phone (412) 268-2033
Department
Computer Science Department
Research/Teaching 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.