Playing consensus scenarios on Tenderbake with Mitten

Tezos Blockchain Consensus PBFT Tenderbake Testing
Published on 2022/04/27
Playing consensus scenarios on Tenderbake with Mitten

What is Mitten

The design and implementation of consensus algorithms, one of the main components of blockchains technology, is a very challenging and complex task. Indeed, one must consider many parameters to ensure soundness and liveness, such as the ratio of tolerated Byzantine actors, desynchronization of participants, and delays or loss of messages on the network. Moreover, covering subtle corner cases of a given implementation might be hard to achieve when stress-testing.

In a previous work, we modeled Tenderbake --- the new consensus protocol of the Tezos blockchain --- as a state machine and wrote it in TLA+. While this high-level overview allows us to concentrate reasoning on the algorithm's core by abstracting some implementation details, it becomes tough to convince ourselves that the existing implementation follows the lines of the inferred model. In fact, given a test scenario, it is challenging to create the conditions and simulate the desired transitions to stress the corresponding implementation.

To finely describe and play scenarios on Tenderbake, we developed Mitten: a tool that acts as a man-in-the-middle proxy between a set of nodes of a (test) network. It is configurable to filter and examine messages according to given scenarios written in a DSL built on OCaml. Mitten allowed us to write and simulate subtle scenarios to reproduce behaviors that are difficult to exhibit under normal circumstances. We were also able to simulate situations that allowed us to test proposed improvements and fixes.

If you are interested in more details about Mitten, we invite you to watch this presentation at the NL research seminar.

Mitten presentation at NL research seminar

Additional resources