CS Talk - Bryan Parno
Title: Fully Verified Outsourced Computation
Host: Joan Feigenbaum
Coffee/tea - 10:15, BCT MC035
Abstract:
Today, when a client submits her personal data to a remote service, she has little assurance that the service will perform as expected or that her data will remain secure. Sadly, frequent headline-grabbing data breaches suggest that current best practices are woefully inadequate, especially as computers permeate ever more aspects of our daily lives.
To provide strong, formal 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 concrete costs of verification by over twenty orders of magnitude, bringing this research area to the threshold of practicality. As a result, verifiable computation is now a thriving area of research that has produced several startups, as well as proposals to enhance the security and privacy of X.509, MapReduce, and Bitcoin.
While verifiable computation provides strong, mathematical guarantees, even the best cryptographic system in the world is useless if implemented badly, applied incorrectly, or used in a larger, vulnerable system. Thus, over the last three years I have led a large team of researchers and engineers in the Ironclad project, working to push the boundaries of formal software verification in order to fully verify the security and reliability of complex systems. By developing a set of new tools and methodologies, Ironclad produced the first complete stack of verified-secure software, including a verified kernel, verified drivers, verified system and cryptographic libraries, and four exemplar applications. We also recently produced the first methodology for verifying both the safety and liveness of complex distributed systems implementations. The Ironclad applications have performance comparable to unverified systems, demonstrating that verification is compatible with practicality. While interesting challenges remain, I expect that verification will fundamentally improve the software that underpins our digital and physical infrastructure.
Bio:
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. 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).