Speaker: Karl Palmskog, Researcher, KTH Royal Institute of Technology, Sweden  

Title: Formal Verification of Blockchains: From Consensus to Code

Abstract:

To ensure trustworthiness of cryptocurrency systems, application of formal verification is needed at every abstraction level - from the idealized consensus protocol level down to the low-level code running at individual network nodes. In this talk, I will describe some recent work that spans across several of these abstraction levels.

First, I will describe an initial abstract formal model of the Algorand consensus protocol, developed in collaboration with the protocol designers. Algorand is a pure proof-of-stake protocol based on cryptographic self-selection of committee members who vote on blocks. The model is encoded as a transition system in the Coq proof assistant that includes adversary actions. So far, we have proved the protocol's asynchronous safety - only a single block can be added in a protocol round - assuming symbolic (Dolev-Yao) cryptographic primitives.

Second, I will outline an experimental implementation of Bitcoin-like cryptocurrency system, unrelated to Algorand, verified for consensus and integrity by continuous refinement. Specifically, starting from a generalized variant of the abstract blockchain model in Coq called Toychain (CPP '18), we derived a concrete blockchain specification in the Dafny program verifier which we implemented and verified in Dafny's imperative language. By exporting the verified code to C# and performing some additional (unverified) refinements and adding a network shim, we obtained an executable system reminiscent of Bitcoin. We experimentally compared our system's performance to the reference Bitcoin implementation, with some encouraging results. I will conclude with some ideas on how the still considerable performance gap to the reference implementation may be narrowed in future work.

Based on joint work with many colleagues at Runtime Verification, Inc., University of Illinois at Urbana-Champaign, and Algorand, Inc.

About the Speaker: Karl Palmskog is a Researcher in the Secure and Trustworthy Execution Platform group at KTH Royal Institute of Technology in Stockholm, Sweden, working on formal verification of system software. He was previously a postdoc at The University of Texas at Austin and University of Illinois at Urbana-Champaign. His research interests include proof engineering and reasoning about distributed systems based on consensus, such as blockchains, using proof assistants. He obtained his PhD from KTH in 2014. His recent work is listed on https://setoid.com

About the Seminar: The COBRA Seminars are weekly seminars hosted by COBRA. The seminars are open to everyone with an interest in blockchain