First ‘Provably Safe’ Ethereum PoS Protocol Highway has been allegedly demonstrated by Casper Labs. In a paper published by the company, it alleges that they have demonstrated the first crypto Highway and are asking people to check it out on their github repository.
Introducing the “minimal” CBC Casper Consensus Protocols
CBC Casper is a family of “correct-by-construction” consensus protocols that share the same proof of asynchronous, Byzantine fault tolerant consensus safety. We describe this family of protocols by defining their protocol states and protocol state transitions, and then we provide a proof of Byzantine fault tolerant consensus safety for the entire Minimal CBC Casper family of protocols. We give examples of members of this family of protocols, including a binary consensus protocol. “Casper the Friendly Ghost”, a blockchain consensus protocol, and a sharded blockchain consensus protocol. Each of these examples is “correct-by-construction” because the way they are defined guarantees that they are part of this family of protocols, and therefore satisfy the consensus safety theorem. This draft is intended to be introductory and educational, it is not a complete description of a system that can be implemented exactly as specified.
First ‘Provably Safe’ Ethereum PoS makes a greater case for Proof of Stake as a replacement for the proof of work method of validation.
From the Report
We present a concrete consensus algorithm based on zamfir2018 together with a criterion for finality, both proposed by Daniel Kane. This consensus algorithm is live in a partially synchronous network and has variable out-of-protocol finality thresholds each observer can choose independently, thus allowing individual tradeoffs between safety and liveness.
At the heart of the protocol are two design choices that keep it simple and intuitive:
There are no targeted messages sent only to specific nodes, like e.g. miller 2016, and no messages that contain a particular choice of other messages that the sender had received earlier, castro 1999 practical’s NEW-VIEW message. Instead, all messages are eventually delivered to everyone, and they attest to earlier messages; all nodes see the same, continuously growing graph of messages, similar to baird 2016.
Decisions are made using simple voting. Liveness is ensured by enforcing a particular structure in the graph that prevents stalemates from persisting.
In section 1 we introduce the basic concepts of messages, justifications and equivocations, and analyze the safety guarantees that can be derived from their structure so that we can determine in a general setting when consensus decisions are final, i.e. under some reasonable assumptions they cannot be reverted.
Section 2 provides an explanation about how these results can be applied to the specific use case of a blockchain.
In section 3, we introduce additional rules that guarantee not only safety, but also liveness; decisions can be relied on and are eventually actually made.
Finally, section 4 puts the abstract consensus algorithm in the context of a distributed proof of stake network, outlines how deposits, rewards and penalties can be handled, and addresses the problem of long range attacks.
So far we proved the desirable properties of the protocol under the assumption that a certain fraction of validators (by weight) is well-behaved. A real-world network’s security can approximately be measured in the cost of an attack: If I wanted to bribe the validators into reverting a finalized transaction or stalling the network, how much would I have to pay?
In a proof of stake network, these aspects are connected by making the weight proportional to a deposit — the validator’s stake — that is locked for a period beginning sufficiently long before the weight was assigned, and ending sufficiently long after it was unassigned. Incorrect behavior, as far as it can be determined objectively, is punished automatically by removing some amount from the deposit. Making stakes is incentivized by rewarding correct behavior.
All of this can be implemented as a smart contract running inside the system itself, with two special hooks:
The state of the smart contract determined by each block b (i.e. the result of executing the transactions in all of b’s ancestors including b itself) defines the weight function Wb after that block.
The system calls the smart contract in each block even if no user made a transaction interacting with it. In that call, the system provides the contract with information about validators’ behavior.
