diff --git a/spec/light-client/accountability/MC_n4_f2_amnesia.tla b/spec/light-client/accountability/MC_n4_f2_amnesia.tla index 186bdacee..97dd1375c 100644 --- a/spec/light-client/accountability/MC_n4_f2_amnesia.tla +++ b/spec/light-client/accountability/MC_n4_f2_amnesia.tla @@ -1,5 +1,5 @@ ---------------------- MODULE MC_n4_f2_amnesia ------------------------------- -EXTENDS Sequences +EXTENDS Sequences, typedefs CONSTANT \* @type: $round -> $process; diff --git a/spec/light-client/accountability/README.md b/spec/light-client/accountability/README.md index a6eda7e67..cc6f1aee4 100644 --- a/spec/light-client/accountability/README.md +++ b/spec/light-client/accountability/README.md @@ -306,3 +306,287 @@ Note that detecting this behavior require application knowledge. Detecting this referring to the block before the one in which height happen. **Q:** can we say that in this case a validator declines to check if a proposed value is valid before voting for it? + +## Specification and verification + +### Specification in TLA+ + +We have written a specification of Tendermint consensus, following the +pseudo-code of [BKM19][]. This specification is written for safety of +consensus, e.g., for checking the safety property called [Agreement][], which +says that no two processes can decide differently. As we were interested in +accountability, we have extended the specification as follows: + + - We have added ghost variables that keep track of the evidence collected by + the correct validators: `evidencePropose`, `evidencePrevote`, and + `evidencePrecommit`. Note that these evidence variables are global, so we + do not fix an algorithm for collecting evidence in the specification. + + - We have added the safety property [Accountability][] that requires the + evidence to contain messages from at least `T + 1` validators, when + [Agreement][] is violated. + +The specification is organized in the following files: + + - [TendermintAcc_004_draft.tla][] is the main file that contains the + protocol specification. + + - [typedefs.tla][] contains auxiliary type definitions for [Apalache][]. + + - [TendermintAccInv_004_draft.tla][] contains an inductive invariant + for proving safety of unbounded executions with [Apalache][]. + + - [TendermintAccTrace_004_draft.tla][] contains an auxiliary module + that lets one execute a predefined sequence of actions (without specifying + concrete inputs for every action). + + +### Model checking + +We have checked the safety properties [Agreement][] and [Accountability][] +with the symbolic model checker [Apalache][] v0.27.0. As Apalache works on +bounded data structures, we have introduced several instances of the +specification: + + - [MC_n4_f1.tla][], [MC_n4_f2.tla][], and [MC_n4_f3.tla][] define instances + of four validators, of which one, two, and three validators are faulty, + respectively. + + - [MC_n5_f1.tla][] and [MC_n5_f2.tla][] define instances of five validators, + of which one and two validators are faulty, respectively. + + - [MC_n6_f1.tla][] defines the instance of six validators, of which one is + faulty. + + - [MC_n4_f2_amnesia.tla][] defines the instance of four validators, of which + two are faulty. This model demonstrates an execution, in which the faulty + validators exercise the amnesia attack. + +If you want to reproduce the model checking runs, check the [Installation][] +and [Running Apalache][] pages first. + +#### Evidence of an amnesia attack + +In this run, we fix the trace of actions, in order to quickly violate +`Agreement`. For details, check the [MC_n4_f2_amnesia.tla][] model. +We ran Apalache as follows: + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit \ + --init=TraceInit --next=TraceNext --inv=Agreement MC_n4_f2_amnesia.tla +... +Found 1 error(s) +... +Total time: 10.416 sec +``` + +The trace `violation1.tla` contains a concrete execution of the protocol +that leads to `State7`, in which two validators decide differently +(this is expected behavior for `N=4` and `F=2`): + +```tla +State7 == + ... + /\ decision = SetAsFun({ <<"c1", "v0">>, <<"c2", "v1">> }) + ... + /\ step = SetAsFun({ <<"c1", "DECIDED">>, <<"c2", "DECIDED">> }) + ... +``` + +By inspecting the evidence, we can see that the correct validators have +collected an evidence of the amnesia attack by the two faulty processes: + +```tla +State7 == + ... + /\ evidencePrevote + = { [id |-> "v0", round |-> 2, src |-> "c1", type |-> "PREVOTE"], + [id |-> "v0", round |-> 2, src |-> "f3", type |-> "PREVOTE"], + [id |-> "v0", round |-> 2, src |-> "f4", type |-> "PREVOTE"], + [id |-> "v1", round |-> 0, src |-> "c2", type |-> "PREVOTE"], + [id |-> "v1", round |-> 0, src |-> "f3", type |-> "PREVOTE"], + [id |-> "v1", round |-> 0, src |-> "f4", type |-> "PREVOTE"] } + /\ evidencePrecommit + = { [id |-> "v0", round |-> 2, src |-> "c1", type |-> "PRECOMMIT"], + [id |-> "v0", round |-> 2, src |-> "f3", type |-> "PRECOMMIT"], + [id |-> "v0", round |-> 2, src |-> "f4", type |-> "PRECOMMIT"], + [id |-> "v1", round |-> 0, src |-> "c2", type |-> "PRECOMMIT"], + [id |-> "v1", round |-> 0, src |-> "f3", type |-> "PRECOMMIT"], + [id |-> "v1", round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] } + ... +``` + +#### Violation of Agreement when 2 out of 4 validators are faulty + +To quickly get an example of `Agreement` violation for the case of two out of +four validators being faulty (this is expected behavior), we run symbolic +execution: + +```sh +$ apalache-mc simulate --features=rows --cinit=ConstInit --no-deadlock \ + --inv=Agreement --length=20 MC_n4_f2.tla +... +Found 1 error(s) +... +It took me 0 days 0 hours 3 min 43 sec +``` + +The trace `violation1.tla` contains a concrete execution of the protocol +that leads to `State7`, in which two validators decide differently +(this is expected behavior for `N=4` and `F=2`): + +```tla +State18 == + ... + /\ decision = SetAsFun({ <<"c1", "v1">>, <<"c2", "v0">> }) + ... + /\ step = SetAsFun({ <<"c1", "DECIDED">>, <<"c2", "DECIDED">> }) + ... +``` + +With symbolic execution, the run times may vary significantly, as Apalache +is randomly choosing actions to try. To get an example for sure, we run +bounded model checking: + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit \ + --inv=Agreement MC_n4_f2.tla +... +Found 1 error(s) +... +It took me 0 days 0 hours 56 min 38 sec +``` + +This usually takes longer than simulation execution, as bounded model +checking checks **all** symbolic executions up to the given length, +as opposite to a **fixed number** of symbolic executions. + +#### Agreement holds true when 1 out of 4 validators is faulty + +In case when only one of the four validators is faulty, we expect `Agreement` +to hold true. Before trying to prove it, we can quickly check that it does +hold true for 100 symbolic executions, each having up to 10 steps: + +```sh +$ apalache-mc simulate --features=rows --cinit=ConstInit --inv=Agreement \ + --length=10 MC_n4_f1.tla +... +It took me 0 days 0 hours 2 min 54 sec +``` + +To get a better guarantee that `Agreement` holds true for all executions +that contain up to 10 steps, we run bounded model checking: + + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit \ + --inv=Agreement --length=10 MC_n4_f1.tla +... +Checker reports no error up to computation length 10 +... +It took me 0 days 21 hours 8 min 48 sec +``` + +Finally, to prove that `Agreement` holds true for arbitrarily long executions, +we show that `TypedInv` is an inductive invariant of the specification. For +details, see [Checking inductive invariants][]. + +Proving that `TypedInv` is inductive and using it to show `Agreement` requires +three steps. + +First, we check that the initial states satisfy `TypedInv` (the induction base): + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit --init=TypedInv \ + --inv=Init MC_n4_f1.tla +... +The outcome is: NoError +... +It took me 0 days 0 hours 0 min 8 sec +``` + +Second, we show the inductive step: + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit \ + --init=TypedInv --inv=TypedInv \ + --length=1 MC_n4_f1.tla +... +The outcome is: NoError +... +It took me 0 days 3 hours 46 min 13 sec +``` + +Third, we show that `Agreement` holds in the states, where `TypedInv` holds +true: + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit \ + --init=TypedInv --inv=Agreement --length=0 MC_n4_f1.tla +... +The outcome is: NoError +... +It took me 0 days 0 hours 1 min 0 sec +``` + +Interestingly, this proof is faster (and more complete) than bounded model +checking up to 10 steps. However, it requires an additional predicate +`TypedInv`. + +#### Accountability holds true when 1 out of 4 validators is faulty + +As we have proven that `TypedInv` is inductive in the previous step, we use it +to show that `Accountability` holds for arbitrarily long executions: + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit --init=TypedInv \ + --inv=Accountability --length=0 MC_n4_f1.tla +... +The outcome is: NoError +... +It took me 0 days 0 hours 1 min 2 sec +``` + +#### Accountability holds true when 2 out of 4 validators are faulty + +As we have proven that `TypedInv` is inductive in the previous step, we use it +to show that `Accountability` holds for arbitrarily long executions, +even if the number of faults is over 1/3: + +```sh +$ apalache-mc check --features=rows --cinit=ConstInit --init=TypedInv \ + --inv=Accountability --length=0 MC_n4_f2.tla +... +The outcome is: NoError +... +It took me 0 days 0 hours 1 min 2 sec +``` + +#### Other instances + +The instances [MC_n4_f3.tla][], [MC_n5_f1.tla][], [MC_n5_f2.tla][], +and [MC_n6_f1.tla][] were checked similar to how we did it +for [MC_n4_f1.tla][] and [MC_n4_f2.tla][]. + + + + + +[BKM19]: https://arxiv.org/abs/1807.04938 +[Apalache]: https://github.com/informalsystems/apalache +[TendermintAcc_004_draft.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/TendermintAcc_004_draft.tla +[typedefs.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/typedefs.tla +[TendermintAccInv_004_draft.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/TendermintAccInv_004_draft.tla +[TendermintAccTrace_004_draft.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/TendermintAccTrace_004_draft.tla +[MC_n4_f1.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f1.tla +[MC_n4_f2.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f2.tla +[MC_n4_f2_amnesia.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f2.tla +[MC_n4_f3.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f3.tla +[MC_n5_f1.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n5_f1.tla +[MC_n5_f2.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n5_f2.tla +[MC_n6_f1.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n6_f1.tla +[Installation]: https://apalache.informal.systems/docs/apalache/installation/index.html +[Running Apalache]: https://apalache.informal.systems/docs/apalache/running.html +[Checking inductive invariants]: https://apalache.informal.systems/docs/apalache/running.html#15-checking-an-inductive-invariant +[Accountability]: https://github.com/tendermint/tendermint/blob/c8302c5fcb7f1ffafdefc5014a26047df1d27c99/spec/light-client/accountability/TendermintAcc_004_draft.tla#L545-L550 +[Agreement]: https://github.com/tendermint/tendermint/blob/c8302c5fcb7f1ffafdefc5014a26047df1d27c99/spec/light-client/accountability/TendermintAcc_004_draft.tla#L530-L534 diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla index d9d78be28..5c8092583 100644 --- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla @@ -8,7 +8,7 @@ * Version 3. Modular and parameterized definitions. * Version 2. Bugfixes in the spec and an inductive invariant. - Igor Konnov, 2020. + Igor Konnov, Josef Widder, 2020-2022. *) EXTENDS TendermintAcc_004_draft @@ -159,7 +159,7 @@ AllIfInDecidedThenReceivedTwoThirds == \* for a round r, there is proposal by the round proposer for a valid round vr ProposalInRound(r, proposedVal, vr) == - \E m \in msgsPropose[r]: + \E m \in msgsPropose[r] \intersect evidencePropose: /\ m.src = Proposer[r] /\ m.proposal = proposedVal /\ m.validRound = vr @@ -200,14 +200,14 @@ IfSentPrecommitThenReceivedTwoThirds == \A r \in Rounds: \A mpc \in msgsPrecommit[r]: mpc.src \in Corr => - \/ /\ mpc.id \in ValidValues - /\ LET PV == { - m \in msgsPrevote[r] \intersect evidencePrevote: m.id = mpc.id - } - IN - Cardinality(PV) >= THRESHOLD2 - \/ /\ mpc.id = NilValue - /\ Cardinality(msgsPrevote[r]) >= THRESHOLD2 + \/ /\ mpc.id \in ValidValues + /\ LET PV == { + m \in msgsPrevote[r] \intersect evidencePrevote: m.id = mpc.id + } + IN + Cardinality(PV) >= THRESHOLD2 + \/ /\ mpc.id = NilValue + /\ Cardinality(msgsPrevote[r] \intersect evidencePrevote) >= THRESHOLD2 \* if a correct process has sent a precommit message in a round, it should \* have sent a prevote @@ -239,15 +239,17 @@ AllIfLockedRoundThenSentCommit == \* a process always locks the latest round, for which it has sent a PRECOMMIT LatestPrecommitHasLockedRound(p) == - LET pPrecommits == - {mm \in UNION { msgsPrecommit[r]: r \in Rounds }: mm.src = p /\ mm.id /= NilValue } + LET pPrecommits == { + mm \in UNION { msgsPrecommit[r]: r \in Rounds }: + mm.src = p /\ mm.id /= NilValue + } IN pPrecommits /= {} => LET latest == CHOOSE m \in pPrecommits: \A m2 \in pPrecommits: m2.round <= m.round - IN + IN /\ lockedRound[p] = latest.round /\ lockedValue[p] = latest.id @@ -316,15 +318,41 @@ RelockValueIfEnoughPrevotes == IN LET EnoughPrevotesInMiddle == \E mr \in Rounds: - /\ r1 < mr /\ mr <= r2 - \* count prevotes in the middle round, excluding p if mr = r2 - /\ LET Prevotes == { m \in msgsPrevote[mr]: - m.id = v2 /\ (m.src /= p \/ mr < r2) } + /\ r1 <= mr /\ mr <= r2 + \* count prevotes in the middle round, excluding p + /\ LET Prevotes == { + m \in msgsPrevote[mr] \intersect evidencePrevote: + m.id = v2 /\ (m.src /= p \/ mr < r2) + } IN Cardinality(Prevotes) >= THRESHOLD2 IN RelockedValue => EnoughPrevotesInMiddle +\* if validRound is defined, then there are two-thirds of PREVOTEs +AllIfValidRoundThenTwoThirds == + \A p \in Corr: + LET vr == validRound[p] IN + \/ vr = NilRound /\ validValue[p] = NilValue + \/ LET PV == { + m \in msgsPrevote[vr] \intersect evidencePrevote: + m.id = validValue[p] + } IN + Cardinality(PV) >= THRESHOLD2 + +AllValidAndLocked == + \A p \in Corr: + /\ validRound[p] >= lockedRound[p] + /\ validRound[p] /= NilRound <=> validValue[p] /= NilValue + /\ lockedValue[p] /= NilValue => validValue[p] /= NilValue + +\* a valid round can be only set to a valid value that was proposed earlier +AllIfValidRoundThenProposal == + \A p \in Corr: + \/ validRound[p] = NilRound + \/ \E m \in msgsPropose[validRound[p]] \intersect evidencePropose: + m.proposal = validValue[p] + \* a combination of all lemmas Inv == /\ EvidenceContainsMessages @@ -343,42 +371,13 @@ Inv == /\ AllNoEquivocationByCorrect /\ PrecommitsLockValue /\ RelockValueIfEnoughPrevotes + /\ AllIfValidRoundThenTwoThirds + /\ AllValidAndLocked + /\ AllIfValidRoundThenProposal \* this is the inductive invariant we like to check TypedInv == TypeOK /\ Inv -\* UNUSED FOR SAFETY -ValidRoundNotSmallerThanLockedRound(p) == - validRound[p] >= lockedRound[p] - -\* UNUSED FOR SAFETY -ValidRoundIffValidValue(p) == - (validRound[p] = NilRound) <=> (validValue[p] = NilValue) - -\* UNUSED FOR SAFETY -AllValidRoundIffValidValue == - \A p \in Corr: ValidRoundIffValidValue(p) - -\* if validRound is defined, then there are two-thirds of PREVOTEs -IfValidRoundThenTwoThirds(p) == - \/ validRound[p] = NilRound - \/ LET PV == { m \in msgsPrevote[validRound[p]]: m.id = validValue[p] } IN - Cardinality(PV) >= THRESHOLD2 - -\* UNUSED FOR SAFETY -AllIfValidRoundThenTwoThirds == - \A p \in Corr: IfValidRoundThenTwoThirds(p) - -\* a valid round can be only set to a valid value that was proposed earlier -IfValidRoundThenProposal(p) == - \/ validRound[p] = NilRound - \/ \E m \in msgsPropose[validRound[p]]: - m.proposal = validValue[p] - -\* UNUSED FOR SAFETY -AllIfValidRoundThenProposal == - \A p \in Corr: IfValidRoundThenProposal(p) - (******************************** THEOREMS ************************************) (* Under this condition, the faulty processes can decide alone *) FaultyQuorum == Cardinality(Faulty) >= THRESHOLD2 diff --git a/spec/light-client/accountability/TendermintAccTrace_004_draft.tla b/spec/light-client/accountability/TendermintAccTrace_004_draft.tla index decd6b733..b901c1c31 100644 --- a/spec/light-client/accountability/TendermintAccTrace_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccTrace_004_draft.tla @@ -23,7 +23,7 @@ VARIABLE TraceInit == /\ toReplay = Trace - /\ action' := "Init" + /\ action = "Init" /\ Init TraceNext == @@ -31,7 +31,7 @@ TraceNext == /\ toReplay' = Tail(toReplay) \* Here is the trick. We restrict the action to the expected one, \* so the other actions will be pruned - /\ action' := Head(toReplay) + /\ action' = Head(toReplay) /\ Next ================================================================================ diff --git a/spec/light-client/accountability/TendermintAcc_004_draft.tla b/spec/light-client/accountability/TendermintAcc_004_draft.tla index 0749e1b49..e9f3c03df 100644 --- a/spec/light-client/accountability/TendermintAcc_004_draft.tla +++ b/spec/light-client/accountability/TendermintAcc_004_draft.tla @@ -494,7 +494,6 @@ EquivocationBy(p) == /\ m1.src = p /\ m2.src = p /\ m1.round = m2.round - /\ m1.type = m2.type IN \/ EquivocationIn(evidencePropose) \/ EquivocationIn(evidencePrevote) @@ -519,8 +518,12 @@ AmnesiaBy(p) == id |-> Id(v2) ] \in evidencePrevote /\ \A r \in { rnd \in Rounds: r1 <= rnd /\ rnd < r2 }: - LET prevotes == - { m \in evidencePrevote: m.round = r /\ m.id = Id(v2) } + LET prevotes == { + m \in evidencePrevote: + /\ m.round = r + /\ m.id = Id(v2) + /\ m.src /= p + } IN Cardinality(prevotes) < THRESHOLD2 diff --git a/spec/light-client/accountability/typedefs.tla b/spec/light-client/accountability/typedefs.tla index ce232f9e9..c9018dc87 100644 --- a/spec/light-client/accountability/typedefs.tla +++ b/spec/light-client/accountability/typedefs.tla @@ -1,11 +1,18 @@ -------------------- MODULE typedefs --------------------------- (* + // the process type @typeAlias: process = Str; + // the value type @typeAlias: value = Str; + // the type of step labels @typeAlias: step = Str; + // the type of round numbers @typeAlias: round = Int; + // the type of action labels @typeAlias: action = Str; + // the type of action traces @typeAlias: trace = Seq(Str); + // the type of PROPOSE messages @typeAlias: proposeMsg = { type: $step, @@ -14,6 +21,7 @@ proposal: $value, validRound: $round }; + // the type of PRECOMMIT messages @typeAlias: preMsg = { type: $step,