Introducing CasperLabs Highway, The First Specification for a Provably Live and Secure CBC Casper Protocol

In consensus protocol literature, there are two critical security properties: safety and liveness. A protocol is safe if it will not make inconsistent decisions. A protocol is live if it is guaranteed to eventually make a decision. Making proof-of-stake (PoS) both safe and live for a decentralized network isn’t easy. One of the first breakthroughs to address these issues was published in a research paper titled “CBC Casper” by Ethereum Researcher Vlad Zamfir. While this initial research on the correct-by-construction (CBC) Casper family of protocols provided a leading-edge framework to address safety, it did not address liveness.

At CasperLabs, we have not only been researching on imminent issues around scalability and energy consumption, but have also been extending on Vlad Zamfir’s existing CBC Casper research to push the boundaries of our industry together.

Today, we are very excited to introduce CasperLabs Highway, the first specification for a provably live and safe consensus protocol within the CBC Casper framework.

We are releasing the protocol specification free to the community under an open-source license. The complete research paper is also available here.

Why CasperLabs Highway is Significant

Highway extends CBC Casper research in two ways.

First, the consensus protocol provides a novel, efficient way of detecting safety at different thresholds.

Second, Highway provides the first-ever specification for a liveness strategy in the CBC Casper framework. In other words, Highway prescribes a strategy for when participants in the network should create protocol messages and proves that the strategy results in the protocol being live.

How CasperLabs Highway Works

Highway utilizes an innovative approach that offers a new “summit” construction for finality which consist of “levels” of agreement. In order to effectively achieve liveness, the design uses a pseudorandom leader sequence with a dynamic round length system.

To understand how this works, let’s start with a simplified model. Time is divided up into rounds; during each round there is a leader who starts the message production. Others wait until they receive the leader’s message, before producing one themselves. Then, near the end of a round everyone sends another message. At each stage another level of agreement is being produced, eventually leading to a summit which can be considered a decision.

However, fixed length rounds are not practical in real systems, so in Highway we make them dynamic. To achieve this, we imagined a literal highway (well, a mathematical highway). On this highway, movement takes place in the form of hops, while the speed of all cars is constant. In any given lane n a car makes 2^n hops on a distance of one meter. Therefore, if you switch to the lane on your left, you increase the frequency of hopping x2. If you switch to the lane on your right, you decrease the frequency x2. Cars from the lane on your left meet you at every jump you make, and cars on your right meet you only every second hop. These “hops” are ticks, and each “meter” a round passes. Thus, the length of a round depends on what lane you are in.

By releasing CasperLabs Highway to the public via an open source license, we hope to inspire further innovation for the benefit of all.

We want your feedback — the good and the “ugly.” As an industry, we need discourse of ideas and critical analysis so we can all move forward together. Working together, we believe we can solve our industry’s challenges and help blockchain networks achieve widespread adoption for businesses and consumers.

Stay up-to-date with what we’re building by following us on our Twitter.If you have any questions, you can join the conversation with our development team on our Discord.