The TLA+ specification of the attackers detection (#231)

* the working attackers isolation spec, needs more comments

* the TLA+ spec of the attackers isolation

rust-spec/lightclient/attacks/Blockchain_003_draft.tla

@@ -0,0 +1,166 @@
+------------------------ MODULE Blockchain_003_draft -----------------------------
+(*
+  This is a high-level specification of Tendermint blockchain
+  that is designed specifically for the light client.
+  Validators have the voting power of one. If you like to model various
+  voting powers, introduce multiple copies of the same validator
+  (do not forget to give them unique names though).
+ *)
+EXTENDS Integers, FiniteSets, Apalache
+
+Min(a, b) == IF a < b THEN a ELSE b
+
+CONSTANT
+  AllNodes,
+    (* a set of all nodes that can act as validators (correct and faulty) *)
+  ULTIMATE_HEIGHT,
+    (* a maximal height that can be ever reached (modelling artifact) *)
+  TRUSTING_PERIOD
+    (* the period within which the validators are trusted *)
+
+Heights == 1..ULTIMATE_HEIGHT   (* possible heights *)
+
+(* A commit is just a set of nodes who have committed the block *)
+Commits == SUBSET AllNodes
+
+(* The set of all block headers that can be on the blockchain.
+   This is a simplified version of the Block data structure in the actual implementation. *)
+BlockHeaders == [
+  height: Heights,
+    \* the block height
+  time: Int,
+    \* the block timestamp in some integer units
+  lastCommit: Commits,
+    \* the nodes who have voted on the previous block, the set itself instead of a hash
+  (* in the implementation, only the hashes of V and NextV are stored in a block,
+     as V and NextV are stored in the application state *) 
+  VS: SUBSET AllNodes,
+    \* the validators of this bloc. We store the validators instead of the hash.
+  NextVS: SUBSET AllNodes
+    \* the validators of the next block. We store the next validators instead of the hash.
+]
+
+(* A signed header is just a header together with a set of commits *)
+LightBlocks == [header: BlockHeaders, Commits: Commits]
+
+VARIABLES
+    refClock,
+        (* the current global time in integer units as perceived by the reference chain *)
+    blockchain,
+    (* A sequence of BlockHeaders, which gives us a bird view of the blockchain. *)
+    Faulty
+    (* A set of faulty nodes, which can act as validators. We assume that the set
+       of faulty processes is non-decreasing. If a process has recovered, it should
+       connect using a different id. *)
+       
+(* all variables, to be used with UNCHANGED *)       
+vars == <<refClock, blockchain, Faulty>>         
+
+(* The set of all correct nodes in a state *)
+Corr == AllNodes \ Faulty
+
+(* APALACHE annotations *)
+a <: b == a \* type annotation
+
+NT == STRING
+NodeSet(S) == S <: {NT}
+EmptyNodeSet == NodeSet({})
+
+BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}]
+
+LBT == [header |-> BT, Commits |-> {NT}]
+(* end of APALACHE annotations *)       
+
+(****************************** BLOCKCHAIN ************************************)
+
+(* the header is still within the trusting period *)
+InTrustingPeriod(header) ==
+    refClock < header.time + TRUSTING_PERIOD
+
+(*
+ Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes
+ and pNodes \subseteq D, test whether the set pNodes \subseteq AllNodes has
+ more than 2/3 of voting power among the nodes in D.
+ *)
+TwoThirds(pVS, pNodes) ==
+    LET TP == Cardinality(pVS)
+        SP == Cardinality(pVS \intersect pNodes)
+    IN
+    3 * SP > 2 * TP \* when thinking in real numbers, not integers: SP > 2.0 / 3.0 * TP 
+
+(*
+ Given a set of FaultyNodes, test whether the voting power of the correct nodes in D
+ is more than 2/3 of the voting power of the faulty nodes in D.
+
+ Parameters:
+   - pFaultyNodes is a set of nodes that are considered faulty
+   - pVS is a set of all validators, maybe including Faulty, intersecting with it, etc.
+   - pMaxFaultRatio is a pair <<a, b>> that limits the ratio a / b of the faulty
+     validators from above (exclusive)
+ *)
+FaultyValidatorsFewerThan(pFaultyNodes, pVS, maxRatio) ==
+    LET FN == pFaultyNodes \intersect pVS   \* faulty nodes in pNodes
+        CN == pVS \ pFaultyNodes            \* correct nodes in pNodes
+        CP == Cardinality(CN)               \* power of the correct nodes
+        FP == Cardinality(FN)               \* power of the faulty nodes
+    IN
+    \* CP + FP = TP is the total voting power
+    LET TP == CP + FP IN
+    FP * maxRatio[2] < TP * maxRatio[1]
+
+(* Can a block be produced by a correct peer, or an authenticated Byzantine peer *)
+IsLightBlockAllowedByDigitalSignatures(ht, block) == 
+    \/ block.header = blockchain[ht] \* signed by correct and faulty (maybe)
+    \/ /\ block.Commits \subseteq Faulty
+       /\ block.header.height = ht
+       /\ block.header.time >= 0 \* signed only by faulty
+
+(*
+ Initialize the blockchain to the ultimate height right in the initial states.
+ We pick the faulty validators statically, but that should not affect the light client.
+
+ Parameters:
+    - pMaxFaultyRatioExclusive is a pair <<a, b>> that bound the number of
+        faulty validators in each block by the ratio a / b (exclusive)
+ *)            
+InitToHeight(pMaxFaultyRatioExclusive) ==
+  /\ \E Nodes \in SUBSET AllNodes:
+      Faulty := Nodes   \* pick a subset of nodes to be faulty
+  \* pick the validator sets and last commits
+  /\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]:
+     \E timestamp \in [Heights -> Int]:
+        \* refClock is at least as early as the timestamp in the last block 
+        /\ \E tm \in Int:
+          refClock := tm /\ tm >= timestamp[ULTIMATE_HEIGHT]
+        \* the genesis starts on day 1     
+        /\ timestamp[1] = 1
+        /\ vs[1] = AllNodes
+        /\ lastCommit[1] = EmptyNodeSet
+        /\ \A h \in Heights \ {1}:
+          /\ lastCommit[h] \subseteq vs[h - 1]   \* the non-validators cannot commit 
+          /\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes
+            \* the faulty validators have the power below the threshold
+          /\ FaultyValidatorsFewerThan(Faulty, vs[h], pMaxFaultyRatioExclusive)
+          /\ timestamp[h] > timestamp[h - 1]     \* the time grows monotonically
+          /\ timestamp[h] < timestamp[h - 1] + TRUSTING_PERIOD    \* but not too fast
+        \* form the block chain out of validator sets and commits (this makes apalache faster)
+        /\ blockchain := [h \in Heights |->
+             [height |-> h,
+              time |-> timestamp[h],
+              VS |-> vs[h],
+              NextVS |-> IF h < ULTIMATE_HEIGHT THEN vs[h + 1] ELSE AllNodes,
+              lastCommit |-> lastCommit[h]]
+             ] \******
+       
+(********************* BLOCKCHAIN ACTIONS ********************************)
+(*
+  Advance the clock by zero or more time units.
+  *)
+AdvanceTime ==
+  /\ \E tm \in Int: tm >= refClock /\ refClock' = tm
+  /\ UNCHANGED <<blockchain, Faulty>>
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Jun 10 14:10:54 CEST 2020 by igor
+\* Created Fri Oct 11 15:45:11 CEST 2019 by igor

