From ab9e7a693be7982b6b8d8f2e2dc3ffad00f22237 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Mon, 13 Jan 2025 10:15:10 +0100 Subject: [PATCH 1/2] agreement for multiple heights (#749) --- specs/consensus/quint/statemachineAsync.qnt | 28 +++++++++++++++------ 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/specs/consensus/quint/statemachineAsync.qnt b/specs/consensus/quint/statemachineAsync.qnt index 19db6487c..578f32380 100644 --- a/specs/consensus/quint/statemachineAsync.qnt +++ b/specs/consensus/quint/statemachineAsync.qnt @@ -23,6 +23,7 @@ export driver.* import consensus.* from "./consensus" export consensus.* import votekeeper.* from "./votekeeper" +import extraSpells.* from "./spells/extra" const validators: Set[Address] const validatorSet: Address -> Weight @@ -65,10 +66,13 @@ action unchangedAll = all { _hist' = _hist } +/// Any two processes agree in the consensus instances in which they both have already decided val AgreementInv = tuples(Correct, Correct).forall(p => - (system.get(p._1).es.chain != List() and system.get(p._2).es.chain != List()) - implies - system.get(p._1).es.chain[0] == system.get(p._2).es.chain[0]) + val numDecidedInstances = min( system.get(p._1).es.chain.length(), + system.get(p._2).es.chain.length()) + to(0, numDecidedInstances-1).forall(i => + system.get(p._1).es.chain[i] == system.get(p._2).es.chain[i]) +) // Actions action init = all { @@ -224,13 +228,21 @@ action deliverSomeCertificate(v: Address) : bool = all { } -// deliver a message or a certiciate. +// deliver a message or a certificate. // Take it from the network buffer of from the faulty set and put it into the incoming sets action deliver(v: Address) : bool = any { - nondet prop = oneOf(propBuffer.get(v).union(AllFaultyProposals)) - deliverProposal(v, prop), - nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes)) - deliverVote(v, vote), + val props = propBuffer.get(v).union(AllFaultyProposals) + all{ + props.size() > 0, + nondet prop = oneOf(props) + deliverProposal(v, prop), + }, + val votes = voteBuffer.get(v).union(AllFaultyVotes) + all { + votes.size() > 0, + nondet vote = oneOf(votes) + deliverVote(v, vote), + }, deliverSomeCertificate(v), // we might do fault injection here. But faulty nodes cannot // totally make up certificates. They cannot forge messages to look // like being sent by correct nodes From 304c8ee5e938c4270ad038e30c284712f47f9195 Mon Sep 17 00:00:00 2001 From: Daniel Date: Mon, 13 Jan 2025 12:38:35 +0100 Subject: [PATCH 2/2] feat(spec): Requirements for the proposer selection algorithm (#739) * spec/consensus: improvements in Tendermint overview * spec/consensus: improvements in Tendermint overview * spec/consensus: precommit step reviewed * spec/consensus: added exit conditions section * spec/consensus: exit conditions section updated * spec/consensus: messages section updated * spec/consensus: proposals section reviewed * spec/consensus: proposals section and equivocation * spec/consensus: votes section reviewed * spec/consensus: votes section and equivocation * spec/consensus: proposer selection inputs/outputs * spec/consensus: proposer selection * spec/consensus: proposer selection correctness * Merge branch 'main' into cason/396-proposer-selection * spec/consensus: proposer selection correctness * spec/consensus: proposer selection correctness 2 * spec/consensus: proposer selection fairness * spec/consensus: proposer selection fairness 2 * spec/consensus: misbehavior and proposer selection * spec/consensus: removing some 'validator' entries * spec/consensus: stateful proposer selection fairness * spec/consensus: stateful proposer selection --- specs/consensus/misbehavior.md | 35 +++++++++----- specs/consensus/overview.md | 84 ++++++++++++++++++++++++++++++---- 2 files changed, 98 insertions(+), 21 deletions(-) diff --git a/specs/consensus/misbehavior.md b/specs/consensus/misbehavior.md index 6fa0ecc1a..d0795d69e 100644 --- a/specs/consensus/misbehavior.md +++ b/specs/consensus/misbehavior.md @@ -69,19 +69,20 @@ constitute a source of information for social or legal actions after-the-fact. CometBFT only record specific misbehavior, namely the [duplicate vote evidence](https://github.com/cometbft/cometbft/blob/main/spec/core/data_structures.md#duplicatevoteevidence). While attacks are rare, such behavior has been observed as a result of -misconfiguration. Most companies operating a validator typically implement this +misconfiguration. Most companies operating a consensus process (also known as a +_validator_) typically implement this node as a fault-tolerant setup itself, having copies of the private key of the -validator on multiple machines. If such a fault-tolerant setup is implemented +process on multiple machines. If such a fault-tolerant setup is implemented poorly or misconfigured, this may result in duplicate (and sometimes conflicting) signatures in a protocol step, although no actual attack was intended. Still, such behavior may be used for mild penalties (e.g., not paying fees to the validator for some time, taking a small penalty of their stake), as -part of the incentivization scheme motivating validator operators to fix such +part of the incentivization scheme motivating operators to fix such issues and ensure reliability of their node. While a single instance of an unintentional double vote of one process does not pose big problems (it cannot bring disagreement), repeated unintentional -double votes by several validator operators having large voting power might +double votes by several processes having large voting power might eventually lead to disagreement and a chain halt. Therefore it make sense to incentivize individual operators to fix their setup while the whole system is still operational. @@ -121,26 +122,34 @@ a small proposal message carrying only the has of the value, and the big proposa is run. Observe that the way it is typically implemented, `proposer(h, r)` is not a -"mathematical function" that takes as input the height and the round and -produces an ID. Rather it is typically implemented as a stateful function that -is based on priorities. The latter depend on voting powers and who has been -proposer in previous heights. +"mathematical function" that takes as input the height, the round, and the set +of processes running that height and returns a process. +Rather it is typically implemented as a function that keeps an internal state, +for instance to represent the process priorities, as in the case of +the [proposer selection procedure of CometBFT][cometbft-proposer]. +The latter depends on voting powers and who has been proposer in previous +heights. Verification is more complex than double vote and double propose: - In contrast to double vote, where it is still trivial to verify the misbehavior evidence a week after it was generated, in order to verify bad - proposer we need knowledge on the validator priorities at that time. + proposer we may need knowledge of the internal state of the proposer selection + algorithm at that time. - multiple layers are involved - maintaining and updating voting powers is typically an application level concern - - the `proposer(h, r)` function is situated at the consensus level + - the [`proposer(h, r)` function](./overview.md#proposer-selection) is + situated at the consensus level - misbehavior detection can only happen at consensus level - in order to use the evidence, the application must be able to verify the evidence. This this case it means that the application must - - be aware of the consensus-level `proposer` function and priorities, namely, be able to reproduce the output of `proposer(h, r)` for any given state + - be aware of the consensus-level `proposer(h, r)` function and its + internal state, namely, be able to reproduce the output of + `proposer(h, r)` for any given height - potentially have historical data (the evidence might come a couple of - blocks after the fact) on validator sets + blocks after the fact) on the set of processes running consensus at + multiple heights ### What cannot be done @@ -202,3 +211,5 @@ The change to Tendermint is just that prevote messages have an additional field that carries the content of the `vr` field of the proposal that triggered the sending of the prevote. See [Accountable Tendermint](./accountable-tm/README.md) for more details. + +[cometbft-proposer]: https://github.com/cometbft/cometbft/blob/main/spec/consensus/proposer-selection.md diff --git a/specs/consensus/overview.md b/specs/consensus/overview.md index 96578343c..1cd217433 100644 --- a/specs/consensus/overview.md +++ b/specs/consensus/overview.md @@ -411,19 +411,84 @@ correct behaviour provided that `p` is able to prove the existence of a ## Functions -The [pseudo-code][pseudo-code] of the consensus algorithm includes calls to -functions that are not defined in the pseudo-code itself, but are assumed to be +The [pseudo-code][pseudo-code] of the algorithm includes calls to functions +that are not defined in the pseudo-code itself, but are assumed to be implemented by the processes running the consensus protocol. ### Proposer Selection -The first external function is `proposer(h, r)` that returns the process -selected as the proposer of round `r` of height `h` of consensus. The roles of -the proposer of a round are described in the [propose round step](#propose). - -> The formalization of the properties requires for the proposer selection -> algorithm is a work in progress, see -> https://github.com/informalsystems/malachite/issues/396. +The `proposer(h, r)` function receives a height `h >= 0` and a round `r >= 0` +and returns the process, among the processes running height `h`, selected as +the proposer of round `r` of height `h`. +The role of the proposer is described in the [`propose`](#propose) round step. + +The `proposer(h, r)` function requires the knowledge of the set of processes +running the height `h` of consensus. +The set of processes running a given height of consensus is fixed: +it cannot vary over rounds. +But different heights on consensus may be run by distinct set of processes and +processes may have distinct associated [voting powers](#voting-power) in different heights. + +#### Determinism + +Given a consensus height `h` and the set of processes running height `h`, +the `proposer(h, r)` function **must be deterministic**. +This means that any two correct processes that invoke `proposer(h, r)` with the +same inputs, including the implicit input that is the set of processes running +consensus height `h` and associated voting powers, should receive the exactly +same output (process). + +#### Correctness + +The main goal of the `proposer(h, r)` function is to eventually select a +correct process to coordinate a round of consensus and to propose an +appropriate value for it. +A correct implementation of the function must guarantee that, for every height +`h`, there is a round `r* >= 0` where `proposer(h, r*)` returns a process `p` +that is a correct process: `p` does not misbehave nor crash. + +Fortunately, it is relatively simple to produce a correct implementation of the +`proposer(h, r)` method: it is enough to ensure that every process running +consensus height `h` is selected as the proposer for at least one round. +In other words, it is enough that processes take turns as the proposers of +different rounds of a height. + +#### Fairness + +Tendermint is a consensus algorithm that adheres to the _rotating coordinator_ +approach. +This means that the role of coordinating rounds and proposing values is +expected to be played by different processes over time, in successive +heights of consensus. +(In contrast to the _fixed coordinator_ approach, where the coordinator or +proposer is only replaced when it is suspected to be faulty). + +While a correct `proposer(h, r)` implementation eventually selects every +process as the proposer of a round of height `h`, being the proposer of the +first round of a height is the most relevant role, since most heights of +consensus are expected to be finalized in round 0. +A fair proposer selection algorithm should therefore ensure that all processes +have, over a reasonable long sequence of heights `h`, a similar chance of being +selected as `proposer(h, 0)`, thus to propose the value that is most likely to be +decided on that height. + +In the case of Proof-of-Stake (PoS) blockchains, where processes are assumed to +have distinct voting powers, a fair proposer selection algorithm should ensure +that every process is chosen, over a reasonable long sequence of heights, as +`proposer(h, 0)` in a number of heights `h` that is proportional to its voting +power. +Observe that when the set of processes running consensus varies over heights, +so as the voting power associated to each process, producing a fair proposer +selection algorithm becomes more challenging. + +> The [proposer selection procedure of CometBFT][cometbft-proposer], which +> implements Tendermint in Go, is a useful reference of how a fair proposer +> selection can be achieved with a dynamic set of processes and voting powers. +> It is worth noting that this algorithm maintains an internal state, which is +> updated whenever a new proposer is selected. +> This means that reproducing the algorithm output requires, in addition to the +> inputs mentioned in the [Determinism section](#determinism), retrieving or +> recomputing the associated algorithm's internal state. ### Proposal value @@ -487,3 +552,4 @@ to the current time plus the duration returned by the corresponding functions [pseudo-code]: ./pseudo-code.md [tendermint-arxiv]: https://arxiv.org/abs/1807.04938 [accountable-tendermint]: ./misbehavior.md#misbehavior-detection-and-verification-in-accountable-tendermint +[cometbft-proposer]: https://github.com/cometbft/cometbft/blob/main/spec/consensus/proposer-selection.md