# Proposal: BFT protocol that can mutate its operator set in a byzantine setting

**URL:** <https://community.obol.org/t/proposal-bft-protocol-that-can-mutate-its-operator-set-in-a-byzantine-setting/106>\
**Category:** Research\
**Tags:** Nethermind\
**Created:** [December 16, 2023, 8:31pm UTC](https://community.obol.org/t/proposal-bft-protocol-that-can-mutate-its-operator-set-in-a-byzantine-setting/106 "2023-12-16T20:31:43Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Michal](https://avatars.discourse-cdn.com/v4/letter/m/34f0e0/32.png) [@Michal](https://community.obol.org/u/Michal)\
**Post date:** [December 16, 2023, 8:31pm UTC](https://community.obol.org/t/proposal-bft-protocol-that-can-mutate-its-operator-set-in-a-byzantine-setting/106/1 "2023-12-16T20:31:43Z")

</div>

Author: @olegjakushkin

## Task

Identify a BFT protocol that can mutate its operator set in a byzantine setting. In other words describe DV cluster states and transitions – allow the Obol operator’s cluster to add and remove operators, efficiently start and exit validators or stop the cluster.

## Background

Obol Charon’s framework was built around a lock file, which defined the state of system participants. This static setup has been effective in the past. However, we now face the challenge of adapting this system to allow for flexible modifications to the cluster without causing disruptions to the ongoing operations.

## Problem Statement

In Obol, we group sets of participants into clusters. Their stability and efficiency are paramount. A significant challenge in such a setting is managing the dynamic state of the DV cluster hosted on top of Byzantine Fault Tolerant (BFT) protocols. How do we keep the system state moving while performing operations requiring a complicated setup? How do we allow new members to join and leave while clearly understanding the DV state?

So the Problem Statement is to describe cluster communication rules as well as the cluster state model so that the DV cluster would behave predictably and never lock concerning given constrains (here by “lock” we mean cases when required operations order gets confused due to operator disagreement or operations ordering issues).

## Challenges

1. BFT does not save individual nodes from dis-coordination - multiple nodes can try to propose different mutations to be initiated. E.g., we started adding a validator and suddenly understood we needed to ban an operator as it is not responsive due to our state model. Thus, this document aims to cover “no going back when started” **composite mutation attacks by nodes breaking the mutation sequence** rules and halting cluster state progression, meanwhile changing the set of operators leading to the mutation having to be dropped altogether.
2. Initial Obol research on this topic assumes that some of the state changes can be done by individual operator signing. This can lead to a single node gaining the ability to halt a cluster. Thus we will investigate such halting and possible state change rules that can prevent cluster halting. This is different from (1) in the way that an attack here is a willing full-actor action on an ongoing composite mutation.
3. Current obol research on potential system state changes needs to define exit strategies for validators, operators, and clusters. This means that currently, the only mechanism for operator exit is an Operator Ban that removes system potential for clear consensual node exit and can, in the future, lead to the **system’s inability to impose and distinguish bad actors from good ones**.

## **Proposed solution**

### State model

We expend Obol state model from Obol Design Doc that already uses composite mutations to support cluster exit, validator stopping:

 ![Untitled](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/c53503c6e4ccd99f04eb3660eea22d0e805eeba8.png)

### Consensus game rules:

We add the following rules to respect the nature of synchronised distributed state changes:

1. There shall be only one of each composite mutation type running in parallel. Each running composite mutation shall have its timestamp+UUID (unique id for cluster definition) synchronised across the operator set. A particular implementation may use other composite mutation tracking against the distributed state over time logic, here only the principal idea of knowing all running composite mutation types matters.
2. Any successful composite mutation (one that has enough signatures on each mutation it is composed of and has no invalidation or cancelling mutation happening) of the operator set cancels and declines all other running mutations (for example, by timestamp+UUID providing a cut off on the DAG).

As in BFT, there is always a leader proposing the state update. We assume that mutations that are single-user state updates can be

1. Provided by the node when it becomes a leader. Here, we assume BFT implementation to be reliable for state agreement and consistency between nodes, with the leader receiving information on if his proposal was not agreed to (due to time frame or quorum disagreement).
2. Or sent to a leader as a request if selected BFT flavour or other architectural challenges make it hard for a node to be a leader.

For an external observer, these composite mutation state-changing mechanisms can look like a set of operations, each running in a loop, yet as we allow only one composite mutation of each type at the same time, the resulting system state changes are:

1. Easily manageable, one can always
  1. view all currently running mutations,
  2. update operators set via banning or voluntary exit in parallel with other running mutations,
  3. cancel outdated running mutations if needed by submitting new mutation that is part of a composite mutation of the same type making previous composite mutation irrelevant (as we have only up to one composite mutation type running at the same time).

2. State evolution can be easily stored in external monitoring solutions and tracked over time in a nearly linear fashion

### Model formal verification

We test the proposed model, recreating it using the formalism of the Petri network (PN) model with inhibitor arcs. To allow needed complexity, we devise a set of PN component blocks that we later interconnect together where each one can be verified separately for reachability and lockability. (described in Appendix A).

Each composable mutation can be defined similarly to this “Change Operators” one:

 ![Untitled 1](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/a60de56d2fb804a13578ee7f46800be94731490a.png)

And simplified into a set of main actions:

 ![Untitled 2](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/f845685428ad7dd5c1cbb64b0faa29e40a7c2d16.png)

Overall system model as a **Distributed System state machine** modeled from PN components (notation as on the figures above):

 ![Untitled 3](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/40741357fe699061acfa2526ce3c90cf09ea77ef.png)

Here we can change validators and operators set; have validators enabled or disabled, stop cluster gently after exiting all validators.

Model was described in .net format verifiable by common PN verification tools an was verified and tested using opensource [SMPT](https://github.com/nicolasAmat/SMPT) tool (which ”won a bronze medal in the “reachability” category of the Model Checking Contest 2022, an international competition of model checking tools for the verification of concurrent systems. It also obtains the 100% confidence award.”).

Resulting state model addressing certain aspects, such as the consensual removal of nodes looks like this (on top level each state is a result of one or more mutations):

| Action \ Requirements | All/Quorum/Single Affirm | Description |
| --- | --- | --- |
| Create cluster | all | Setting up a new DV cluster. Every member or entity that will be part of this cluster needs to participate or consent to its creation. |
| Change operators | quorum old, all new | altering the set of operators who have the authority to manage and control the cluster |
| Add validators | all | Register validator within operators set for control and duties performance |
| Stop Validator | quorum | Exit validator |
| Update/Add cluster metadata | quorum | Modifying or adding new information to the cluster’s metadata, such as configuration details |
| Update/Add operator metadata | single | Operators can update their own metadata, such as contact details or specific settings |
| Rotate node identity | quorum | Changing a node’s identity, like updating cryptographic credentials |
| Cluster Exit | quorum | This process ensures orderly and consensual disbanding or restructuring of the cluster. |

Note that a quorum of operators generates deposit data, and the principal provider activates the validator using this deposit data so in real life this happens out of the scope of BFT consensus state while here we add or remove validators to operators within our model.

## Drawbacks of the proposed solutions:

Also as some of the decisions happen off-chain there is a potential for deadlocks caused by issues of quorum aggregation (as some synchronization happens in the background in off-chain channels as described in the Task statement). This can especially arise on every action that requires “All” to sign instead of “Quorum”, note that in some of the actions, we should assume only Quorum and newer be able to check for “All”. Thus a recommendation can be made to demote operations currently set requiring all nodes to synchronise to only the quorum subset, or use only BFT implementations where a check for All to consent is available.

State model can not provide additional guarantees on top of those provided by the general application of the BFT+DAG consensus algorithm utilized underneath in terms of resistance to Byzantine nodes.

Created model assumes state model is eventually consistent and messages are delivered in uncorrupted form.

## **Results:**

In the presented model, we:

1. Proposed solution for banning an operator when a composed mutation has started
2. Introduced rules allowing to control of individual operators signing state-updating mutations
3. Defined exit strategies for the state model

We have a formalised, generalized model of **BFT Consensus-based State Change using Petri Networks**

We can now model readability and deadlock for a wide set of system flow graphs based on BFT consenting (or declining nodes)

We gathered a complete states graph model including Validators and Operators Exiting and Cluster termination

## Appendix A: Components of Petri Network

We want to be able to model this solution as a Formal model. Thus we developed a conceptual framework and code for the generation of our network description in Petri Networks with inhibitor arcs .net language. We consider the implementation of:

- Composite mutations (with up to one of each type running concurrently)
- Set of Operators that elect a leader and who create a decision of what operation to partake in (DV BFT cluster)
- A set of Validators that can be considered activated or deactivated during the DV cluster runtime by moving them into Active Validators set

As Petri Networks contain only:

- marks
- places
- transitions
- arcs

we need to expand this set with components that would scale automatically and implement parts needed for the task such as Set, Act, Vote by Quorum, Update State.

**Set**

Most work in our model revolves around Set mutations  
Add item

 ![Untitled 4](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/4866ba15070d1d2952f6babd27c1098ff734c242.png)

Remove item

 ![Untitled 5](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/0f6c1e7d2ad614f0c3a2ca93da400a4a0ca24f62.png)

Emptiness check

 ![Untitled 6](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/8fb2eb0c8310bf20ca602acc4e9a1c5dd57b1acc.png)

Set Items counting

 ![Untitled 7](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/d02db844836b8222b0da3131c6668cd34e54cb13.png)

We then generalise Set component description (where N is max set capacity we allow in out model):

 ![Untitled 8](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/2dda3f1e65248afd13811d36e25eb8c7973c5cf5.png)

This allowed us to instantiate as many sets as we want using short code listings like

 ![Untitled 9](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/f45bd183899b50b97b347730c33c18dc5a56a7e3.png)

And display them in Formal Verification Application:

 ![Untitled 10](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/5a918d383e8e334b1b6e1f6b710e1dd55eeb61d3.png)

We introduce petri network model that includes dynamic network capacity and max occupancy

**Schematic depiction of action in presence of disabled nodes**

 ![Untitled 11](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/14a4ed5eaf75aec6c0663c9831044874bae12240.png)

We replicate this structure for all possible Nodes composition

This all lead us to a notion of **Consensus decision process that looks like this:**

1. We generate quorum checker for k of N nodes (here N is the number of nodes in the cluster and k is the quorum)
2. If we set k = N we can check that all nodes voted

 ![image10](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/3de25ec43aa63e7971646c8f235b9f08e2e94a45.jpeg)

**Schematic depiction of a node selecting an Activate decision**

 ![Untitled 12](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/534aadab16e1505706275cc1a868c9e62fddf98f.png)

Each node can make a set of possible action choices

**Schematic depiction of state action selection**

 ![Untitled 13](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/97efef8cfbe9654408e5a8237ebda22425129ced.png)

Next we want to model how consensus can be shown in the presence of many nodes and possible actions in details

**Modelling BFT Consensus-based State Change using Petri Networks**

In BFT we always have a leader-like node

Leading node proposes action (state change, this is all done by underlying BFT including state sync details of which are out of our current scope)

others verify (\operatorname{Quorum}(k) nodes)

System updates state

 ![Untitled 14](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/fc819c5ba31865fb0d5b95c41cef335183481699.png)

**Schematic depiction of Composite mutations leading to system state update**

 ![Untitled 15](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/98669cabc3929c8054e9ef31ed97605f134b8445.png)

Leader Election ( for the first nodes in the node-set we highlight in green the action path that could happen, and in red, dependencies of each action associated with a corresponding PN model transition)

 ![Untitled 16](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/c96c535815511d313a2d9011c0bb5af52d851fa7.png)

Leader Action flow

 ![Untitled 17](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/d08286019c2d7a1d622008ad0cf68f2d5e9e1898.png)

Quorum on Leader Action (here for clarification of the action result, we highlight the decision reached/cancelled in green and red, and the PN place where the token may be placed for forced task cancellation in yellow)

 ![Untitled 18](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/6c598df25efd24af992f366dace6a1910d772582.png)

Frame-based Node Action Start

 ![Untitled 19](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/beb69a53bfc75ffb15722a08ac3d5a20bdca682d.png)

Pruning based clean up on Quorum end

 ![Untitled 20](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/dc2fb68a45a27fa55bd6a0973ac6a747606a7b2c.png)

Updated Schematic action flow

 ![Untitled 21](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/338d209eadfec61e5b6f1209b2d806f0c212aac5.png)

Updated Quorum on Leader Action

 ![Untitled 22](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/52a9551b57c90f4d2dad1969210a906b8456eb6c.png)

Using the fact that PNs are deterministic we can split yes/no decisions and remove Time Frame End dependency from here

 ![Untitled 23](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/7305fdafa92dde493f0afd51ff70c8af97625520.png)

Multistage mutations correlation

 ![Untitled 24](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/679ef56f89e1562d2e208e46ae96a5412c67807e.png)

**Modeling Quorum Consensus using Petri Networks**

Our state is governed by composite mutations thus a single **System state update can look like this:**

 ![Untitled](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/c53503c6e4ccd99f04eb3660eea22d0e805eeba8.png)

this example depicts our most complicated composite mutation, all others work in similar fashion

to simplify its future representation we will use such **Composite Mutation System state update type simplified depictions:**

 ![Untitled 2](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/f845685428ad7dd5c1cbb64b0faa29e40a7c2d16.png)

We can cancel, start, lock on the process and check for success of ending of any composite mutation.

And thus overall system model would look like such **Distributed System state machine** :

![Untitled]()

Here we can change validators, operators set; have validators enabled or disabled, stop cluster gently after exiting all validators.

## Appendix B: Petri Network Code generator

To facilitate standartised network generation we developed the following components:

1. `Place` class:

2. `Transition` class:

3. `SubSystem` class:

4. `ConstSizeSetSubSystem` class (extends `SubSystem`):

5. `LeaderElection` class (extends `SubSystem`):

6. `LeaderVoteLock` class (extends `SubSystem`):

 ![Untitled 25](https://europe1.discourse-cdn.com/flex013/uploads/obol/original/1X/de6e89b99d1a90ef601f0eceb9998a65c947cbc4.png)

```
Generated network and its incividual components can be formally modeled and verified in Petri Nets modelling tool such as [SMPT](https://github.com/nicolasAmat/SMPT/tree/master) and [Nd](https://projects.laas.fr/tina/download.php) that support .net format with inhibitor nodes by setting various default states for operations, operators and validators (putting markers into places) and testing desired configuration of a given network.

```

Given that BFT protocol implementation algorithm is out of scope and we can construct Blockchain or DAG using given base state consensus synchronizing solution, also not all of the state change decisions of operators can be automated as some synchronisation happens in the background in off-chain