Casper CBC in Isabelle

NOTE: This is an early draft of this paper

----------------------------------------------------------------------------------------------------------------------------------------------------

GitHub LayerXcom/cbc-casper-proof

Desigin

Make this papar "standalone" as possible, not just a "translation from the paper to Isabelle"

Express our original findings & achievement

Tereminology

The original paper (Introducing the “Minimal CBC Casper” Family of Consensus Protocols): "the CBC Casper paper" (?)

Introduction

Background on consensus algorithm

Nakamoto, PoS, Casper FFG etc.

CBC Casper

CBC framework is flexible approach to create a family of consensus protocols, not limited to a certain fork choice rule, even blockchain.

Motivation for formal method

Proof based on formal method

Our contributions

Mathematical refinement of CBC framework

Formal verification of CBC framework

Code generation

CBC Casper

Description of CBC Casper

"Correct-by-construction" (CBC) approach

CBC framework allows to create consensus algorithm from binary consensus to blockchain consensus by defining CBC paramerters

Asynchronous safety for any properties

Model (state, message)

A fork choice rule (an estimator, in CBC lingo) is "forced" i.e. every message from other validators are checked whether the consensus value it proposes are the correct result of execution of the estimator.

Fault

Asynchronous safety

Abstract safety + safety oracle

No "byzantine fault threshold" in protocol

Mathematical refinement of CBC framework

Message justification

We captured message justification$ m_1 \preceq m_2 \Leftrightarrow m_1 \in Justification(m_2)as binary relation.

We proved $ (\preceq, M)is a strict partial order and well-founded.

We proved that if$ vis not equivocating, $ (\preceq, From\_Sender(v, \sigma))is well-ordered.

State transition

The binary relation$ (\rightarrow), \Sigmais a partial order (just a set inclusion).

Formal verification of CBC framework

Proof engineering

Usage of locale to express CBC Casper params

XXX_types lemmas which represents the type system of CBC Casper

NOTE: Isabelle doesn't have dependent types

Verified theorems & properties

Asynchronous safety

We proved all theorems & lemmas in the section 2 & 3 in the original paper.

Properties of latest messages

Lemma 10 (Observed non-equivocating validators have one latest message).

This is a whole replacement of the section 4.1 of the original paper.

The incorrect ness of section 4.1 is already pointed out by someone (Lemmas 6 and 9 should be formulated differently. #14).

GHOST

More realistic definition of GHOST.

With the GHOST estimator in the original paper, there will be no block other than the genesis block$ g (discussion in gitter).

Basic lemmas

message_in_state_is_valid etc.

nrryuya.icon > To be added.

Bugs we found

Wrong claims

M isn't always strict subset of C × V × Σ (not reported yet)

Proved the counterexample of this.

Wrong definitions

Mistakes in proofs

Small fixes in words and sentences

The Top Letters of All Words are capitalized or The top letters of only the first Word are capitalized?

Code generation

Generated code of clique oracle

nrryuya.icon > As written in the above, proof of correctness of clique oracle is WIP.

Comparison to other works

Formal verification of distributed algorithm

Verdi

Section 7 is about proof engineering

Velisarios (pBFT in Coq)

Proof assistants and blockchain consensus

PoW oriented

Only quiescent(?) consistency

Reusing definitions of Toychain

Proof of simple safety & liveness

Simple proof of Casper CBC in Isabelle (Yoichi Hirai, 2017)

Weak abstraction (no "params")

Two-party, binary consensus

(Therfore) no concept of "fault threshold$ t"

Both of two validators are not equivocating.

consisent_view is used for this assumption.

Only max weight estimator

tie_breaking assumption on weight

Prove safety of estimate, not property

Simple definitions of a valid message / state

No safety oracle

It also proved the transitivity and asymmetry of message justification using transitive closure

Future work

dominik.icon > will include this in the conclusion and keep it rather short -> contributions for the next paper

Formal verification

Safety oracle in the draft of Section 7

Liveness

Validator lotation

CBC Sharding

From protocol specifications to implementation

Practical specifications of CBC client and the formal verification of it in Isabelle

More code generation works

Mesurement of performance