Nathalie Bertrand

Vincent Gramoli

Igor Konnov

Marijana Lazic

Pierre Tholoniat

Josef Widder

Marijana Lazić

Compositional Verification of Byzantine Consensus

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Reasoning about executions of distributed algorithms is hard due to several sources of non-determinism, such as asynchrony and faults. It therefore requires expert knowledge to design and to rigorously prove distributed algorithms. Unsurprisingly, bugs in specifications and in proofs of theoretical work appear in the literature. With the resurgence of interest in byzantine consensus largely driven by blockchains, correctness of these algorithms has become crucial for security.

Thankfully, recent progress in automated verification are first steps towards the model checking of faulttolerant consensus algorithms. For instance, parameterized model checking allows one to verify algorithms for an arbitrary number n of processes [START_REF] Bloem | Decidability of Parameterized Verification[END_REF] that is unknown at design time. In addition, it reduces the model checking for any fault number f and its upper bound t to bounded model checking questions [START_REF] Fisman | On verifying fault tolerance of distributed protocols[END_REF]. The threshold automaton (TA) framework for communication-closed algorithms [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF][START_REF] Balasubramanian | Complexity of verification and synthesis of threshold automata[END_REF] exploits thresholds in guards such as "number of messages from distinct processes exceeds 2t + 1", and in the resilience condition of the form n > 3t. The parameterized model checking of threshold automata builds upon a reduction [START_REF] Elrad | Decomposition of distributed programs into communication-closed layers[END_REF][START_REF] Lipton | Reduction: A method of proving properties of parallel programs[END_REF] that moves steps of asynchronous (interleaved) executions to obtain simpler executions, which are equivalent to the original executions with respect to safety and liveness properties. As moving steps preserves the admissibility of the execution, this reduction is, however, closely tied to the asynchronous semantics. Such a technique has recently proved instrumental in verifying fully asynchronous parts of consensus algorithms, like broadcast algorithms [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF].

Due to the famous impossibility result [START_REF] Michael | Impossibility of distributed consensus with one faulty process[END_REF], the above method could not be applied to proving deterministic consensus algorithms 1 in the asynchronous setting. The aforementioned reduction technique does not apply to partial synchrony [START_REF] Dwork | Consensus in the presence of partial synchrony[END_REF] either: moving the message reception step to a later point in the execution might violate an assumed message delay. In fact, these delays are important as typical partially synchronous consensus algorithms feature monotonically increasing timers to catch up with the unknown bound on the delay to receive a message. The crux of the problem is to automatically prove liveness or the consensus termination. Due to similar complications, most known verification results are designed for either synchronous (lock step) or asynchronous semantics.

In addition, partially synchronous consensus algorithms generally rely on a coordinator process that helps other processes converge and whose identifier rotates across rounds. Some efforts were devoted to proving the termination of partially synchronous consensus algorithms, like Paxos, assuming synchrony [START_REF] Hawblitzel | Ironfleet: proving practical distributed systems correct[END_REF]. The drawback is that such algorithms aim at tolerating non-synchronous periods before reaching a global stabilization time (GST) after which they terminate. Proving that such an algorithm terminates under synchrony does not show that the algorithm would also terminate if processes reached GST at different points of their execution. Instead, one would also need to show that correct processes can catch up in the same round. This would, in turn, require proving the correctness of a synchronizer algorithm [START_REF] Dwork | Consensus in the presence of partial synchrony[END_REF].

The problem of verifying consensus is even more subtle when processes are byzantine as they can execute arbitrary steps, changing their state and the values they share. Hence, verifying that an algorithm tolerates byzantine faults requires to reason about the combination of asynchronous executions with all the possible scenarios resulting from arbitrary behaviors, hence adding up to the already large number of reachable states. The verification of such algorithms is thus often restricted to showing safety properties, like agreement and validity, and ignoring liveness [START_REF] Lamport | Byzantizing paxos by refinement[END_REF]. This is not surprising, especially given that such coordinator-based protocols, need a non-trivial byzantine fault tolerant synchronizer algorithm [START_REF] Bravo | Making byzantine consensus live[END_REF].

Our results

In this paper, we leverage the automatic parameterized model checking to prove both the safety and liveness of a byzantine consensus algorithm. Our contributions are as follows:

1. We focus on a safe but not live variant of the binary byzantine consensus of DBFT [START_REF] Crain | DBFT: Efficient leaderless Byzantine consensus and its applications to blockchains[END_REF] that is particularly simple: It does not need a coordinator, relies neither on randomization nor on signature and solves consensus deterministically. The novelty here lies in making it live by assuming a stronger notion of fairness (compared to typical reliable channels) to ensure termination, hence bypassing the need for partial synchrony. It builds upon ideas common to randomized and partially synchronous algorithms by featuring: (i) a binary value broadcast [START_REF] Mostéfaoui | Signature-free asynchronous Byzantine consensus with T < N/3 and O(N 2 ) messages[END_REF], a variant of the reliable broadcast for binary values that guarantees that correct processes deliver exclusively values broadcast by correct processes and (ii) a round-based execution that broadcasts and delivers values at multiple times before comparing the finally delivered message content to the parity of the round [START_REF] Crain | DBFT: Efficient leaderless Byzantine consensus and its applications to blockchains[END_REF]. If the content matches the parity, then the algorithm decides, otherwise the algorithm updates its estimate for the next round. Interestingly, our fairness assumption only requires the existence of a specific ordering of message receptions in every infinite sequence of invocations of the binary value broadcast, without constraining the rest of the consensus algorithm.

2. We design a compositional proof methodology as a first step towards exploiting modularity of distributed algorithms in parameterized model checking. We provide threshold automata (TAs) models for two distributed algorithms that have strong interactions, namely an inner broadcast TA and an outer decision TA that invokes the inner one for some of its communications. To deal with the state space explosion, we express the guarantees of the inner broadcast primitive as temporal logic properties that we automatically verify with model checking and we replace the inner TA in the global TA by a gadget TA that captures the proven temporal specification. Hence, the compositional approach comprises a simple TA interface proved by hand and the combinatorial hard part that deals with asynchrony and faults proved automatically with the model checker.

3. We formally verify our consensus algorithm using the parameterized model checker (ByMC) [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF] for any number n of processes and t of faulty processes. With ByMC, we check the temporal specifications (safety and liveness) of the inner TA encoding the broadcast algorithm, that we then exploit in the outermost TA. We demonstrate the efficiency gain of our compositional approach by running ByMC on (i) the naive TA encoding of our consensus algorithm as well as (ii) the composite TA resulting from our compositional approach. It turns out that ByMC could not prove the safety of the naive TA within days (after which we decided to forcefully stop it). In contrast, ByMC successfully checks the liveness and safety of the composite TA in slightly more than a minute.

Building upon recent progress in automated verification, our compositional proof is a typical example of new ways that can help addressing the error-prone task of proving distributed systems correct. While encoding partial synchrony in model checkers remains an open research challenge, our work shows that fairness, which appears as a more natural assumption that can be formalized for curent model checkers, can be strengthened to alleviate the need in distributed algorithms for additional assumptions, like partial synchrony.

Related Work

Interactive theorem provers [START_REF] Sergey | Programming and proving with distributed protocols[END_REF][START_REF] Rahli | Formal specification, verification, and implementation of fault-tolerant systems using EventML[END_REF][START_REF] Klaus Von Gleissenthall | Pretend synchrony: synchronous verification of asynchronous distributed programs[END_REF] were used to prove consensus algorithms. In particular, Coq helped prove two-phase commit [START_REF] Sergey | Programming and proving with distributed protocols[END_REF], Raft [START_REF] Wilcox | Verdi: a framework for implementing and formally verifying distributed systems[END_REF] and the Algorand consensus algorithm [START_REF] Musab | Towards a verified model of the algorand consensus protocol in coq[END_REF] while Dafny [START_REF] Hawblitzel | Ironfleet: proving practical distributed systems correct[END_REF] proved MultiPaxos. Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF] was used to prove byzantine fault tolerant algorithms [START_REF] Charron-Bost | Formal verification of consensus algorithms tolerating malicious faults[END_REF] and was combined with Ivy to prove the Stellar consensus protocol [START_REF] Losa | On the formal verification of the stellar consensus protocol. In 2nd Workshop on Formal Methods for Blockchains[END_REF]. Theorem provers check proofs, not the algorithms. Hence, one has to invest efforts into writing detailed mechanical proofs.

