Mon 8 Jan 2018 14:30 - 15:00 at Museum A - Verified Applications Chair(s): K. Rustan M. Leino

We present the first formalisation of a blockchain-based distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant.

Our development includes a reference mechanisation of the block forest data structure, necessary for implementing provably correct per-node protocol logic. We also define a model of a network, implementing the protocol in the form of a replicated state-transition system. The protocol’s executions are modelled via a small-step operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated.

In this work, we focus on the notion of global system safety, proving a form of eventual consistency. To do so, we provide a library of theorems about a pure functional implementation of block forests, define an inductive system invariant, and show that, in a quiescent system state, it implies a global agreement on the state of per-node transaction ledgers. Our development is parametric with respect to implementations of several security primitives, such as hash-functions, a notion of a proof object, a Validator Acceptance Function, and a Fork Choice Rule. We precisely characterise the assumptions, made about these components for proving the global system consensus, and discuss their adequacy.

All results described in this paper are formalised in Coq.

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

13:30 - 15:30: Verified ApplicationsCPP at Museum A
Chair(s): K. Rustan M. LeinoAmazon
13:30 - 14:00
Talk
Mechanising and Verifying the WebAssembly Specification
CPP
Conrad WattUniversity of Cambridge, UK
DOI
14:00 - 14:30
Talk
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
CPP
Sidney AmaniUNSW, Australia, Myriam BégelENS Paris-Saclay, France, Maksym Bortin, Mark StaplesCSIRO, Australia
DOI
14:30 - 15:00
Talk
Mechanising Blockchain Consensus
CPP
George PîrleaUniversity College London, Ilya SergeyUniversity College London
DOI Pre-print
15:00 - 15:30
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
CPP
Cezary KaliszykUniversity of Innsbruck, Julian ParsertUniversity of Innsbruck, Austria