Verification of consensus algorithms

Tutors: Lacramioara Astefanoaei, Philippe Bidinger, Eugen Zalinescu

Description

At Nomadic Labs, we all contribute to the Tezos blockchain platform. Tezos is mostly written in OCaml. Thus by design, Tezos offers better safety guarantees. This is thanks to the OCaml robust static type system and memory management which help rule out potential runtime errors.

At the heart of the Tezos blockchain (and of any other blockchain more generally), there is a consensus algorithm. Its role is to ensure that all participants agree on a common blockchain.

One of the distinguishing features of Tezos is that it is self-amending. This means that the Tezos rules can be changed through a voting procedure. As the consensus protocol itself is part of these rules, it can be changed this way. Consequently, the self-amending mechanism makes Tezos appealing as a test bed for experimenting with different consensus algorithms making it possible to analyze the strengths, weaknesses, and suitability of different approaches in the blockchain context.

All this is great and it would be even greater if we could verify a priori the candidate consensus algorithms. Some consensus algorithms have already been verified to some extent. Some notable, successful verification efforts are:

Goals

The main goal of this internship is to model and verify a classical BFT consensus algorithm for blockchains such as HotStuff in the presentation of Gotsman et. al6 with one or two verification tools, such as TLA+7, Asphalion8, Uppaal9, Maude10, Psync11. The findings, most notably the strengths and the limitations of the chosen tools, will be documented in a report.

Requirements

You should be curious to explore the subject of consensus verification and enjoy experimenting with various verification tools.

Internship Context

You will work at the Nomadic Labs' offices in Paris or Grenoble.

Participating in a large scale open-source project you will have to rapidly learn to use collaborative tools (Git, merge request, issues, gitlab, continuous integration, documentation) and to communicate about your work. The final results might be presented at an international conference or workshop.

You will have a designated advisor at Nomadic Labs and will have to work independently and to propose thoroughly-considered solutions to the different problems you will have to solve. You will be encouraged to seek advice from members of the team.

Intellectual Property

All material produced (essays, documentation, code, etc.) will be released under an open source license (e.g. MIT or CC).