Specialized decision procedures are a way of proving consensus algorithms. They were used to prove Paxos [START_REF] Kragl | Inductive sequentialization of asynchronous programs[END_REF]. Crash fault tolerant consensus algorithms were manually encoded with their invariants and properties to prove formulae using the Z3 SMT solver [START_REF] Dragoi | A logic-based framework for verifying consensus algorithms[END_REF]. Decision procedures also proved the safety of byzantine fault tolerant consensus algorithms when f = t [START_REF] Berkovits | Verification of thresholdbased distributed algorithms by decomposition to decidable logics[END_REF] but not their termination. Similarly, a proof by refinement of the safety of a byzantine variant of Paxos was proposed [START_REF] Lamport | Byzantizing paxos by refinement[END_REF] but its liveness is not proven. These decision procedures require the user to fit the specification into the suitable logical fragment.

Explicit-state model checking fully automates verification of distributed algorithms [START_REF] Holzmann | The SPIN Model Checker[END_REF][START_REF] Yu | Model checking TLA + specifications[END_REF]. It allows to check the reliable broadcast algorithm [START_REF] John | Towards modeling and model checking fault-tolerant distributed algorithms[END_REF]. TLC [START_REF] Yu | Model checking TLA + specifications[END_REF] checked a reduction of fault tolerant distributed algorithms in the Heard-Of model that exploits their communication-closed property [START_REF] Chaouch-Saad | A reduction theorem for the verification of round-based distributed algorithms[END_REF]. And the agreement of consensus algorithms was proved in the asynchronous setting [START_REF] Noguchi | Safety verification of asynchronous consensus algorithms with model checking[END_REF]. These explicit-state tools enumerate all reachable states and thus suffer from state explosion.

Symbolic model checkers [START_REF] Burch | Symbolic model checking: 10ˆ20 states and beyond[END_REF] cope with this explosion by representing state transitions efficiently. NuSMV and SAT helped check consensus algorithms for up to 10 processes [START_REF] Tsuchiya | Using bounded model checking to verify consensus algorithms[END_REF][START_REF] Tsuchiya | Verification of consensus algorithms using satisfiability solving[END_REF]. Apalache [START_REF] Konnov | TLA+ model checking made symbolic[END_REF] uses satisfiability modulo theories (SMT) to check inductive invariants and verify symbolic executions of TLA + specifications of the reliable broadcast and crash fault tolerant consensus algorithms but requires parameters to be fixed. These tools cannot be used to prove (or disprove) correctness for an arbitrary number of processes.

Parameterized model checking [START_REF] Downey | Parameterized Complexity[END_REF] works for an arbitrary number n of processes [START_REF] Bloem | Decidability of Parameterized Verification[END_REF]. Although the problem is undecidable [START_REF] Krzysztof | Limits for automatic verification of finite-state concurrent systems[END_REF] in general, one can verify specific classes of algorithms [START_REF] Emerson | Reducing model checking of the many to the few[END_REF]. Indeed, distributed algorithms with a ring-based topology were checked with automata-theoretic method [START_REF] Aiswarya | An automata-theoretic approach to the verification of distributed algorithms[END_REF] and with Presburger arithmetics formulae verified by an SMT solver [START_REF] Sangnier | Parameterized verification of algorithms for oblivious robots on a ring[END_REF]. Bosco [START_REF] Jiun | Bosco: One-step byzantine asynchronous consensus[END_REF] has been the focus of various parameterized verification techniques [START_REF] Lazic | Synthesis of distributed algorithms with parameterized threshold guards[END_REF][START_REF] Balasubramanian | Complexity of verification and synthesis of threshold automata[END_REF], however, it acts as a fast path wrapper around a separate correct consensus algorithm. The condition-based consensus algorithm [START_REF] Mostéfaoui | Conditions on input vectors for consensus solvability in asynchronous distributed systems[END_REF][START_REF] Mostéfaoui | Evaluating the conditionbased approach to solve consensus[END_REF] was verified [START_REF] Balasubramanian | Complexity of verification and synthesis of threshold automata[END_REF] with the byzantine model checker ByMC [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF][START_REF] Konnov | ByMC: Byzantine model checker[END_REF][START_REF] Konnov | Tutorial: Parameterized verification with byzantine model checker[END_REF], only under the condition that the difference between the numbers of processes initialized with 0 and 1 differ by at least t. Recently, the crash fault tolerant Ben-Or consensus algorithm was proved correct with a probabilistic reasoning extension of ByMC [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]. In this paper, we also exploit ByMC but prove a byzantine consensus algorithm. Some efforts were devoted to verify consensus algorithms in the partially synchronous setting [START_REF] Dwork | Consensus in the presence of partial synchrony[END_REF] where after an unknown global stabilization time (GST) all links deliver messages in a bounded amount of time. Such algorithms were verified using parameterized model checking [START_REF] Maric | Cutoff bounds for consensus algorithms[END_REF], however, these are only crash fault tolerant and cannot tolerate byzantine failures. PSync [START_REF] Dragoi | PSync: a partially synchronous language for fault-tolerant distributed algorithms[END_REF] views asynchronous executions in lock-steps and proves the LastVoting variant [START_REF] Charron-Bost | The heard-of model: computing in distributed systems with benign faults[END_REF] of Paxos but requires semi-decision procedures of a fragment of first-order logic. Partial synchrony is often tied to some complexity in byzantine consensus algorithms. To terminate, partially synchronous algorithms typically distinguish the execution of a coordinator from the execution of other processes [START_REF] Castro | Practical byzantine fault tolerance and proactive recovery[END_REF][START_REF] Charron-Bost | The heard-of model: computing in distributed systems with benign faults[END_REF][START_REF] Lamport | Byzantizing paxos by refinement[END_REF] and rely on a monotonically increasing timer to catch up with the unknown bound on the message delay. Our byzantine consensus algorithm does not inherit such intricacies.

Instead of assuming partial synchrony, we assume some notion of fairness. There exist related notions, like fair schedulers [START_REF] Bracha | Asynchronous consensus and broadcast protocols[END_REF] and limited link synchrony [START_REF] Aguilera | Communication-efficient leader election and consensus with limited link synchrony[END_REF]. Fair schedulers consider that the events of two processes receiving from two other processes are independent and that the probability for a process to receive from any other process is > 0 in any round [START_REF] Bracha | Asynchronous consensus and broadcast protocols[END_REF]. By contrast, our fairness is not probabilistic allowing us to model check safety and (deterministic) liveness. A key difference between our fairness assumption and partial synchrony is that our fairness does not impose restrictions on all links, which is similar to the notion of minimal synchrony needed to solve consensus [START_REF] Aguilera | Communication-efficient leader election and consensus with limited link synchrony[END_REF]. This minimal synchrony was later named [x + 1]-bi-source and helped solve byzantine consensus without all n 2 point-to-point links being eventually synchronous [START_REF] Aguilera | Consensus with byzantine failures and little system synchrony[END_REF]. More precisely, [x + 1]-bi-source states that there is a correct process that has x + 1 bi-directional links with itself and other correct processes and these links eventually behave synchronously. It was shown in [START_REF] Olivier Baldellon | A necessary and sufficient synchrony condition for solving byzantine consensus in symmetric networks[END_REF], that (t + 1)-bi-source is necessary and sufficient to implement authenticated byzantine consensus. Later, the same result was generalized to unauthenticated byzantine consensus with m ≤ (n -(t + 1))/t distinct values [START_REF] Bouzid | Minimal synchrony for byzantine consensus[END_REF].

Finally, an interesting novelty of our algorithm is that it neither needs a coordinator (or leader) nor that any link be eventually synchronous. By contrast, all the consensus algorithms we know of that do not require all links to be timely rely on a coordinator [START_REF] Aguilera | Communication-efficient leader election and consensus with limited link synchrony[END_REF][START_REF] Aguilera | Consensus with byzantine failures and little system synchrony[END_REF][START_REF] Hamouma | Byzantine consensus with few synchronous links[END_REF][START_REF] Bouzid | Minimal synchrony for byzantine consensus[END_REF]. They use a rotating coordinator whose particular messages can influence the estimate of other processes, to help them converge. If the coordinator does not manage to lead processes to a consensus, then another coordinator takes its role in what is called a new view. Before GST, processes may proceed at different rates. After GST, a synchronizer [START_REF] Bravo | Making byzantine consensus live[END_REF] is typically required to ensure that sufficiently many processes take part in the same view in order to guarantee termination. This is probably to circumvent this difficulty that the verification of the liveness of partially synchronous algorithms is often simplified by assuming synchrony [START_REF] Hawblitzel | Ironfleet: proving practical distributed systems correct[END_REF].

