# A MILP Model for a Byzantine Fault Tolerant Blockchain Consensus
## 1 Introduction
The chain of blocks is formed in a linear manner, so each block is assigned with a unique incremental number, called _block index_, where the largest block index in a chain of blocks is called _blockchain height_. The dBFT is a partially-synchronous algorithm, where each consensus node is allowed to temporarily become a _speaker_ in a round-robin fashion (see [14] for more details). Given a height \(H\), consensus node \(i\) will be declared speaker when \(H\equiv i\) (\(modN\)). The speaker node is allowed to propose a block (by grouping the transactions from its mempool), which is then validated by the other consensus nodes (at least \(2f+1\), since \(f\) could have failed). If speaker does not respond (or appear to have failed), a timer is triggered after \(T\) seconds and a _view change_ occurs, where consensus nodes nominate \(i+1\) (\(modN\)) as the next speaker. In theory, due to the 1 BF nature of dBFT, only a single block can exist at each block height, and malformed blocks are rejected by the functional nodes, up to the Byzantine fault limit \(f\). To reduce the number of messages in P2P layer, the first version of dBFT (named dBFT 1.0) included only two of the three phases from PBFT, which allowed rare (but inconvenient) scenarios where more than one block is proposed (due to severe delays and timing issues). This situation required nodes to be reset after several weeks of operation, since following a \"bad path\" in the blockchain (also called _spork_) would lock that node forever (no fork is possible in a 1 BF consensus). A solution to this spark issue was made possible in 2019 with the proposal of dBFT 2.0, which included an extra _commit phase_ to the consensus, with other synchrony conditions. However, although operational in practice for several months (without any spark), no theoretical study has demonstrated the correctness of such mechanism. In fact, most consensus mechanisms proposed for blockchains typically do not include mathematical proofs for correctness, as it is very challenging and time-consuming task, focusing only on computational experiments. Moreover, computational studies typically focus only on non-Byzantine failures, which are easier to analyze. This work proposes a MILP model that behaves as a _very strong Byzantine adversary_, capable of exploring many sorts of issues in the consensus algorithm, including arbitrary network delays and generating intentional failures in an _exact manner_ (finding a maximum-damage scenario). Although quite strong, the adversary is computationally-bound such that it is not capable of subverting cryptographic technologies involved and to generate exponential delays. We apply the proposed technique for the Neo dBFT 1.0 and 2.0, demonstrating the Byzantine failures in a graphical approach (to visually observe attack conditions). The limitations of the approach are also discussed, due to the time discretization techniques employed and high number of variables in the model, so efficient solvers and integer programming are needed. We refer the reader to the paper by [PERSON] et al. (2015) for more details on the dBFT paradigm and recent discussions on novel consensus algorithms for blockchain. To the best of our knowledge, this is the first time MILP is used to generate exact adversarial models for the verification of Byzantine consensus systems. This paper is organized as follows. Section 1 introduces the work and presents background for MILP and the dBFT consensus. Then, Section 2 presents background on replicate state machines for Byzantine problems, the detailed operations for three-phase dBFT consensus and a few related works from the literature. Section 3 proposes mathematical formulations to describe several adversarial conditions for dBFT 1.0 and 2.0. On Section 4, we perform several experiments and analyze the scenarios with a developed graphical tool. Finally, Section 5 concludes the work and presents future perspectives for the verification of Byzantine models using experimental tools.