rust-spec/lightclient/attacks/Isolation_001_draft.tla

@@ -0,0 +1,159 @@
+----------------------- MODULE Isolation_001_draft ----------------------------
+(**
+ * The specification of the attackers isolation at full node,
+ * when it has received an evidence from the light client.
+ * We check that the isolation spec produces a set of validators
+ * that have more than 1/3 of the voting power.
+ *
+ * It follows the English specification:
+ *
+ * https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
+ *
+ * The assumptions made in this specification:
+ *
+ *  - the voting power of every validator is 1
+ *     (add more validators, if you need more validators)
+ *
+ *  - Tendermint security model is violated
+ *    (there are Byzantine validators who signed a conflicting block)
+ *
+ * Igor Konnov, Zarko Milosevic, Josef Widder, Informal Systems, 2020
+ *)
+
+
+EXTENDS Integers, FiniteSets, Apalache
+
+\* algorithm parameters
+CONSTANTS
+  AllNodes,
+    (* a set of all nodes that can act as validators (correct and faulty) *)
+  COMMON_HEIGHT,
+    (* an index of the block header that two peers agree upon *)
+  CONFLICT_HEIGHT,
+    (* an index of the block header that two peers disagree upon *)
+  TRUSTING_PERIOD,
+    (* the period within which the validators are trusted *)
+  FAULTY_RATIO
+    (* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
+       from above (exclusive). Tendermint security model prescribes 1 / 3. *)
+
+VARIABLES  
+  blockchain,           (* the chain at the full node *)
+  refClock,             (* the reference clock at the full node *)
+  Faulty,               (* the set of faulty validators *)
+  conflictingBlock,     (* an evidence that two peers reported conflicting blocks *)
+  state,                (* the state of the attack isolation machine at the full node *)
+  attackers             (* the set of the identified attackers *)
+
+vars == <<blockchain, refClock, Faulty, conflictingBlock, state>>  
+ 
+\* instantiate the chain at the full node
+ULTIMATE_HEIGHT == CONFLICT_HEIGHT + 1 
+BC == INSTANCE Blockchain_003_draft
+
+\* use the light client API
+TRUSTING_HEIGHT == COMMON_HEIGHT
+TARGET_HEIGHT == CONFLICT_HEIGHT
+
+LC == INSTANCE LCVerificationApi_003_draft
+    WITH localClock <- refClock, REAL_CLOCK_DRIFT <- 0, CLOCK_DRIFT <- 0
+
+\* old-style type annotations in apalache
+a <: b == a
+
+\* [LCAI-NONVALID-OUTPUT.1::TLA.1]
+ViolatesValidity(header1, header2) ==
+    \/ header1.VS /= header2.VS
+    \/ header1.NextVS /= header2.NextVS
+    \/ header1.height /= header2.height
+    \/ header1.time /= header2.time
+    (* The English specification also checks the fields that we do not have
+       at this level of abstraction:
+       - header1.ConsensusHash != header2.ConsensusHash or
+       - header1.AppHash != header2.AppHash or
+       - header1.LastResultsHash header2 != ev.LastResultsHash
+    *)
+
+Init ==
+    /\ state := "init"
+    \* Pick an arbitrary blockchain from 1 to COMMON_HEIGHT + 1.
+    /\ BC!InitToHeight(FAULTY_RATIO) \* initializes blockchain, Faulty, and refClock
+    /\ attackers := {} <: {STRING}      \* attackers are unknown
+    \* Receive an arbitrary evidence.
+    \* Instantiate the light block fields one by one,
+    \* to avoid combinatorial explosion of records.
+    /\ \E time \in Int:
+        \E VS, NextVS, lastCommit, Commits \in SUBSET AllNodes:
+          LET conflicting ==
+             [ Commits |-> Commits,
+               header |->
+                 [height |-> CONFLICT_HEIGHT,
+                  time |-> time,
+                  VS |-> VS,
+                  NextVS |-> NextVS,
+                  lastCommit |-> lastCommit] ]
+          IN  
+          LET refBlock == [ header |-> blockchain[COMMON_HEIGHT],
+                           Commits |-> blockchain[COMMON_HEIGHT + 1].lastCommit ]
+          IN
+          /\ "SUCCESS" = LC!ValidAndVerifiedUntimed(refBlock, conflicting)
+          \* More than third of next validators in the common reference block
+          \* is faulty. That is a precondition for a fork.
+          /\ 3 * Cardinality(Faulty \intersect refBlock.header.NextVS)
+                > Cardinality(refBlock.header.NextVS)
+          \* correct validators cannot sign an invalid block
+          /\ ViolatesValidity(conflicting.header, refBlock.header)
+              => conflicting.Commits \subseteq Faulty
+          /\ conflictingBlock := conflicting
+
+    
+\* This is a specification of isolateMisbehavingProcesses.
+\*
+\* [LCAI-FUNC-MAIN.1::TLA.1]
+Next ==
+    /\ state = "init"
+    \* Extract the rounds from the reference block and the conflicting block.
+    \* In this specification, we just pick rounds non-deterministically.
+    \* The English specification calls RoundOf on the blocks.
+    /\ \E referenceRound, evidenceRound \in Int:
+      /\ referenceRound >= 0 /\ evidenceRound >= 0
+      /\ LET reference == blockchain[CONFLICT_HEIGHT]
+            referenceCommit == blockchain[CONFLICT_HEIGHT + 1].lastCommit
+            evidenceHeader == conflictingBlock.header
+            evidenceCommit == conflictingBlock.Commits
+        IN
+        IF ViolatesValidity(reference, evidenceHeader)
+        THEN /\ attackers' := blockchain[COMMON_HEIGHT].NextVS \intersect evidenceCommit
+             /\ state' := "Lunatic"
+        ELSE IF referenceRound = evidenceRound
+        THEN /\ attackers' := referenceCommit \intersect evidenceCommit
+             /\ state' := "Equivocation"
+        ELSE
+          \* This property is shown in property
+          \* Accountability of TendermintAcc3.tla
+          /\ state' := "Amnesia"
+          /\ \E Attackers \in SUBSET (Faulty \intersect reference.VS):
+             /\ 3 * Cardinality(Attackers) > Cardinality(reference.VS)
+             /\ attackers' := Attackers
+    /\ blockchain' := blockchain
+    /\ refClock' := refClock
+    /\ Faulty' := Faulty
+    /\ conflictingBlock' := conflictingBlock
+
+(********************************** INVARIANTS *******************************)
+
+\* This invariant ensure that the attackers have
+\* more than 1/3 of the voting power
+\*
+\* [LCAI-INV-Output.1::TLA-DETECTION-COMPLETENESS.1]
+DetectionCompleteness ==
+  state /= "init" =>
+    3 * Cardinality(attackers) > Cardinality(blockchain[CONFLICT_HEIGHT].VS)
+
+\* This invariant ensures that only the faulty validators are detected
+\*
+\* [LCAI-INV-Output.1::TLA-DETECTION-ACCURACY.1]
+DetectionAccuracy ==
+  attackers \subseteq Faulty
+
+==============================================================================