The only work we know that assumes fairness for verification of asynchronous consensus is the one of finitary fairness [START_REF] Alur | Finitary fairness[END_REF]. Unfortunately, it is demonstrated in the shared memory context and without byzantine failures. One can see our contribution as a step forward in the message passing context and with byzantine failures, and in order to achieve this result we introduce a novel composition technique.

In Section 2 we introduce our preliminary definitions, in Section 3 we model our fair binary value broadcast, in Section 4 we present our composition, in Section 5 we verify the consensus algorithm and in Section 6 we present the results of the model checker and conclude. In the optional appendix we explain the multiple-round TA to one-round TA reduction (A), provide examples related to fairness (B), missing proofs (C and E) and detailed specifications (D, F).

Preliminaries

The system is composed of n asynchronous sequential processes from the set Π = {p 1 , . . . , p n }, and i is called the "index" of p i . The processes communicate by exchanging messages through an asynchronous reliable point-to-point network, hence there is no bound on the delay to transfer a message but this delay is finite.

Failure model and fairness. Up to t < n/3 processes can exhibit a byzantine behavior [START_REF] Marshall | Reaching agreement in the presence of faults[END_REF], and behave arbitrarily. We refer to f ≤ t as the actual number of byzantine processes. A byzantine process is referred to as faulty, a non-faulty process is correct. As stated above, point-to-point reliable channels implicitly assume fairness, however, we will strengthen this fairness property by assuming that in an infinite sequence of binary value broadcast executions of our algorithm, there is one execution where some binary value is delivered by correct processes before the other value. The definition of this fairness is not needed for safety and is deferred to Section 3.3 to verify liveness.

Algorithm semantics. To define the asynchronous semantics of a distributed algorithm executed by these processes, we consider discrete time such that at each point in time, exactly one process takes a step. Hence the distributed execution is an interleaving of the individual steps taken by the processes. In particular, we assume that two messages cannot be received at the same time by the same process. Process p i sends a message to p j by invoking the primitive "send HEADER(m) to p j ", where HEADER indicates the type of message and m its content. Process p i receives a message by executing the primitive "receive()". We refer to broadcast(HEADER(m), •, messages) → messages as "for each p j ∈ Π do send HEADER(m) to p j " and "upon reception of HEADER(m) from process p j do messages[p j ] ← messages[p j ] ∪ {m}". We will use the process id i as a subscript to denote by var i that a variable var is local to process i but we omit it when it is clear from the context.

The verification method considered in this paper exploits the fact that the algorithms are communicationclosed [START_REF] Elrad | Decomposition of distributed programs into communication-closed layers[END_REF], i.e. only messages from the current round of a process may influence its steps. This can be implemented by tagging every message by its round number r; during round r all received messages with tag r < r are discarded and all received messages with tag r > r are stored for later. We also assume that computation takes no time.

The consensus problem. Assuming that each correct process proposes a binary value, the binary byzantine consensus problem is for each of them to decide on a binary value in such a way that the following properties are satisfied:

1. Termination. Every correct process eventually decides on a value.

Agreement.

No two correct processes decide on different values.

Validity. If all correct processes propose the same value, no other value can be decided.

Threshold automaton (TA) A threshold automaton [START_REF] Konnov | On the completeness of bounded model checking for thresholdbased distributed algorithms: Reachability[END_REF] describes the behaviour of a process in a distributed algorithm. Its nodes are locations representing local states, and labeled edges are guarded rules. Formally, it is a tuple L, I, Γ, Π, R, RC where L is the set of locations, I ⊂ L is the set of initial locations, Γ is the set of shared variables, Π is the finite set of parameter variables, R is the set of rules, and RC is the resilience condition over N |Π| 0 . Rules are defined as tuples from, to, φ, u , where from (resp. to) describes the source (resp. destination) locations, and the rule label is φ → u. Formula φ is called a threshold guard or simply a guard.

Example 1. Fig. 1 in Section 3.1 presents the pseudocode of the binary value broadcast and its threshold automaton. There are 10 locations, namely

L = {V 0 , V 1 , B 0 , B 1 , B 01 , C 0 , C 1 , CB 0 , CB 1 , C 01 }, and two of them are initial, I = {V 0 , V 1 }.
Shared variables are b 0 and b 1 , while parameter variables are n, t and f . The set of rules R consists of {r i | 1 ≤ i ≤ 12} and 7 self-loops. For instance, rule r 3 is defined as B 0 , C 0 , b 0 ≥2t+1f , 0 . Finally, the resilience condition is n > 3t ∧ t ≥ f ≥ 0.

A multi-round threshold automaton is intuitively defined such that one round is represented by a threshold automaton, and additionally we have so-called round-switch rules that connect final locations with initial ones, and therefore allow processes to move from one round to the following one. We typically depict those round-switch rules as dotted arrows. Examples of multi-round TA are depicted in Figures 2 and3. When it is clear from the context that automata have multiple rounds, we just call them threshold automata. When we want to stress that a TA does not have multiple rounds, we may call it a one-round TA.

Counter systems

The semantics of a (one-round) threshold automaton TA are given by a counter system Sys(TA) = Σ, I, T where Σ is the set of all configurations among which I are the initial ones, and T is the transition relation. A configuration σ ∈ Σ of a one-round TA captures the values of location counters (counting the number of processes at each location, therefore non-negative integers), values of global variables, and parameter values. A transition t ∈ T is unlocked in σ if there exists a rule r = from, to, φ, u ∈ R such that φ evaluates to true in σ, and location counter of from is at least 1, denoted κ[from] ≥ 1, showing that at least one process is currently in from. In this case we can execute transition t on σ by moving a process along the rule r from location from to location to, which is modeled by decrementing counter κ[from], incrementing κ[to], and updating global variables according to the update vector u.

A counter system Sys(TA) of a multi-round TA is defined analogously. A configuration captures the values of location counters and global variables in each round, and parameter values (that do not change over rounds). Then we define that a transition t is unlocked in a round R by evaluating the guard φ and the counter of location from in the round R. The execution of t in σ accordingly updates κ[from, R], κ[to, R] and global variables of that round, while the values of these variables in other rounds stay unchanged.

Linear temporal logic notations Following a standard model checking approach, we use formulas in linear temporal logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] to formalize the desired properties of distributed algorithms. The basic elements of these formulas, called atomic propositions, are predicates over configurations related (i) to the emptiness of each location at each round and (ii) to the evaluation of threshold guards in each round. They have the following form:

(i) κ[L, R] = 0 expresses that at least one correct process is in location L in round R, while κ[L, R] = 0 expresses the opposite (in one-round systems we just write κ[L] = 0 or κ[L] = 0); (ii) [b 0 , R]≥2t+1-f
is evaluated depending on the values of the shared variable b 0 in round R and parameters t and f (in one-round systems we just write b 0 ≥2t+1f ). LTL builds on propositional logic with ⇒ for 'implication', ∨ for 'or' and ∧ for 'and', and has extra temporal operators ♦ that stands for 'eventually', for 'always'. LTL formulas are evaluated over infinite runs of Sys(TA). Examples of LTL properties in a one-round system are (BV-Just v ), (BV-Obl v ) and (BV-Unif v ) (see page 7). LTL properties in multi-round systems often have quantifiers over round variables, as for example in (Agree v ) and (Valid v ) (see page 11).

The tool ByMC is used to automatically verify a specific fragment of LTL on one-round systems [START_REF] Konnov | Para 2 : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF]. This fragment is sufficient to express safety and liveness properties of consensus [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]. Moreover, using communicationclosure, the verification for this fragment of temporal logic on multi-round systems reduces to one-round systems [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]Theorem 6]. We explain in more details this reduction in Appendix A.

The assumption of reliable communication is modeled as follows at the TA level: if the guard of a rule is true infinitely often, then the origin location of that rule will eventually be empty. This reflects that an if branch of the pseudo-code is taken if the condition is true. This progress assumption2 is in particular crucial to prove liveness properties: in the sequel, we prepend it to the liveness properties in the TA specification.

Fairness of binary value broadcast

To overcome the limited scalability of model checking tools, our compositional verification approach consists of decomposing a distributed algorithm in several blocks that can be verified in isolation to obtain a simplified threshold automaton that can be model checked.

In this section we focus on a binary value broadcast, or bv-broadcast for short, that will serve as the main building block of the byzantine consensus algorithm of Section 4. In Section 3.1 we formally model the bv-broadcast as a threshold automaton that tolerates a number f of byzantine failures upper-bounded by t among n processes. In Section 3.2 we model the specification of bv-broadcast in LTL to verify it within 10 seconds. In Section 3.3 we introduce the fairness of an infinite sequence of executions of bv-broadcast that will play a crucial role in verifying in Section 5 that we indeed solve the byzantine consensus problem.

