UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Mechanising blockchain consensus

Pîrlea, G; Sergey, I; (2018) Mechanising blockchain consensus. In: Andronick, J and Felty, A, (eds.) CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. (pp. pp. 78-90). Association for Computing Machinery (ACM): New York, NY, USA. Green open access

[thumbnail of toychain-accepted.pdf]
toychain-accepted.pdf - Published Version

Download (673kB) | Preview


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 modeled 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.

Type: Proceedings paper
Title: Mechanising blockchain consensus
Event: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018)
Location: Los Angeles, CA, USA
Dates: 07 January 2018 - 08 January 2018
ISBN-13: 9781450355865
Open access status: An open access version is available from UCL Discovery
DOI: 10.1145/3167086
Publisher version: http://dx.doi.org/10.1145/3167086
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: blockchain, consensus, protocol verification, Coq
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
URI: https://discovery.ucl.ac.uk/id/eprint/10038868
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item