Casper CBC in Isabelle
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).
(WIP) Properties of minimal transition 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.
(WIP) 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.
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). (WIP) Proved that GHOST is a valid estimator. (WIP) Proved that GHOST is a majoirty driven property. Basic lemmas
message_in_state_is_valid etc.
nrryuya.icon > To be added.
Bugs we found
Wrong claims
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?
not more than and less than
Code generation
Generated code of clique oracle
nrryuya.icon > As written in the above, proof of correctness of clique oracle is WIP.
(ToDo) Generated code of GHOST fork choice. (ToDo) Improvement of the generated code. 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.
Prove safety of estimate, not property
Simple definitions of a valid message / state
limited setting
No safety oracle
It also proved(?) the irreflexivity and transitivity of message justification using tran Future work
dominik.icon > will include this in the conclusion and keep it rather short -> contributions for the next paper
Formal verification
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