Modeling the binary value broadcast

The binary value broadcast [START_REF] Mostéfaoui | Signature-free asynchronous Byzantine consensus with T < N/3 and O(N 2 ) messages[END_REF], or bv-broadcast for short, is a communication primitive guaranteeing that all binary values "bv-delivered" were "bv-broadcast" by a correct process. It is particularly useful to solve the byzantine consensus problem with randomization [START_REF] Mostéfaoui | Signature-free asynchronous binary Byzantine consensus with t < n/3, O(n 2 ) messages and O(1) expected time[END_REF][START_REF] Cachin | Asymmetric byzantine consensus[END_REF] or partial synchrony [START_REF] Crain | DBFT: Efficient leaderless Byzantine consensus and its applications to blockchains[END_REF][START_REF] Cachin | Anonymity preserving byzantine vector consensus[END_REF]. Consider Fig. 1 (left) that depicts its pseudocode and Fig. 1 (right) that depicts the corresponding threshold automaton (TA). contestants ← contestants ∪ {v}

V 0 V 1 B 0 B 1 CB 0 CB 1 B 01 C 0 C 1 C 01 r 1 : b 0 ++ r 2 : b 1 ++ b0 ≥ 2 t+ 1 -f r3 b 1 ≥ t+ 1 -f → b 1 ++ r 4 b0 ≥ t+ 1 -f → b0 ++ r5 b 1 ≥ 2 t+ 1 -f r 6 b 1 ≥ t+ 1 -f → b 1 ++ r 7 b0 ≥ 2 t+ 1 -f r8 b 1 ≥ 2 t+ 1 -f r 9 b0 ≥ t+ 1 -f → b0 ++ r10 b 1 ≥ 2 t+ 1 -f r 11 b0 ≥ 2 t+ 1 -f r12

Pseudocode of the binary value broadcast

The bv-broadcast (see Fig. 1, left) aims at having at least 2t+1 processes broadcasting the same binary value. Once a correct process receives a value from t+1 distinct processes, it broadcasts it (line 4) if it did not broadcast it already (line 5). Once a correct process receives a value from 2t+1 distinct processes, it delivers it. Here the delivery at process p i is modeled by adding the value to the set contestants i , which will simplify the pseudocode of the byzantine consensus algorithm in Section 4.1.

Threshold automaton of the binary value broadcast

The corresponding TA of Fig. 1 (right) has two initial locations V 0 or V 1 , indicating whether the (correct) process initially has value 0 or 1, respectively. We can see that a correct process p i sends only two types of messages, (BV, 0, i ) and (BV, 1, i ), these trigger the corresponding receptions at other processes. Global variables b 0 and b 1 , respectively, capture the number of the two types of messages sent by correct processes. Thus, for example, b 0 ++ models a process broadcasting message (BV, 0, i ).

From local to global variables for model checking

While producing a formal model, extra care is needed to avoid introducing redundancies. For example, line 4 indicates that the process broadcasts value v if it received v from t+1 distinct processes. One may thus be tempted to evaluate a guard based on a local receive variable but, as the formal model needs to count sent values to not "re-broadcast" (line 5), it would be sufficient to simply enable a guard based on global send variables instead of also maintaining local receive variables. Note, however, that the point-to-point reliable channels ensures that p j sends message m to p i implies that eventually p i receives message m from p j . To remove redundant local receive variables, one can use the quantifier elimination for Presburger arithmetic [START_REF] Moj | Uber die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt[END_REF] and obtain quantifier-free guard expressions over the shared variables that are valid inputs to ByMC [START_REF] Konnov | ByMC: Byzantine model checker[END_REF][START_REF] Konnov | Tutorial: Parameterized verification with byzantine model checker[END_REF]. For more details, note that Stoilkovska et al. [START_REF] Stoilkovska | Eliminating message counters in threshold automata[END_REF] eliminated the quantifier over the similar receive variables in Ben-Or's consensus algorithm [START_REF] Ben-Or | Another advantage of free choice (extended abstract): Completely asynchronous agreement protocols[END_REF] with the SMT solver Z3 [START_REF] Mendonça De Moura | Z3: an efficient SMT solver[END_REF]. Hence shared variables b 0 and b 1 of the TA denote, respectively, the number of messages (BV, 0, i ) and (BV, 1, i ) sent by correct processes in the pseudocode.

Modeling arbitrary (byzantine) behaviors in the TA

In order to model that, among the received messages, f messages could have been sent by byzantine processes, we need to map the 'if' statement of the pseudocode, comparing the number of receptions from distinct processes to t+1, to the TA guards, comparing the number b 1 + f of messages sent to t + 1. As b 1 counts the messages sent by correct processes and f is the number of faulty processes that can send arbitrary values, a correct process can move from B 0 to B 01 as soon as t+1-f correct processes have sent 1, provided that f faulty processes have also sent 1.

As a result, the guard of rule r 4 only evaluates over global send variables as: if more than t+1 messages of type b 1 have been sent by correct processes (hence the guard b 1 ≥ t+1-f ), then the shared variable b 1 is incremented, mimicking the broadcast of a new message of type b 1 . Rule r 3 corresponds to lines 7-8 and delivers value v = 0 by storing it into variable contestants upon reception of this value from 2t + 1 distinct processes. Hence, reaching location C 0 in the TA indicates that the value 0 has been delivered. As a process might stay in this location forever, we add a self-loop with guard condition set to true.

Other locations and rules

locations V 0 V 1 B 0 B 1 B 01 C 0 CB 0 C 1 CB 1 C 01
values broadcast / / 0 1 0,1 0 0,1 1 0,1 0,1 values delivered / / / / / 0 0 1 1 0,1 The locations of the automaton correspond to the exclusive situations for a correct process depicted in Table 1.

After location C 0 , a process is still able to broadcast 1 and eventually deliver 1 after that. After location B 01 , a process is able to deliver 0 and then deliver 1, or deliver 1 first and then deliver 0, depending on the order in which the guards are satisfied. Apart from the self-loops, note that the automaton is a directed acyclic graph. Also, on every path in the graph, a shared variable is incremented only once. This reflects that in the pseudocode, a value may only be broadcast if it has not been broadcast before.

Properties of the binary value broadcast

As was previously proved by hand [START_REF] Mostéfaoui | Signature-free asynchronous Byzantine consensus with T < N/3 and O(N 2 ) messages[END_REF][START_REF] Mostéfaoui | Signature-free asynchronous binary Byzantine consensus with t < n/3, O(n 2 ) messages and O(1) expected time[END_REF], the bv-broadcast primitive satisfies four properties: BV-Justification, BV-Obligation, BV-Uniformity and BV-Termination. Here, we formalize these properties in linear temporal logic (LTL) to formally prove them correct. As we will discuss in Section 6, we verify the four properties automatically with model checking for any parameters n and t < n/3 in less then 10 seconds.

The BV-Justification property states: "If p i is correct and v ∈ contestants i , then v has been bv-broadcast by some correct process" where v ∈ {0, 1}. Alternatively, "if v is not bv-broadcast by some correct process and p i is correct, then v / ∈ contestants i ". In the TA from Fig. 1, v ∈ contestants i corresponds to process i being in one of the locations C v , CB v or C 01 . Thus, justification can be expressed in LTL as the conjunction BV-Just 0 ∧ BV-Just 1 where, BV-Just v is the following formula:

κ[V v ] = 0 ⇒ κ[C v ] = 0 ∧ κ[CB v ] = 0 ∧ κ[C 01 ] = 0 . (BV-Just v )
BV-Obligation requires that if at least (t+1) correct processes bv-broadcast the same value v, then v is eventually added to the set contestants i of each correct process p i . This can again be formalized as BV-Obl 0 ∧ BV-Obl 1 where BV-Obl v is the following formula:

b v ≥ t+1 ⇒ ♦ L∈Locs v κ[L] = 0 , (BV-Obl v )
where

Locs v = {V 0 , V 1 , B 0 , B 1 , B 01 , C 1-v , CB 1-v } are all the possible locations of a process i if v ∈ contestants i .
BV-Uniformity requires that if a value v is added to the set contestants i of a correct process p i , then eventually v ∈ contestants j at every correct process p j . We formalize this as BV-Unif 0 ∧ BV-Unif 1 where BV-Unif v is the following:

