Formal Verification of Consensus Algorithms

Blockchain

Nakamoto consensus

The proved property: blockchain integrity, i.e., that additions to the blockchain are guaranteed to be persistent.

Similar to common prefix

Consideration of attackers

Max DiGiacomo-Castillo, Yiyun Liang, Advay Pal, John C. Mitchell (Stanford)

UPPAAL-SMC

Analyzing Selfish mining

Ouroboros

Forkable Strings of ouroboros paper in Isabelle/HOL

Kawin Worrasangasilpa

psi calculus: a generalization of the pi calculus with more advanced features

we can embed (shallow-embedding?) it as a domain-specific language (DSL) in Haskell and:

both execute and run (it’s just Haskell after all)

test using QuickCheck (Haskell’s randomized testing tool)

do formal verification using the psi calculus metatheory.

Søren Eller Thomsen and Bas Spitters

Safety and Liveness of a protocol similat to Ouroboros Praos

Casper FFG

Runtime Verification

Based on Toychain

Verification of previous version of Casper FFG with Isabelle by Yoichi Hirai

Alloy, Isabelle

Runtime Verification

CBC Casper

Algorand

GitHub by Runtime Verification

Stellar Consensus Protocol

Verification with Isabelle and Ivy

Formalizes some definitions and proofs of the Stellar whitepaper and a simpler take on federated voting in Isabelle

Formalizes and proves safety of the ballot protocol in Ivy

Junghun Yoo (University of Oxford) et al.

Stellar Consensus Protocol in UPPAAL

Pierre Tholoniat (University of Sydney), Vincent Gramoli (University of Sydney)

Verify Two components of Red Belly Blockchain using the ByMC model checker

1. A simple broadcast primitive

2. A blockchain consensus algorithm written in 309

Others

Formal verification of fairness of the Tendermint proposer election algorithm

GitHub, Idris

Traditional BFT

Velisarios

ESOP'18

Vincent Rahli et al. (University of Luxembourg)

A logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols

Extends the Logic of Events (LoE) in order to reason not only about crash faults, but also about arbitrary faults.

In LoE, an event is an abstract entity that corresponds either (1) to the handling of a received message, or (2) to some arbitrary activity about which no information is provided.

As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT. (See Velisarios/PBFT)

proved only safety

ref: a survey paper by the author An Ecosystem for Verifying Implementations of BFT protocols (Ivana Vukotic et.al)

https://gyazo.com/4d01242baf866458468d6f205f68e6b6

Others

Develop a methodology for deductive verification of thresholdbased distributed protocols using decidable logic

Decomposition into two well-established decidable logics

Implemented with Z3 and CVC4

Verified Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos

Traditional CFT

Verdi

A framework for formally verifying distributed systems implementations in Coq

Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas Anderson (University of Washington, USA)

cited 118

Contribution from Karl Palmskog

Verdi Raft

proved only safety

Verdi currently supports verifying safety properties, but not liveness properties, and none of Verdi’s network semantics currently capture Byzantine fault models. We believe that Verdi could be extended to support these features: liveness properties could be verified by supporting infinite traces and adding fairness hypotheses as axioms as in TLA, while Byzantine fault models can be supported by adding more non-determinism in the network semantics.

Verdi Chord

DISEL

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Ilya Sergey (University College London, UK)

James R. Wilcox, Zachary Tatlock (University of Washington, USA)

Contribution from Karl Palmskog

Example of Two-phase commit

Ivy

Multi-Paxos, Raft

Deductive verification based on effectively propositional logic (EPR)

A decidable fragment of first-order logic (also known as the Bernays-Schönfinkel-Ramsey class).

The finite model property, allowing to display violations as finite structures which are intuitive for users.

Modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check.

The steps of the transformations are also mechanically checked, ensuring the soundness of the method

Paxos and its variants

Implemented in Ivy

EventML

Vincent Rahli (Cornell University)

A language for implementing distributed systems

Nicolas Schiper Vincent Rahli Robbert Van Renesse Mark Bickford Robert L. Constable (Cornell University)

from Verdi Raft's paper

EventML programs can be verified in NuPRL using the Logic of Events.

EventML and the Logic of Events have been used to verify an implementation of Multi-Paxos, a total-order broadcast service, used as part of a distributed database

IronFleet

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill (Microsoft Research)

cited 134

TLA-style state-machine refinement and Hoare-logic verification (Dafny, an SMT-based program verification toolchain)

from Verdi Raft's paper,

This approach enables building practical distributed systems and proving both safety and, unlike our Raft proof in Verdi, liveness properties.

Also unlike our Raft implementation in Verdi, IronFleet’s implementation of Paxos supports many important practical features including verified marshaling and parsing, state transfer, and log truncation

Head-Of model

Bernadette Charron-Bost (Ecole polytechnique), Andr´e Schiper (EPFL)

Henri Debrat (Universit´e de Lorraine & LORIA) and Stephan Merz (Inria Nancy Grand-Est & LORIA)

Formalize Heard-Of model in Isabelle/HOL the

HO model can represent algorithms that operate in communication-closed rounds, which is true of virtually all known fault-tolerant distributed algorithms.

Both safety and liveness

Extenstion for Byzantine faults

Martin Biely (TU Wien) et al.

DSL based on Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages

Paxos

Does not deal with Byzantine faults

Ognjen Maric, Christoph Sprenger, and David Basin (ETH Zurich)

Ognjen Maric, Christoph Sprenger, and David Basin (ETH Zurich)

Define a language ConsL, capable of expressing numerous consensus algorithms (Paxos, Chandra-Toueg, Ben-Or etc.)

Leverage model checking to provide the first fully automated decision procedure applicable to a range of consensus algorithms (Promela/Spin)

Other Isabelle/HOL works

From TLA+ specification to Isabelle

Model checking of traditional protocols

TLA+

Two-phase commit Slide

Paxos

Leslie Lamport

SPIN

Paxos

Giorgio Delzanno et.al.

SMV

Non-probabilistic Verification: the verification of Validity and Agreement and the non-probabilistic arguments for proving Probabilistic wait-free termination using Cadence SMV

Probabilistic Verification: the verification of the probabilistic arguments for proving Probabilistic wait-free termination using PRISM

Related/Others

Miguel Castro (MIT)

Formal proof of safety and liveness of pBFT using I/O automata

Emmanuelle Anceaume (IRISA) et al.

Bitcoin, GHOST, Byzcoin, Algorand, PeerCensus, Red Belly

Yoichi Hirai