Fully Verified Outsourced Computation

Frequent headline-grabbing data breaches suggest that current best practices for safeguarding personal data are woefully inadequate.  To try to move beyond the cycle of attacks and patches we see today, I design and build systems with formal end-to-end guarantees.  For example, to provide strong guarantees for outsourced computations, I 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, 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.

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, 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. While interesting challenges remain, I expect that verification will fundamentally improve the software that underpins our digital and physical infrastructure.

Bryan Parno is a Researcher in the Security and Privacy Group at Microsoft Research.  After receiving a Bachelor's degree from Harvard College, he completed his PhD at Carnegie Mellon University, where his dissertation won the 2010 ACM Doctoral Dissertation Award.  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 at the IEEE Symposium on Security and Privacy 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 received a Best Paper Awards at the IEEE Symposium on Security and Privacy and the USENIX Symposium on Networked Systems Design and Implementation.  He has recently extended his interest in bootstrapping trust to the problem of building practical, formally verified secure systems. His other research interests include user authentication, secure network protocols, and security in constrained environments (e.g., RFID tags, sensor networks, or vehicles).