Casper CBC: Formal verification

Runtime Verification

Elaine Li, Traian S,erb ̆anut, ̆a, Denisa Diaconescu, Grigore Rosu, VladZamfir

Target

Minimal framework

Safety

Non-triviality

Light client

Define validators as "Comparable" type

https://gyazo.com/7f3ec5373541145bc423befb66cf662c

StrictlyComparable contains:

a proof that there exists at least one witness of type X (inhabited)

a comparison operator which takes two elements of type X and returns either Lt, Eq or Gt (compare)

and a proof that this comparison operator imposes a strict ordering on elements of type X (compare_strictorder)

Abstract away messages from states, state transitions, fault weights

State

https://gyazo.com/e604bb9bca200f746130da5668685e24

Reachability of states

https://gyazo.com/dadc4088747465c2f14ff9f0845d9030

Fault weight

https://gyazo.com/755d4c0155de8a5e6e6c9a9db7ea55a9

nrryuya.icon > The decoupled "mutually recursive definition of states and messages" are only handled in the definition of full node and not in the safety and non-triviality proofs

Strong non-triviality

Non-triviality = the existence of a protocol property$ Pfor which there is a protocol state$ \sigma_1that is decided on$ Pand another protocol state$ \sigma_2that is decided on$ ¬P

"In our generalization efforts, we found that non-triviality precisely captures the notion of non-local confluence in the abstract rewriting system literature"

Strong non-triviality = for every protocol state s1, there exists a protocol state s2 that is s1’s next state and a protocol state s3 that is s1’s future state, such that s1 and s3 share a common future, but s2 and s3 do not

Proved by full/light node specification but not only by abstract definition

LayerX

Isabelle/HOL

Target

Minimal framework

Safety

State transition

(WIP) LMD GHOST

Simple finality detector

Previous work

CBC Casper binary consensus in Isabelle/HOL (2017 Mar) by pirapira

Trail of Bits

PlusCal and TLA+

Liveness without message delay