Portrait of Bryan Parno

Bryan Parno



I joined the Security and Privacy Research Group here at Microsoft Research in 2010.  I am interested in a broad range of security topics (e.g., network and system security, applied cryptography, usable security, and data privacy), as well as topics such as operating system design, distributed systems, and mobile computing.

My current work focuses on protocols for verifiable computation and zero-knowledge proofs, building practical, formally verified secure systems, and developing next-generation application models.  I have been fortunate to work with many excellent interns, including Ben Kreuter, Karthik Nagaraj, Mariana Raykova, Joshua Schiffman, Srinath Setty, Sai Deep Tetali, Xi Xiong, and Samee Zahur.

I completed my PhD at Carnegie Mellon University under the supervision of Adrian Perrig.  My dissertation studies the design, implementation, and evaluation of a combination of hardware, software, and cryptographic primitives for extending the trust you have in one service or device in order to allow you to trust other services and devices.  My dissertation won the 2010 ACM Doctoral Dissertation Award.

Earlier in my career, I studied computer science at Harvard University.


  • September 20, 2016 – A nice overview article of recent progress in verification.
  • February 2, 2016 – I’ve been invited to give a talk at the Formal Methods for Security (FMS) Workshop, which is co-located with PLDI.  Please consider attending!
  • December 15, 2015 – I’ve been invited to give a talk at the Layered Assurance Workshop in Los Angeles, on December 5-6, 2016.  Please consider attending!
  • October 4, 2015 – The source code for IronFleet, our system for verifying the safety and liveness of complex distributed systems, is now on GitHub.
  • September 9, 2015 – I’ve been invited to give a talk at the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) in January.  I’ll be discussing our Ironclad project and some of the interesting research questions we’ve uncovered in trying to verify large, complex systems.  Please consider attending!
  • July 22, 2015 – The source code for Geppetto, our system for improving the versatility and performance of verifiable computations, is now online.
  • July 24, 2014 – ACM published my book, Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers, as part of their new ACM Books series.
  • May 21, 2013 – Our paper, Pinocchio: Nearly Practical Verifiable Computation, received the Best Paper Award at the IEEE Symposium on Security and Privacy.
  • April 3, 2013 – Our paper, Embassies: Radically Refactoring the Web, received the Best Paper Award at the USENIX Symposium on Networked Systems Design and Implementation (NSDI).
  • March 26, 2013 – I’ll be co-chairing CCSW this year — please consider submitting.
  • March 12, 2013 – I’ll be giving a plenary talk at ACNS this summer — please consider attending.
  • May 22, 2012 – Our paper, User-Driven Access Control: Rethinking Permission Granting in Modern Operating Systems, received the Best Practical Paper Award at the IEEE Symposium on Security and Privacy.
  • December 19, 2011 – I was selected for Forbes’ 30-Under-30: Science list.
  • August 30, 2011 – Our book, Bootstrapping Trust in Modern Computers, has been published.  It can be purchased from Springer or Amazon.
  • May 11, 2011 – My dissertation won the 2010 ACM Doctoral Dissertation Award!



Established: October 2, 2014

An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation…

Verifiable Computing

Verifiable computation schemes enable a client to outsource the computation of a function F on various inputs to an untrusted worker, and then verify the correctness of the returned results. Critically, the outsourcing and verification procedures must be more efficient…

Dafny: A Language and Program Verifier for Functional Correctness

Established: December 23, 2008

Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative,…