♦ (κ[C v ] =0 ∨ κ[CB v ] =0 ∨ κ[C 01 ] =0) ⇒ ♦ L∈Locs v κ[L]=0 , (BV-Unif v )
where Locs v is defined as in (BV-Obl v ). Finally, the BV-Termination property claims that eventually the set contestants i of each correct process p i is non empty. This can be phrased as the following LTL formula BV-Term:

♦ κ[V 0 ]=0 ∧ κ[V 1 ]=0 ∧ κ[B 0 ]=0 ∧ κ[B 1 ]=0 ∧ κ[B 01 ]=0 , (BV-Term)
forcing each correct process to be in one of the "final" locations C 0 , C 1 , C 01 , CB 0 , CB 1 .

A fairness assumption to solve asynchronous consensus

We now introduce a fairness assumption that will be crucial in the rest of this paper. In order to define it, we first define a good execution of the bv-broadcast with respect to binary value v as an execution where all correct processes (invoke bv-broadcast and) bv-deliver v before bv-delivering any other value. Second, we consider an infinite sequence of bv-broadcast executions, tagged with r ∈ N. It is important to stress that the setting is asynchronous, that is, processes invoke bv-broadcast infinitely many times, but at their own relative speed. Thus, they do not all invoke the bv-broadcast tagged with the same number r at the same time. Nonetheless, every process invokes bv-broadcast infinitely many times and in the r th invocation its behavior depends on the messages sent in the r th invocation of other processes. Therefore, we refer to the r th execution of bv-broadcast even though the processes invoke it at different times. We say that such an infinite sequence of bv-broadcast executions is fair if it contains an execution tagged with r that results in a good execution with respect to value r mod 2.

Definition 1 (v-good bv-broadcast).

A bv-broadcast execution is v-good if all its correct processes bv-deliver v first.

We express this property in LTL. A bv-broadcast execution is v-good if no process ever visits locations C 1-v and CB 1-v :

κ[C 1-v ] = 0 ∧ κ[CB 1-v ] = 0 .
Definition 2 (fair infinite sequence of bv-broadcast executions). An infinite sequence of bv-broadcast executions is fair if there exists an r such that the r th execution is (r mod 2)-good.

We simply refer to a fair bv-broadcast as if the infinite sequence of bv-broadcast executions is fair. For simplicity, we sometimes say that bv-broadcast is fair, when we actually mean that the infinite sequence of its executions is fair. We illustrate in Appendix B a possible execution of bv-broadcast whose existence implies fairness.

Composite Automaton for Byzantine Consensus

In this section we exploit the results of the first verification phase of Section 3 to simplify the threshold automaton of the byzantine consensus algorithm. In Section 4.1 we introduce the pseudocode of the byzantine consensus algorithm and its threshold automaton obtained with the naive (non-compositional) modeling described in Section 3.1. In Section 4.2 we replace, in this threshold automaton, the inner bv-broadcast automaton by a smaller automaton simplified with the bv-broadcast properties that are now verified. The verification of the resulting composite automaton is deferred to Section 5.

The byzantine consensus algorithm

Algorithm 1 is a byzantine consensus algorithm that relies on the fair binary value broadcast of Section 3 and derives from a safe (but not live) variant of the binary consensus algorithm of DBFT [START_REF] Crain | DBFT: Efficient leaderless Byzantine consensus and its applications to blockchains[END_REF] used in blockchains [START_REF] Crain | Evaluating the Red Belly Blockchain[END_REF]. It invokes bv-broadcast(•) at line 6 and uses a set contestants of binary values, whose scope is global, updated by the bv-broadcast (Fig. 1(left), line 8) and accessed by the procedure propose(•) (Alg. 1, line 7). As mentioned in Section 2, recall that the algorithm is communication-closed, so that for simplicity in the presentation we omit the current round number r as the subscript of the variables and the parameter of the function calls. Variable favorites is an array of n indices whose j th slot records, upon delivery, the message broadcast by process j in the current round. Each process p i manages the following local variables: the current estimate est, initially the input value of p i ; and a set of binary values qualifiers. This algorithm maintains a round number r, initially 0 (line 4), and incremented at the end of each iteration of the loop at line 15. Process p i exchanges EST and AUX messages (lines 6-8), until it received AUX messages from nt distinct processes whose values were bv-delivered by p i (lines 9-10). Process p i then tries at line 13 to decide a value v that depends on the content of qualifiers and the parity of the round. If qualifiers is a singleton there are two possible cases: if the value is the parity of the round then p i decides this value (line 13), otherwise it sets its estimate to this value (line 12). If favorites contains both binary values, then p i sets its estimate to the parity of the round (line 14). Although p i does not exit the infinite loop to help other processes decide, it can safely exit the loop after two rounds at the end of the second round that follows the first decision because all processes will be guaranteed to have decided. Note that even though a process may invoke decide(•) multiple times at line 13, only the first decision matters as the decided value does not change (see Section 5).

V 0 V 1 B 0 B 1 B 01 C 0 C 1 CB 0 CB 1 C 01 E 1 E 0 D 1 V 0 V 1 B 0 B 1 B 01 C 0 C 1 CB 0 CB 1 C 01 E 0 D 0 E 1 r 1 : b 0 ++

The effect of fairness

Note that the fairness notion from Section 3.3 ensures there is a round r in which all correct processes bv-deliver (r mod 2) first. The following lemma states that under the fairness assumption there is a round of Algorithm 1 in which all correct processes start with the same estimate. The proof is deferred to Appendix C.

Lemma 1.

If the infinite sequence of bv-broadcast executions of Algorithm 1 is fair, with the r th execution being (r mod 2)good, then all correct processes start round r+1 of Algorithm 1 with estimate r mod 2.

Modeling deterministic consensus

Figure 2 depicts the threshold automaton (TA) obtained by modeling Algorithm 1 with the method of Section 3.1. The TA depicts two iterations of the repeat loop (line 5), since Algorithm 1 favors different values depending on the parity of the round number. For simplicity, we refer to the concatenation of two consecutive rounds of the algorithm as a superround of the TA. As one can expect, this TA embeds the TA of the bv-broadcast which Figure 3: The composite threshold automaton of the byzantine consensus of Algorithm 1. Rules s j , 1 ≤ i ≤ 11, are obtained from s j by replacing each variable c ∈ {a 0 , a 1 , bvb 0 , bvb 1 } with its corresponding one c . is depicted by the dashed arrows, just as Algorithm 1 invokes the bv-broadcast algorithm of Fig. 1 (left). We thus distinguish the outer TA modeling the consensus algorithm from the inner TA modeling the bv-broadcast algorithm. Although Algorithm 1 is relatively simple, the global TA happens to be too large to be verified through model checking, as we explain in Section 6; the main limiting factor is its 14 unique guards that constrain the variables to enable rules in the TA. The detail of each rule of the TA is deferred to Appendix D.

V 0 V 1 M M 0 M 1 M 01 E 0 D 1 E 1 V 0 V 1 M M 0 M 1 M 01 D 0 E 1 E 0 s 1 : b v b 0 + + s2 : b v b1 + + s 3 : b v b0 ≥ 1 → a 0 + + s 4 : b v b 1 ≥ 1 → a 1 + + s 5 : a 0 ≥ n -t -f s 6 : b v b 1 ≥ 1 s 7 : b v b 0 ≥ 1 s 8 : a 1 ≥ n -t -f s9 : a0 ≥ n -t -f s 10 : a 0 +a 1 ≥n-t-f s 1 1 : a 1 ≥ n -t -f s 12 s 13 s 1 4

Simplified threshold automaton

Our objective is to formally prove that Algorithm 1 is unconditionally safe, and that it is live under the assumption of fairness at the bv-broadcast level. Since the threshold automaton of Figure 2 is too large to be handled automatically, we build on the properties proved for the bv-broadcast to simplify in the threshold automaton from Figure 2 the part representing the bv-broadcast. On the resulting simpler threshold automaton, assuming fairness of the bv-broadcast, we prove the termination of Algorithm 1 with the byzantine model checker ByMC in Section 6.

High-level idea. Ideally, the simplified threshold automaton could be obtained from the one of Fig. 2 by merging all internal states of the bv-broadcast into a single state with two possible outcomes. However, such a merge is not trivial because the bv-broadcast procedure "leaks" into the consensus algorithm. First of all, line 7 of Algorithm 1 refers to contestants, a global variable that is modified by the bv-broadcast algorithm (Fig. 1, left). Second, a process can execute line 8 of Algorithm 1 even if the bv-broadcast has not terminated. To capture this porosity, we introduce a new shared variable, some additional states and a transition rule that exploits a correctness property of the bv-broadcast.