rust-spec/lightclient/attacks/LCVerificationApi_003_draft.tla

@@ -0,0 +1,192 @@
+-------------------- MODULE LCVerificationApi_003_draft --------------------------
+(**
+ * The common interface of the light client verification and detection.
+ *) 
+EXTENDS Integers, FiniteSets
+
+\* the parameters of Light Client
+CONSTANTS
+  TRUSTING_PERIOD,
+    (* the period within which the validators are trusted *)
+  CLOCK_DRIFT,
+    (* the assumed precision of the clock *)
+  REAL_CLOCK_DRIFT,
+    (* the actual clock drift, which under normal circumstances should not
+       be larger than CLOCK_DRIFT (otherwise, there will be a bug) *)
+  FAULTY_RATIO
+    (* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
+       from above (exclusive). Tendermint security model prescribes 1 / 3. *)
+
+VARIABLES  
+  localClock (* current time as measured by the light client *)
+
+(* the header is still within the trusting period *)
+InTrustingPeriodLocal(header) ==
+    \* note that the assumption about the drift reduces the period of trust
+    localClock < header.time + TRUSTING_PERIOD - CLOCK_DRIFT
+
+(* the header is still within the trusting period, even if the clock can go backwards *)
+InTrustingPeriodLocalSurely(header) ==
+    \* note that the assumption about the drift reduces the period of trust
+    localClock < header.time + TRUSTING_PERIOD - 2 * CLOCK_DRIFT
+
+(* ensure that the local clock does not drift far away from the global clock *)
+IsLocalClockWithinDrift(local, global) ==
+    /\ global - REAL_CLOCK_DRIFT <= local
+    /\ local <= global + REAL_CLOCK_DRIFT
+
+(**
+  * Check that the commits in an untrusted block form 1/3 of the next validators
+  * in a trusted header.
+ *)
+SignedByOneThirdOfTrusted(trusted, untrusted) ==
+  LET TP == Cardinality(trusted.header.NextVS)
+      SP == Cardinality(untrusted.Commits \intersect trusted.header.NextVS)
+  IN
+  3 * SP > TP     
+
+(**
+ The first part of the precondition of ValidAndVerified, which does not take
+ the current time into account.
+ 
+ [LCV-FUNC-VALID.1::TLA-PRE-UNTIMED.1]
+ *)
+ValidAndVerifiedPreUntimed(trusted, untrusted) ==
+  LET thdr == trusted.header
+      uhdr == untrusted.header
+  IN
+  /\ thdr.height < uhdr.height
+     \* the trusted block has been created earlier
+  /\ thdr.time < uhdr.time
+  /\ untrusted.Commits \subseteq uhdr.VS
+  /\ LET TP == Cardinality(uhdr.VS)
+         SP == Cardinality(untrusted.Commits)
+     IN
+     3 * SP > 2 * TP     
+  /\ thdr.height + 1 = uhdr.height => thdr.NextVS = uhdr.VS
+  (* As we do not have explicit hashes we ignore these three checks of the English spec:
+   
+     1. "trusted.Commit is a commit is for the header trusted.Header,
+      i.e. it contains the correct hash of the header".
+     2. untrusted.Validators = hash(untrusted.Header.Validators)
+     3. untrusted.NextValidators = hash(untrusted.Header.NextValidators)
+   *)
+
+(**
+ Check the precondition of ValidAndVerified, including the time checks.
+ 
+ [LCV-FUNC-VALID.1::TLA-PRE.1]
+ *)
+ValidAndVerifiedPre(trusted, untrusted, checkFuture) ==
+  LET thdr == trusted.header
+      uhdr == untrusted.header
+  IN
+  /\ InTrustingPeriodLocal(thdr)
+     \* The untrusted block is not from the future (modulo clock drift).
+     \* Do the check, if it is required.
+  /\ checkFuture => uhdr.time < localClock + CLOCK_DRIFT
+  /\ ValidAndVerifiedPreUntimed(trusted, untrusted)
+
+
+(**
+ Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header.
+ This test does take current time into account, but only looks at the block structure.
+ 
+ [LCV-FUNC-VALID.1::TLA-UNTIMED.1]
+ *)   
+ValidAndVerifiedUntimed(trusted, untrusted) ==
+    IF ~ValidAndVerifiedPreUntimed(trusted, untrusted)
+    THEN "INVALID"
+    ELSE IF untrusted.header.height = trusted.header.height + 1
+             \/ SignedByOneThirdOfTrusted(trusted, untrusted)
+         THEN "SUCCESS"
+         ELSE "NOT_ENOUGH_TRUST"
+
+(**
+ Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header.
+ 
+ [LCV-FUNC-VALID.1::TLA.1]
+ *)   
+ValidAndVerified(trusted, untrusted, checkFuture) ==
+    IF ~ValidAndVerifiedPre(trusted, untrusted, checkFuture)
+    THEN "INVALID"
+    ELSE IF ~InTrustingPeriodLocal(untrusted.header)
+    (* We leave the following test for the documentation purposes.
+       The implementation should do this test, as signature verification may be slow.
+       In the TLA+ specification, ValidAndVerified happens in no time.
+     *) 
+    THEN "FAILED_TRUSTING_PERIOD" 
+    ELSE IF untrusted.header.height = trusted.header.height + 1
+             \/ SignedByOneThirdOfTrusted(trusted, untrusted)
+         THEN "SUCCESS"
+         ELSE "NOT_ENOUGH_TRUST"
+
+
+(**
+  The invariant of the light store that is not related to the blockchain
+ *)
+LightStoreInv(fetchedLightBlocks, lightBlockStatus) ==
+    \A lh, rh \in DOMAIN fetchedLightBlocks:
+            \* for every pair of stored headers that have been verified
+        \/ lh >= rh
+        \/ lightBlockStatus[lh] /= "StateVerified"
+        \/ lightBlockStatus[rh] /= "StateVerified"
+           \* either there is a header between them
+        \/ \E mh \in DOMAIN fetchedLightBlocks:
+            lh < mh /\ mh < rh /\ lightBlockStatus[mh] = "StateVerified"
+           \* or the left header is outside the trusting period, so no guarantees
+        \/ LET lhdr == fetchedLightBlocks[lh]
+               rhdr == fetchedLightBlocks[rh]
+           IN
+           \* we can verify the right one using the left one
+           "SUCCESS" = ValidAndVerifiedUntimed(lhdr, rhdr)
+
+(**
+  Correctness states that all the obtained headers are exactly like in the blockchain.
+ 
+  It is always the case that every verified header in LightStore was generated by
+  an instance of Tendermint consensus.
+  
+  [LCV-DIST-SAFE.1::CORRECTNESS-INV.1]
+ *)  
+CorrectnessInv(blockchain, fetchedLightBlocks, lightBlockStatus) ==
+    \A h \in DOMAIN fetchedLightBlocks:
+        lightBlockStatus[h] = "StateVerified" =>
+            fetchedLightBlocks[h].header = blockchain[h]
+
+(**
+ * When the light client terminates, there are no failed blocks.
+ * (Otherwise, someone lied to us.) 
+ *)            
+NoFailedBlocksOnSuccessInv(fetchedLightBlocks, lightBlockStatus) ==
+     \A h \in DOMAIN fetchedLightBlocks:
+        lightBlockStatus[h] /= "StateFailed"            
+
+(**
+ The expected post-condition of VerifyToTarget.
+ *)
+VerifyToTargetPost(blockchain, isPeerCorrect,
+                   fetchedLightBlocks, lightBlockStatus,
+                   trustedHeight, targetHeight, finalState) ==
+  LET trustedHeader == fetchedLightBlocks[trustedHeight].header IN
+    \* The light client is not lying us on the trusted block.
+    \* It is straightforward to detect.
+    /\ lightBlockStatus[trustedHeight] = "StateVerified"
+    /\ trustedHeight \in DOMAIN fetchedLightBlocks
+    /\ trustedHeader = blockchain[trustedHeight]
+    \* the invariants we have found in the light client verification
+    \* there is a problem with trusting period
+    /\ isPeerCorrect
+        => CorrectnessInv(blockchain, fetchedLightBlocks, lightBlockStatus)
+    \* a correct peer should fail the light client,
+    \* if the trusted block is in the trusting period
+    /\ isPeerCorrect /\ InTrustingPeriodLocalSurely(trustedHeader)
+        => finalState = "finishedSuccess"
+    /\ finalState = "finishedSuccess" =>
+        /\ lightBlockStatus[targetHeight] = "StateVerified"
+        /\ targetHeight \in DOMAIN fetchedLightBlocks
+        /\ NoFailedBlocksOnSuccessInv(fetchedLightBlocks, lightBlockStatus)
+    /\ LightStoreInv(fetchedLightBlocks, lightBlockStatus)
+
+
+==================================================================================

rust-spec/lightclient/attacks/MC_5_3.tla

@@ -0,0 +1,18 @@
+------------------------- MODULE MC_5_3 -------------------------------------
+
+AllNodes == {"n1", "n2", "n3", "n4", "n5"}
+COMMON_HEIGHT == 1
+CONFLICT_HEIGHT == 3
+TRUSTING_PERIOD == 1400     \* two weeks, one day is 100 time units :-)
+FAULTY_RATIO == <<1, 2>>    \* < 1 / 2 faulty validators
+
+VARIABLES
+  blockchain,           \* the reference blockchain
+  refClock,             \* current time in the reference blockchain
+  Faulty,               \* the set of faulty validators
+  state,                \* the state of the light client detector
+  conflictingBlock,     \* an evidence that two peers reported conflicting blocks
+  attackers
+
+INSTANCE Isolation_001_draft
+============================================================================