Casper CBC in Isabelle
GitHub LayerXcom/cbc-casper-proof
Kanban
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
Safety / liveness proof of consensus algorithm (See Safety & liveness of consensus algorithm)
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
How faults are handled in CBC framework? (See Casper CBC: Others)
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
See Casper CBC: State 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.
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).
(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
M isn't always strict subset of C × V × Σ (not reported yet)
Proved the counterexample of this.
Wrong definitions
Fix the type signature of Later_From #24
Fix the type signature of estimator #23
Fix the definition of the epoch score function #20
"Blocks_In" is not defined #22
Mistakes in proofs
Remove redundant parenthesis in definition 4.10 #18
Add some missing cardinality notations in the proof of Lemma 8 #21
Small fixes in words and sentences
Modify a word "prevblock" to "previous block" #19
Replace a period in a sentence with a comma #25
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
Review for the draft of section 7 (safety oracle)
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
See Formal verification of distributed algorithm
Verdi
Verdi, Raft in Coq
Section 7 is about proof engineering
Velisarios (pBFT in Coq)
Proof assistants and blockchain consensus
Toychain
PoW oriented
Only quiescent(?) consistency
Formal verification of FFG in Coq
Reusing definitions of Toychain
Proof of simple safety & liveness
Simple proof of Casper CBC in Isabelle (Yoichi Hirai, 2017)
GitHub Repo, Blog post
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
Prove safety of estimate, not property
Simple definitions of a valid message / state
limited setting
tie_breaking assumption
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
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