Step by step construction. Figure 3 depicts the simplified composite threshold automaton of Algorithm 1 as a repeated superround. The left part of its superround corresponds to a round (or loop iteration) r i of Algorithm 1 for a given correct process p i such that r i mod 2 = 1 whereas its right half corresponds to a round r i where r i mod 2 = 0. Below we describe the construction of the left half of Figure 3 by explaining its locations and rules:

• V 0 , V 1 .
Initially, p i holds an estimate binary value.

• V 0 , V 1 → M.
Then, p i invokes bv-broadcast with the value of its estimate (line 6). This transition has no guard.

We count the number of correct processes that broadcast each value with shared variables bvb 0 and bvb 1 .

• M. When p i has called bv-broadcast but has not broadcast any AUX message yet, it is in location M. This corresponds to line 6. Note that a process that stays in M is not idle in practice: it actually keeps running the bv-broadcast primitive that was triggered earlier. However, we do not keep track of the messages exchanged in the underlying bv-broadcast primitive: bvb 0 and bvb 1 only count the initial value sent by bv-broadcast.

• M → M 0 , M 1 . When contestants i becomes non-empty (line 7), p i broadcasts an AUX message and proceeds to the next location. This AUX message contains the first value delivered to p i by bv-broadcast. We can thus define two shared variables, a 0 and a 1 , representing the number of 0s and 1s broadcast by correct processes with an AUX tag.

What is the guard on this condition? The earliest moment at which a correct process can have a non-empty contestants set is when another correct process has actually called bv-broadcast with such a value. Indeed, by BV-Justification, "If p i is correct and v ∈ contestants i , v has been bv-broadcast by a correct process". The condition that v has been bv-broadcast by a correct process is bvb v ≥ 1. Note that this condition relies only on the past behavior of correct processes, thanks to the byzantine fault tolerance of bv-broadcast. We do not have to take into account the possible messages sent by faulty processes here.

Such a transition may happen, but not necessarily immediately: even if another correct process has bv-broadcast 1 somewhere, p i might not have delivered it yet and can stay longer in location M, thanks to the self-loop. The correctness properties will be checked on all these possible executions. To prove the termination of the consensus algorithm, we need the BV-Termination as a precondition.

• M 0 , M 1 → M 01 . After having broadcast its AUX value, p i might deliver the other value in contestants i thanks to the bv-broadcast primitive, and move to location M 01 . The guard is the same as before. This transition does not trigger another AUX broadcast though. Recall that we assumed in Section 2 that no two receptions can occur at the same time at the same process.

• M 0 , M 1 , M 01 → D 1 , E 1 , E 0 .
Process p i can pass the guard of line 10 when it has received enough AUX messages with the same value. Some messages might come from faulty processes because AUX messages are sent with a regular broadcast (not bv-broadcast). Hence, it might be possible for a correct process to move to the next step even if it has received only ntf messages from correct processes.

A superround R of the composite automaton from Fig. 3 captures round 2R-1 followed by round 2R of Algorithm 1. One can thus restate Lemma 1 as the following corollary in the TA terminology. The proof is deferred to Appendix E. Corollary 1. Let r ∈ N be such that the r th execution of bv-broadcast in Algorithm 1 is (r mod 2)-good. Then:

• If there exists R ∈ N with r = 2R-1, then κ[M 0 , R] = 0) holds. • If there exists R ∈ N with r = 2R, then (κ[M 1 , R] = 0 holds.

Verification of Byzantine consensus

In this section we formally prove that Algorithm 1 solves the byzantine consensus problem with the fair bv-broadcast and without partial synchrony. (Appendix B provides a counter-example illustrating why the algorithm does not terminate without the fair broadcast.) In particular, we apply a strategy used for crash fault tolerant randomized consensus [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] to our context to prove both the safety (Section 5.1) and liveness (Section 5.2) of the determinstic byzantine consensus algorithm.

Safety

Under no fairness assumption, one can prove the safety properties-agreement and validity-of the byzantine consensus based on bv-broadcast. Precisely, we formulate these properties in LTL and want to establish that they hold on the threshold automaton of Fig. 3.

Agreement requires that no two correct processes disagree, that is, if one process decides v then no process should decide 1-v for all binary values v ∈ {0, 1}. Thus, we want to prove that the following formula holds for both values of v:

∀R ∈ N, ∀R ∈ N ♦ κ[D v , R] = 0 ⇒ κ[D 1-v , R ] = 0 , (Agree v )
stating that for any two superrounds R and R , if eventually a process decides v, then globally (in any superround) no process will decide 1v. In terms of the TA from Fig. 3, if a process enters location D v no process should enter location D 1-v (not only in that superround, but in any other).

Validity requires that if no process proposes a value v ∈ {0, 1}, no process should ever decide that value. Hence, we want to prove the following formula for both values of v:

∀R ∈ N κ[V v , 1] = 0 ⇒ κ[D v , R] = 0 , (Valid v )
stating that if initially no process has value v, then globally (in any superround) no process decides v. In terms of the TA, if location V v is initially empty (in superround 1), then no process should enter location D v in any superround.

ByMC can only check formulas of the form ∀R ∈ N ϕ[R] (see Appendix A). Thus, automatically checking (Agree v ) and (Valid v ) is non-trivial, as they both involve two superround numbers: R and R in (Agree v ), and 1 and R in (Valid v ). We instead check well-chosen one-superround invariants (Inv1 v ) and (Inv2 v ):

∀R ∈ N ♦ κ[D v , R] = 0 ⇒ κ[D 1-v , R] = 0 ∧ κ[E 1-v , R] = 0 , (Inv1 v ) ∀R ∈ N κ[V v , R] = 0 ⇒ κ[D v , R] = 0 ∧ κ[E v , R] = 0 . (Inv2 v )
The choice of these invariants follows a previous approach used for the crash fault tolerant consensus [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] where Proposition 2 claims that correctness of these invariants implies correctness of (Agree v ) and (Valid v ). This easily follows from the fact that (i) emptiness of D 0 and E 0 in one superround leads to the emptiness of V 0 in the next superround, and (ii) emptiness of E 1 (and D 1 ) in one superround leads to the emptiness of V 1 in the next superround. Therefore, in order to prove agreement and validity, we only need to prove (Inv1 v ) and (Inv2 v ) for both values v ∈ {0, 1}. We successfully do this automatically with ByMC (see Section 6).

Liveness

We now aim at proving termination of Algorithm 1. First, we need to prove that every superround eventually terminates, in the sense that for every round eventually there are no processes in any location to the exception of the final ones (D 0 , E 0 and E 1 ). Formally, using ByMC we prove the following:

∀R ∈ N ♦ L∈L\{D 0 ,E 0 ,E 1 } κ[L, R] = 0 . (SRoundTerm)
From this property and the shape of the TA from Fig. 3, it easily follows that if no process ever enters E 0 and E 1 of some superround, then all processes visit D 0 in that superround. Similarly, if no process ever enters E 0 and E 1 of some superround, then all processes visit D 1 in that superround. This allows us to express termination as the following LTL property on the threshold automaton of Fig. 3:

∃R ∈ N κ[E 0 , R] = 0 ∧ κ[E 1 , R] = 0 ∨ κ[E 0 , R] = 0 ∧ κ[E 1 , R] = 0 . (Term)
In words, there is a superround R in which either (i) all processes visit D 1 , or (ii) all processes visit D 0 . Here again formula (Term) is non-trivial to check since it contains an existential quantifier over supperrounds, that cannot be handled by the model checker ByMC. Adapting the technique from [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]Section 7] to a non-randomized context, it is sufficient to prove a couple of properties on the threshold automaton of Fig. 3, that we detail below. The first property expresses that if no process starts a superround R with value v, then all processes decide 1-v in superround R:

∀R ∈ N κ[V 0 , R] = 0 ⇒ κ[E 0 , R] = 0 ∧ κ[E 1 , R] = 0 ∧ κ[V 1 , R] = 0 ⇒ κ[E 0 , R] = 0 ∧ κ[E 1 , R] = 0 . (Dec)
The second property claims that (i) emptiness of M 0 in superround R implies (emptiness of E 0 and therefore also) emptiness of D 0 and E 0 in R and (ii) emptiness of M 1 in superround R implies emptiness of E 1 in R:

∀R ∈ N κ[M 0 , R] = 0) ⇒ (κ[D 0 , R] ∧ κ[E 0 , R] = 0) ∧ κ[M 1 , R] = 0) ⇒ κ[E 1 , R] = 0 . (Good)
The main idea is to exploit the fairness of bv-broadcast, which ensures the existence of a round r which is (r mod 2)-good. Intuitively, the next superround R = r/2 is the desired witness for (Term), namely the one in which all processes decide (not necessarily for the first time). We formalize this in our main result: Theorem 1. Assuming fairness of the bv-broadcast, the byzantine consensus algorithm (Algorithm 1) terminates.

Proof. First we prove formulas (SRoundTerm) and (Dec) and (Good) automatically using the model checker ByMC. Formula (SRoundTerm) guarantees that formula (Term) indeed expresses termination. Next, we show that formulas (Dec) and (Good) together imply (Term). Indeed, since we assume fairness of the bv-broadcast, from Corollary 1 we know that there is a superround R in which one of the following two scenarios happen:

• κ[M 1 , R] = 0. In this case formula (Good) implies κ[E 1 , R] = 0. Note that the form of the (dotted) roundswitch rules yield that no process starts the superround R+1 with value 1, that is, we have κ[V 1 , R+1] = 0. Then formula (Dec) implies κ[E 0 , R+1] = 0 ∧ κ[E 1 , R+1] = 0 , which makes formula (Term) true, that is, all processes visit D 0 in superround R+1.

• κ[M 0 , R] = 0. In this case formula (Good) implies (κ[D 0 , R] ∧ κ[E 0 , R] = 0) . Now the round-switch rules yield that no process starts the superround R+1 with value 0, that is, we have κ[V 0 , R+1] = 0. Then formula (Dec) implies κ[E 0 , R+1] = 0 ∧ κ[E 1 , R+1] = 0 , which satisfies formula (Term), that is, all processes visit D 1 in R+1. As a consequence, our automated proofs of properties (SRoundTerm) and (Dec) and (Good) guarantee termination of Algorithm 1 under fairness of bv-broadcast.

Threshold automaton Size

Property # schemas Avg. schema length Time bv-broadcast (Fig. 1) The bv-broadcast and the composite automaton were verified on a laptop with Intel® Core™ i7-1065G7 CPU @ 1.30GHz × 8 and 32 GB of memory. The naive automaton timed-out even on a 4 AMD Opteron 6276 16-core CPU with 64 cores at 2300MHz with 64 GB of memory. Good and Dec are only relevant for the composite automaton. Although not indicated here, we also generated a counter-example of Inv1 0 for n > 3t on the composite automaton in ~4s. The specification of the termination for ByMC is deferred to Appendix F.

4

Experiments and Conclusions

Through composition, we model checked the safety but also the liveness of byzantine consensus for any parameters t and n > 3t. Table 2 demonstrates the relevance of our approach as it allows to verify the byzantine consensus automatically in less than 70 seconds whereas a non-compositional approach could not make it in less than a day. Our results imply that our notion of fairness is a sufficient assumption to cope with the impossibility of solving consensus in asynchronous setting. In this sense, this work is a step towards addressing "the need for more refined models of distributed computing that better reflect realistic assumptions" that was raised as an open question in [START_REF] Michael | Impossibility of distributed consensus with one faulty process[END_REF].

A Reducing multi-round TA to one-round TA Let us first formally define a (finite or infinite) run in a (one-round or multi-round) counter system Sys(TA). It is an alternating sequence of configurations and transitions σ 0 , t 1 σ 1 , t 2 , . . . such that σ 0 ∈ I is an initial configuration and for every i ≥ 1 we have that t i is unlocked in σ i-1 , and executing it leads to σ i , denoted t i (σ i-1 ) = σ i .

Here we briefly describe the reasoning behind the reduction of multi-round TAs to one-round TAs [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]Theorem 6]. Note that the behavior of a process in one round only depends on the variables (the number of messages) of that round. Namely, we check if a transition is unlocked in a round by evaluating a guard and a location counter in that round. This allows us to modify a run by swapping two transitions from different rounds, as they do not affect each other, and preserve LTL -X properties, which are properties expressed in LTL without the next operator X . The type of swapping we are interested in is the one where a transition of round R is followed by a transition of round R < R. Starting from any (fully asynchronous) run, if we keep swapping all such pairs of transitions, we will obtain a run in which processes synchronize at the end of each round and which has the same LTL -X properties as the initial one. This, so-called round-rigid structure, allows us to isolate a single round and analyze it. Still, different rounds might behave differently as they have different initial configurations. If we have a formula ∀R ∈ N. ϕ[R], where ϕ[R] is in the above mentioned fragment of (multi-round) LTL, then Theorem 6 of [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] shows exactly that it is equivalent to check that (i) this formula holds (or ϕ[R] holds on all rounds R) on a multi-round TA, and (ii) formula ϕ [START_REF] Aguilera | Consensus with byzantine failures and little system synchrony[END_REF] (or just ϕ) holds on the one-round TA (naturally obtained from the TA by removing dotted round-switch rules) with respect to all possible initial configurations of all rounds. Thus, we can verify properties of the form ∀R ∈ N. ϕ[R] on multi-round threshold automata, by using ByMC to check ϕ on a one-round threshold automaton with an enlarged set of initial configurations.

B Examples of fairness and of non-termination without fairness

First, we explain that the fairness is satisfied as soon as one execution of bv-broadcast has correct processes delivering all values broadcast by correct processes first. Then, we explain that the byzantine consensus algorithm cannot terminate without an additional assumption, like fairness.

Relevance of the fairness assumption.

It is interesting to note that our fairness assumption is satisfied by the existence of an execution with a particular reception order of some messages of the two broadcasts within the bv-broadcast. Consider that t = n/3 -1 and that at the beginning of a round r, the two following properties hold: (i) estimate r mod 2 is more represented than estimate (1r) mod 2 among correct processes and (ii) all correct processes deliver the values broadcast by correct processes before any value broadcast during the bv-broadcast by byzantine processes are delivered. Indeed, the existence of such a round r in any infinite sequence of executions of bv-broadcast implies that this sequence is fair (Def. 2): as r mod 2 is the only value that can be broadcast by t+1 correct processes, this is the first value that is received from t+1 distinct processes and rebroadcast by the rest of the correct processes. This is thus also the first value that is bv-delivered by all correct processes. Non-termination without fairness. It is interesting to note why Algorithm 1 does not solve consensus when t < n/3 and without our fairness assumption. We exhibit an example of execution of the algorithm with n = 4 and f = 1, starting at round r and for which the estimates of the correct processes are kept as (1r) mod 2, (1r) mod 2, r mod 2 in rounds r and r+2. Repeating this while incrementing r yields an infinite execution, so that the algorithm never terminates. Lemma 2. Algorithm 1 does not terminate without fairness.

Proof. Consider, for example, processes p 1 , p 2 , p 3 and p 4 where p 4 is byzantine and where 0, 0, 1 are the input values of the correct processes p 1 , p 2 , p 3 , respectively, at round 1. We show that at the beginning of round 2, p 1 , p 2 , p 3 have estimates 0, 1, 1. First, as a result of the broadcast (line 2), consider that p 1 and p 2 receive 0 from p 1 , p 2 and p 4 so that p 1 , p 2 bv-deliver 0. Second, p 2 and p 3 receive 1 from p 3 , p 4 and finally p 2 so that p 2 , p 3 bv-deliver 1. Third, p 3 receives 0 from p 0 , p 2 and finally from p 3 itself, hence p 3 bv-delivers 0. Now we have: (a) p 1 , p 2 , p 3 bv-deliver 0, 0, 1 and (b) p 2 , p 3 later bv-deliver 1 and 0, respectively. As a result of (a), we have p 1 , p 2 broadcast, and say p 4 sends, AUX, 0, • so that p 0 receives these three messages, p 1 , p 2 broadcast AUX, 0, • , and say p 4 sends, AUX, 1, • to p 2 so that p 2 receives these messages, p 1 broadcasts AUX, 0, • while p 3 broadcasts, and say p 4 sends, AUX, 1, • so that p 3 receives these messages. Finally, by (b) we have contestants 2 = contestants 3 = {0, 1}. This implies that the nt first values inserted in favorites 1 , favorites 2 and favorites 3 in round r are values {0}, {0, 1}, {0, 1}, respectively. Finally, qualifiers 1 , qualifiers 2 and qualifiers 3 are {0}, {0, 1} and {0, 1}, respectively. And p 1 , p 2 , p 3 set their estimate to 0, 1, 1.

