Fully Verified Outsourced Computation
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).