|
@ -37,33 +37,42 @@ _AppHash_, _TxResults_, _ConsensusParams_, and _ValidatorUpdates_, or |
|
|
(b) log an error if the Application is in next-block execution mode and _does_ provide values for |
|
|
(b) log an error if the Application is in next-block execution mode and _does_ provide values for |
|
|
_AppHash_, _TxResults_, _ConsensusParams_, or _ValidatorUpdates_ (the values provided will be ignored). |
|
|
_AppHash_, _TxResults_, _ConsensusParams_, or _ValidatorUpdates_ (the values provided will be ignored). |
|
|
|
|
|
|
|
|
* Requirement 3 [`PrepareProposal`, `ProcessProposal`, coherence]: For any two correct processes $p$ and $q$, |
|
|
|
|
|
|
|
|
* Requirement 3 [`PrepareProposal`, timeliness] If $p$'s Application fully executes prepared blocks in |
|
|
|
|
|
`PrepareProposal` and the network is in a synchronous period while processes $p$ and $q$ are in $r_p$, |
|
|
|
|
|
then the value of _TimeoutPropose_ at $q$ must be such that $q$ does not prevote _nil_ in $r_p$ due to |
|
|
|
|
|
$q$'s propose timer timing out. |
|
|
|
|
|
|
|
|
|
|
|
Full execution of blocks at `PrepareProposal` time stands on Tendermint's critical path. Thus, |
|
|
|
|
|
Requirement 3 ensures the Application will set a value for _TimeoutPropose_ such that the time it takes |
|
|
|
|
|
to fully execute blocks in `PrepareProposal` does not interfere with Tendermint's propose timer. |
|
|
|
|
|
|
|
|
|
|
|
* Requirement 4 [`PrepareProposal`, `ProcessProposal`, coherence]: For any two correct processes $p$ and $q$, |
|
|
if $q$'s Tendermint calls `RequestProcessProposal` on $v'_p$, |
|
|
if $q$'s Tendermint calls `RequestProcessProposal` on $v'_p$, |
|
|
$q$'s Application returns Accept in `ResponseProcessProposal`. |
|
|
$q$'s Application returns Accept in `ResponseProcessProposal`. |
|
|
|
|
|
|
|
|
Requirement 3 makes sure that blocks proposed by correct processes _always_ pass the correct receiving process's |
|
|
|
|
|
|
|
|
Requirement 4 makes sure that blocks proposed by correct processes _always_ pass the correct receiving process's |
|
|
`ProcessProposal` check. |
|
|
`ProcessProposal` check. |
|
|
On the other hand, if there is a deterministic bug in `PrepareProposal` or `ProcessProposal` (or in both), |
|
|
On the other hand, if there is a deterministic bug in `PrepareProposal` or `ProcessProposal` (or in both), |
|
|
strictly speaking, this makes all processes that hit the bug byzantine. This is a problem in practice, |
|
|
strictly speaking, this makes all processes that hit the bug byzantine. This is a problem in practice, |
|
|
as very often validators are running the Application from the same codebase, so potentially _all_ would |
|
|
as very often validators are running the Application from the same codebase, so potentially _all_ would |
|
|
likely hit the bug at the same time. This would result in most (or all) processes prevoting `nil`, with the |
|
|
likely hit the bug at the same time. This would result in most (or all) processes prevoting `nil`, with the |
|
|
serious consequences on Tendermint's liveness that this entails. Due to its criticality, Requirement 3 is a |
|
|
|
|
|
|
|
|
serious consequences on Tendermint's liveness that this entails. Due to its criticality, Requirement 4 is a |
|
|
target for extensive testing and automated verification. |
|
|
target for extensive testing and automated verification. |
|
|
|
|
|
|
|
|
* Requirement 4 [`ProcessProposal`, determinism-1]: `ProcessProposal` is a (deterministic) function of the current |
|
|
|
|
|
|
|
|
* Requirement 5 [`ProcessProposal`, determinism-1]: `ProcessProposal` is a (deterministic) function of the current |
|
|
state and the block that is about to be applied. In other words, for any correct process $p$, and any arbitrary block $v'$, |
|
|
state and the block that is about to be applied. In other words, for any correct process $p$, and any arbitrary block $v'$, |
|
|
if $p$'s Tendermint calls `RequestProcessProposal` on $v'$ at height $h$, |
|
|
if $p$'s Tendermint calls `RequestProcessProposal` on $v'$ at height $h$, |
|
|
then $p$'s Application's acceptance or rejection **exclusively** depends on $v'$ and $s_{p,h-1}$. |
|
|
then $p$'s Application's acceptance or rejection **exclusively** depends on $v'$ and $s_{p,h-1}$. |
|
|
|
|
|
|
|
|
* Requirement 5 [`ProcessProposal`, determinism-2]: For any two correct processes $p$ and $q$, and any arbitrary block $v'$, |
|
|
|
|
|
|
|
|
* Requirement 6 [`ProcessProposal`, determinism-2]: For any two correct processes $p$ and $q$, and any arbitrary block $v'$, |
|
|
if $p$'s (resp. $q$'s) Tendermint calls `RequestProcessProposal` on $v'$ at height $h$, |
|
|
if $p$'s (resp. $q$'s) Tendermint calls `RequestProcessProposal` on $v'$ at height $h$, |
|
|
then $p$'s Application accepts $v'$ if and only if $q$'s Application accepts $v'$. |
|
|
then $p$'s Application accepts $v'$ if and only if $q$'s Application accepts $v'$. |
|
|
Note that this requirement follows from Requirement 4 and the Agreement property of consensus. |
|
|
|
|
|
|
|
|
Note that this requirement follows from Requirement 5 and the Agreement property of consensus. |
|
|
|
|
|
|
|
|
Requirements 4 and 5 ensure that all correct processes will react in the same way to a proposed block, even |
|
|
|
|
|
|
|
|
Requirements 5 and 6 ensure that all correct processes will react in the same way to a proposed block, even |
|
|
if the proposer is Byzantine. However, `ProcessProposal` may contain a bug that renders the |
|
|
if the proposer is Byzantine. However, `ProcessProposal` may contain a bug that renders the |
|
|
acceptance or rejection of the block non-deterministic, and therefore prevents processes hitting |
|
|
acceptance or rejection of the block non-deterministic, and therefore prevents processes hitting |
|
|
the bug from fulfilling Requirements 4 or 5 (effectively making those processes Byzantine). |
|
|
|
|
|
|
|
|
the bug from fulfilling Requirements 5 or 6 (effectively making those processes Byzantine). |
|
|
In such a scenario, Tendermint's liveness cannot be guaranteed. |
|
|
In such a scenario, Tendermint's liveness cannot be guaranteed. |
|
|
Again, this is a problem in practice if most validators are running the same software, as they are likely |
|
|
Again, this is a problem in practice if most validators are running the same software, as they are likely |
|
|
to hit the bug at the same point. There is currently no clear solution to help with this situation, so |
|
|
to hit the bug at the same point. There is currently no clear solution to help with this situation, so |
|
@ -76,43 +85,43 @@ is about to broadcast a non-`nil` precommit message, a correct process can only |
|
|
Let $e^r_p$ be the vote extension that the Application of a correct process $p$ returns via `ResponseExtendVote` in round $r$, height $h$. |
|
|
Let $e^r_p$ be the vote extension that the Application of a correct process $p$ returns via `ResponseExtendVote` in round $r$, height $h$. |
|
|
Let $w^r_p$ be the proposed block that $p$'s Tendermint passes to the Application via `RequestExtendVote` in round $r$, height $h$. |
|
|
Let $w^r_p$ be the proposed block that $p$'s Tendermint passes to the Application via `RequestExtendVote` in round $r$, height $h$. |
|
|
|
|
|
|
|
|
* Requirement 6 [`ExtendVote`, `VerifyVoteExtension`, coherence]: For any two correct processes $p$ and $q$, if $q$ receives $e^r_p$ |
|
|
|
|
|
|
|
|
* Requirement 7 [`ExtendVote`, `VerifyVoteExtension`, coherence]: For any two correct processes $p$ and $q$, if $q$ receives $e^r_p$ |
|
|
from $p$ in height $h$, $q$'s Application returns Accept in `ResponseVerifyVoteExtension`. |
|
|
from $p$ in height $h$, $q$'s Application returns Accept in `ResponseVerifyVoteExtension`. |
|
|
|
|
|
|
|
|
Requirement 6 constrains the creation and handling of vote extensions in a similar way as Requirement 3 |
|
|
|
|
|
|
|
|
Requirement 7 constrains the creation and handling of vote extensions in a similar way as Requirement 4 |
|
|
contrains the creation and handling of proposed blocks. |
|
|
contrains the creation and handling of proposed blocks. |
|
|
Requirement 6 ensures that extensions created by correct processes _always_ pass the `VerifyVoteExtension` |
|
|
|
|
|
|
|
|
Requirement 7 ensures that extensions created by correct processes _always_ pass the `VerifyVoteExtension` |
|
|
checks performed by correct processes receiving those extensions. |
|
|
checks performed by correct processes receiving those extensions. |
|
|
However, if there is a (deterministic) bug in `ExtendVote` or `VerifyVoteExtension` (or in both), |
|
|
However, if there is a (deterministic) bug in `ExtendVote` or `VerifyVoteExtension` (or in both), |
|
|
we will face the same liveness issues as described for Requirement 3, as Precommit messages with invalid vote |
|
|
|
|
|
|
|
|
we will face the same liveness issues as described for Requirement 4, as Precommit messages with invalid vote |
|
|
extensions will be discarded. |
|
|
extensions will be discarded. |
|
|
|
|
|
|
|
|
* Requirement 7 [`VerifyVoteExtension`, determinism-1]: `VerifyVoteExtension` is a (deterministic) function of |
|
|
|
|
|
|
|
|
* Requirement 8 [`VerifyVoteExtension`, determinism-1]: `VerifyVoteExtension` is a (deterministic) function of |
|
|
the current state, the vote extension received, and the prepared proposal that the extension refers to. |
|
|
the current state, the vote extension received, and the prepared proposal that the extension refers to. |
|
|
In other words, for any correct process $p$, and any arbitrary vote extension $e$, and any arbitrary |
|
|
In other words, for any correct process $p$, and any arbitrary vote extension $e$, and any arbitrary |
|
|
block $w$, if $p$'s (resp. $q$'s) Tendermint calls `RequestVerifyVoteExtension` on $e$ and $w$ at height $h$, |
|
|
block $w$, if $p$'s (resp. $q$'s) Tendermint calls `RequestVerifyVoteExtension` on $e$ and $w$ at height $h$, |
|
|
then $p$'s Application's acceptance or rejection **exclusively** depends on $e$, $w$ and $s_{p,h-1}$. |
|
|
then $p$'s Application's acceptance or rejection **exclusively** depends on $e$, $w$ and $s_{p,h-1}$. |
|
|
|
|
|
|
|
|
* Requirement 8 [`VerifyVoteExtension`, determinism-2]: For any two correct processes $p$ and $q$, |
|
|
|
|
|
|
|
|
* Requirement 9 [`VerifyVoteExtension`, determinism-2]: For any two correct processes $p$ and $q$, |
|
|
and any arbitrary vote extension $e$, and any arbitrary block $w$, |
|
|
and any arbitrary vote extension $e$, and any arbitrary block $w$, |
|
|
if $p$'s (resp. $q$'s) Tendermint calls `RequestVerifyVoteExtension` on $e$ and $w$ at height $h$, |
|
|
if $p$'s (resp. $q$'s) Tendermint calls `RequestVerifyVoteExtension` on $e$ and $w$ at height $h$, |
|
|
then $p$'s Application accepts $e$ if and only if $q$'s Application accepts $e$. |
|
|
then $p$'s Application accepts $e$ if and only if $q$'s Application accepts $e$. |
|
|
Note that this requirement follows from Requirement 7 and the Agreement property of consensus. |
|
|
|
|
|
|
|
|
Note that this requirement follows from Requirement 8 and the Agreement property of consensus. |
|
|
|
|
|
|
|
|
Requirements 7 and 8 ensure that the validation of vote extensions will be deterministic at all |
|
|
|
|
|
|
|
|
Requirements 8 and 9 ensure that the validation of vote extensions will be deterministic at all |
|
|
correct processes. |
|
|
correct processes. |
|
|
Requirements 7 and 8 protect against arbitrary vote extension data from Byzantine processes |
|
|
|
|
|
similarly to Requirements 4 and 5 and proposed blocks. |
|
|
|
|
|
Requirements 7 and 8 can be violated by a bug inducing non-determinism in |
|
|
|
|
|
|
|
|
Requirements 8 and 9 protect against arbitrary vote extension data from Byzantine processes |
|
|
|
|
|
similarly to Requirements 5 and 6 and proposed blocks. |
|
|
|
|
|
Requirements 8 and 9 can be violated by a bug inducing non-determinism in |
|
|
`VerifyVoteExtension`. In this case liveness can be compromised. |
|
|
`VerifyVoteExtension`. In this case liveness can be compromised. |
|
|
Extra care should be put in the implementation of `ExtendVote` and `VerifyVoteExtension` and, |
|
|
Extra care should be put in the implementation of `ExtendVote` and `VerifyVoteExtension` and, |
|
|
as a general rule, `VerifyVoteExtension` _should_ always accept the vote extension. |
|
|
as a general rule, `VerifyVoteExtension` _should_ always accept the vote extension. |
|
|
|
|
|
|
|
|
* Requirement 9 [_all_, no-side-effects]: $p$'s calls to `RequestPrepareProposal`, |
|
|
|
|
|
|
|
|
* Requirement 10 [_all_, no-side-effects]: $p$'s calls to `RequestPrepareProposal`, |
|
|
`RequestProcessProposal`, `RequestExtendVote`, and `RequestVerifyVoteExtension` at height $h$ do |
|
|
`RequestProcessProposal`, `RequestExtendVote`, and `RequestVerifyVoteExtension` at height $h$ do |
|
|
not modify $s_{p,h-1}$. |
|
|
not modify $s_{p,h-1}$. |
|
|
|
|
|
|
|
|
* Requirement 10 [`ExtendVote`, `FinalizeBlock`, non-dependency]: for any correct process $p$, |
|
|
|
|
|
|
|
|
* Requirement 11 [`ExtendVote`, `FinalizeBlock`, non-dependency]: for any correct process $p$, |
|
|
and any vote extension $e$ that $p$ received at height $h$, the computation of |
|
|
and any vote extension $e$ that $p$ received at height $h$, the computation of |
|
|
$s_{p,h}$ does not depend on $e$. |
|
|
$s_{p,h}$ does not depend on $e$. |
|
|
|
|
|
|
|
@ -127,13 +136,13 @@ Additionally, |
|
|
>**TODO** I have left out all the "events" as they don't have any impact in safety or liveness |
|
|
>**TODO** I have left out all the "events" as they don't have any impact in safety or liveness |
|
|
>(same for consensus params, and validator set) |
|
|
>(same for consensus params, and validator set) |
|
|
|
|
|
|
|
|
* Requirement 11 [`FinalizeBlock`, determinism-1]: For any correct process $p$, |
|
|
|
|
|
|
|
|
* Requirement 12 [`FinalizeBlock`, determinism-1]: For any correct process $p$, |
|
|
$s_{p,h}$ exclusively depends on $s_{p,h-1}$ and $v_{p,h}$. |
|
|
$s_{p,h}$ exclusively depends on $s_{p,h-1}$ and $v_{p,h}$. |
|
|
|
|
|
|
|
|
* Requirement 12 [`FinalizeBlock`, determinism-2]: For any correct process $p$, |
|
|
|
|
|
|
|
|
* Requirement 13 [`FinalizeBlock`, determinism-2]: For any correct process $p$, |
|
|
the contents of $T_{p,h}$ exclusively depend on $s_{p,h-1}$ and $v_{p,h}$. |
|
|
the contents of $T_{p,h}$ exclusively depend on $s_{p,h-1}$ and $v_{p,h}$. |
|
|
|
|
|
|
|
|
Note that Requirements 11 and 12, combined with Agreement property of consensus ensure |
|
|
|
|
|
|
|
|
Note that Requirements 12 and 13, combined with Agreement property of consensus ensure |
|
|
the Application state evolves consistently at all correct processes. |
|
|
the Application state evolves consistently at all correct processes. |
|
|
|
|
|
|
|
|
Finally, notice that neither `PrepareProposal` nor `ExtendVote` have determinism-related |
|
|
Finally, notice that neither `PrepareProposal` nor `ExtendVote` have determinism-related |
|
|