It is easy to see that a symmetric execution in round r = r + 1 leads processes to change their estimate from 0, 1, 1 to 0, 0, 1 looping back to the state where r mod 2 = 1 and estimate are (1r) mod 2, (1r) mod 2, r mod 2.

C Starting a round with identical estimate

Lemma 3 (Lemma 1). If the infinite sequence of bv-broadcast invocations of Algorithm 1 is fair, with the r th invocation (in round r) being (r mod 2)-good, then all correct processes start round r+1 of Algorithm 1 with estimate r mod 2.

Proof. The argument is that all correct processes wait until a growing prefix of the bv-delivered values that are re-broadcast implies that there is a subset of favorites, called qualifiers, containing messages from nt distinct processes such that ∀v ∈ qualifiers. v ∈ contestants. As we assume that the infinite sequence of bv-broadcast invocations of Algorithm 1 is fair, with the r th invocation being (r mod 2)-good, then we know that in round r for every pair of correct processes p i and p j we have p i .qualifiers ⊆ p j .qualifiers or p j .qualifiers ⊆ p i .qualifiers. If p i .qualifiers = p j .qualifiers for all pairs, then by examination of the code, we know that they will set their estimate est to the same value depending on the parity of the current round.

Consider instead, with no loss of generality, that p i .qualifiers is a strict subset of p j .qualifiers in round r. As their values can only be binaries, in {0, 1}, this means that p i .qualifiers is a singleton, say {w}. As all correct processes bv-deliver r mod 2 first, which is then broadcast into p i .favorites, we have w = r mod 2 and p i 's estimate becomes r mod 2 at line 12. As p j .qualifiers is {0, 1}, the estimate of p j is also set to r mod 2 but at line 14.

D Large TA

b 0 ≥ 2t+1-f a 0 ++ r 4 b 1 ≥ t+1-f b 1 ++ r 5 b 0 ≥ t+1-f b 0 ++ r 6 b 1 ≥ 2t+1-f a 1 ++ r 14 , r 15 , r 16 a 0 ≥ n-t-f - r 8 b 1 ≥ t+1-f b 1 ++ r 9 b 1 ≥ 2t+1-f a 1 ++ r 10 b 0 ≥ 2t+1-f a 0 ++ r 11 b 0 ≥ t+1-f b 0 ++ r 12 b 1 ≥ 2t+1-f - r 13 b 0 ≥ 2t+1-f - r 7 , r 18 , r 19 a 1 ≥ n-t-f - r 16 a 0 ≥ n-t-f - r 17
a 0 +a 1 ≥ n-t-fr 20 , r 21 , r 22 true -Table 3: The rules of the threshold automaton from Fig. 2. We omit self loops that have trivial guard true and no update.

E Missing proof of Corollary 1

We restate here Corollary 1 and give its proof.

Corollary 1. Let r ∈ N be such that the r th execution of bv-broadcast in Algorithm 1 is (r mod 2)-good. Then:

• If there exists R ∈ N with r = 2R-1, then κ[M 0 , R] = 0) holds.

• If there exists R ∈ N with r = 2R, then (κ[M 1 , R] = 0 holds.

Proof. By definition of an (r mod 2)-good execution, we know that in this particular invocation of bv-broadcast, all correct processes bv-deliver r mod 2 first. It follows from Lemma 1, that all correct processes start the next round with estimate set to r mod 2. There are two cases to consider depending on the parity of the round: If r mod 2 = 1, then this is the first round of superround R, i.e., r = 2R -1. As a result, κ[M 0 , R] = 0 . If r mod 2 = 0, then this is the second round of superround R, i.e., r = 2R. As a result, κ[M 1 , R] = 0 .

F Specification of the termination property in the simplified threshold automaton for consensus algorithm

The reliable communication assumption and the properties guaranteed by the bv-broadcast are expressed as preconditions for s_round_termination. The progress conditions work exactly the same as in [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]. However, since the shared counters representing the bv-broadcast execution do not represent regular messages, we cannot directly use the reliable communication assumption. Instead, we use the properties of the bv-broadcast that we proved in a separate automaton.

In practice, instead of using progress preconditions on the bv-broadcast counters in s_round_termination, such as: One can note that we do not use BV-Justification as a precondition in this specification. Instead, the BV-Justification property is baked in the structure of the simplified threshold automaton (in the guard of the transition M → M0, M1).

The complete specification of the termination property follows:

Figure 1 :

 1 Figure 1: The pseudocode of the binary value broadcast (left) and its threshold automaton (right)

r 2 :

 2

Figure 2 :

 2 Figure2: The naive threshold automaton of the byzantine consensus of Algorithm 1 where the embedded bv-broadcast automaton is depicted with dashed arrows. Precise formulations of all rules are in Appendix D. Note that the rules r 20 , r 21 and r 22 represent transitions from the end of an odd round to the beginning of the following (even) round of Algorithm 1, while the dotted edges represent transitions from the end of an even round to the beginning of the following (odd) one.

(

  locM == 0 || bvb1 < 1) && (locM == 0 || bvb0 < 1) && (locM1 == 0 || bvb0 < 1) && (locM0 == 0 || bvb1 < 1) we use the following: / * BV-Termination * / (locM == 0) && / * BV-Obligation * / (locM1 == 0 || bvb0 < T + 1) && (locM0 == 0 || bvb1 < T + 1) && / * BV-Uniformity * / (locM1 == 0 || aux0 == 0) && (locM0 == 0 || aux1 == 0) &&

  -Obligation * / (locM1 == 0 || bvb0 < T + 1) && (locM0 == 0 || bvb1 < T + 1) && / * BV-Uniformity * / (locM1 == 0 || aux0 == 0) && (locM0 == 0 || aux1 == 0) && / * Business as usual * /(locM1 == 0 || aux1 < N -T) && (locM0 == 0 || aux0 < N -T) && (locM01 == 0 || aux0 + aux1 < N -bvb1x < T + 1) && / * BV-Uniformity * / (locM1x == 0 || aux0x == 0) && (locM0x == 0 || aux1x == 0) && (locM1x == 0 || aux1x < N -T) && (locM0x == 0 || aux0x < N -T) && (locM01x == 0 || aux1x < N -T) && (locM01x == 0 || aux0x < N -T) && (locM01x == 0 || aux0x + aux1x < N -: <>(locD0 != 0) -> [](locD1 == 0 && locE1x == 0); inv2 _ 0: [](locV0 == 0) -> [](locD0 == 0 && locE0x == 0); inv1 _ 1: <>(locD1 != 0) -> [](locD0 == 0 && locE0x == 0); inv2 _ 1: [](locV1 == 0) -> [](locD1 == 0 && locE1x == 0); dec _ 0: [](locV0 == 0) -> [](locE0 == 0 && locE1 == 0); dec _ 1: [](locV1 == 0) -> [](locE0x == 0 && locE1x ==0); good _ 0: [](locM0 == 0) -> [](locD0 == 0 && locE0x == 0); good _ 1: [](locM1x == 0) -> [](locE1x == 0);

Table 1 :

 1 The locations of correct processes

Table 2 :

 2 Experiments. We used the parallelized version of ByMC 2.4.4 with MPI.

		unique	BV-Just 0	90	54	5.61s
		guards	BV-Obl 0	90	79	6.87s
		10 locations	BV-Unif 0	760	97	27.64s
		19 rules	BV-Term	90	79	6.75s
		14 unique	Inv1 0	>100 000	-	>24h
	Naive consensus (Fig. 2)	guards 24 locations	Inv2 0 SRound-Term >100 000 >100 000	--	>24h >24h
		45 rules
		10 unique	Inv1 0	6	102	4.68s
	Composite consensus (Fig. 3)	guards 16 locations	Inv2 0 SRound-Term 2 2	73 109	4.56s 4.13s
		37 rules	Good 0	2	67	4.55s
			Dec 0	2	73	4.62s

Table 3

 3 details the rules for the first half of the threshold automaton from Fig.2.

	Rules	Guard	Update
	r 1	true	b 0 ++
	r 2	true	b 1 ++
	r 3

We refer to a deterministic consensus algorithm as a consensus algorithm that satisfies linear temporal properties such as safety (agreement, validity) and liveness (termination), even if the environment (e.g., communication delays, scheduler) introduces non-determinism in the algorithm execution.

The progress assumption is in the literature sometimes referred as fairness, but here we want to avoid confusion with the fairness from Section

Acknowledgments

This research is supported under Australian Research Council Future Fellowship funding scheme (project number 180100496) entitled "The Red Belly Blockchain: A Scalable Blockchain for Internet of Things".