You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

171 lines
6.9 KiB

  1. ------------------------ MODULE Blockchain_002_draft -----------------------------
  2. (*
  3. This is a high-level specification of Tendermint blockchain
  4. that is designed specifically for the light client.
  5. Validators have the voting power of one. If you like to model various
  6. voting powers, introduce multiple copies of the same validator
  7. (do not forget to give them unique names though).
  8. *)
  9. EXTENDS Integers, FiniteSets
  10. Min(a, b) == IF a < b THEN a ELSE b
  11. CONSTANT
  12. AllNodes,
  13. (* a set of all nodes that can act as validators (correct and faulty) *)
  14. ULTIMATE_HEIGHT,
  15. (* a maximal height that can be ever reached (modelling artifact) *)
  16. TRUSTING_PERIOD
  17. (* the period within which the validators are trusted *)
  18. Heights == 1..ULTIMATE_HEIGHT (* possible heights *)
  19. (* A commit is just a set of nodes who have committed the block *)
  20. Commits == SUBSET AllNodes
  21. (* The set of all block headers that can be on the blockchain.
  22. This is a simplified version of the Block data structure in the actual implementation. *)
  23. BlockHeaders == [
  24. height: Heights,
  25. \* the block height
  26. time: Int,
  27. \* the block timestamp in some integer units
  28. lastCommit: Commits,
  29. \* the nodes who have voted on the previous block, the set itself instead of a hash
  30. (* in the implementation, only the hashes of V and NextV are stored in a block,
  31. as V and NextV are stored in the application state *)
  32. VS: SUBSET AllNodes,
  33. \* the validators of this bloc. We store the validators instead of the hash.
  34. NextVS: SUBSET AllNodes
  35. \* the validators of the next block. We store the next validators instead of the hash.
  36. ]
  37. (* A signed header is just a header together with a set of commits *)
  38. LightBlocks == [header: BlockHeaders, Commits: Commits]
  39. VARIABLES
  40. now,
  41. (* the current global time in integer units *)
  42. blockchain,
  43. (* A sequence of BlockHeaders, which gives us a bird view of the blockchain. *)
  44. Faulty
  45. (* A set of faulty nodes, which can act as validators. We assume that the set
  46. of faulty processes is non-decreasing. If a process has recovered, it should
  47. connect using a different id. *)
  48. (* all variables, to be used with UNCHANGED *)
  49. vars == <<now, blockchain, Faulty>>
  50. (* The set of all correct nodes in a state *)
  51. Corr == AllNodes \ Faulty
  52. (* APALACHE annotations *)
  53. a <: b == a \* type annotation
  54. NT == STRING
  55. NodeSet(S) == S <: {NT}
  56. EmptyNodeSet == NodeSet({})
  57. BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}]
  58. LBT == [header |-> BT, Commits |-> {NT}]
  59. (* end of APALACHE annotations *)
  60. (****************************** BLOCKCHAIN ************************************)
  61. (* the header is still within the trusting period *)
  62. InTrustingPeriod(header) ==
  63. now < header.time + TRUSTING_PERIOD
  64. (*
  65. Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes
  66. and pNodes \subseteq D, test whether the set pNodes \subseteq AllNodes has
  67. more than 2/3 of voting power among the nodes in D.
  68. *)
  69. TwoThirds(pVS, pNodes) ==
  70. LET TP == Cardinality(pVS)
  71. SP == Cardinality(pVS \intersect pNodes)
  72. IN
  73. 3 * SP > 2 * TP \* when thinking in real numbers, not integers: SP > 2.0 / 3.0 * TP
  74. (*
  75. Given a set of FaultyNodes, test whether the voting power of the correct nodes in D
  76. is more than 2/3 of the voting power of the faulty nodes in D.
  77. *)
  78. IsCorrectPower(pFaultyNodes, pVS) ==
  79. LET FN == pFaultyNodes \intersect pVS \* faulty nodes in pNodes
  80. CN == pVS \ pFaultyNodes \* correct nodes in pNodes
  81. CP == Cardinality(CN) \* power of the correct nodes
  82. FP == Cardinality(FN) \* power of the faulty nodes
  83. IN
  84. \* CP + FP = TP is the total voting power, so we write CP > 2.0 / 3 * TP as follows:
  85. CP > 2 * FP \* Note: when FP = 0, this implies CP > 0.
  86. (* This is what we believe is the assumption about failures in Tendermint *)
  87. FaultAssumption(pFaultyNodes, pNow, pBlockchain) ==
  88. \A h \in Heights:
  89. pBlockchain[h].time + TRUSTING_PERIOD > pNow =>
  90. IsCorrectPower(pFaultyNodes, pBlockchain[h].NextVS)
  91. (* Can a block be produced by a correct peer, or an authenticated Byzantine peer *)
  92. IsLightBlockAllowedByDigitalSignatures(ht, block) ==
  93. \/ block.header = blockchain[ht] \* signed by correct and faulty (maybe)
  94. \/ block.Commits \subseteq Faulty /\ block.header.height = ht /\ block.header.time >= 0 \* signed only by faulty
  95. (*
  96. Initialize the blockchain to the ultimate height right in the initial states.
  97. We pick the faulty validators statically, but that should not affect the light client.
  98. *)
  99. InitToHeight ==
  100. /\ Faulty \in SUBSET AllNodes \* some nodes may fail
  101. \* pick the validator sets and last commits
  102. /\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]:
  103. \E timestamp \in [Heights -> Int]:
  104. \* now is at least as early as the timestamp in the last block
  105. /\ \E tm \in Int: now = tm /\ tm >= timestamp[ULTIMATE_HEIGHT]
  106. \* the genesis starts on day 1
  107. /\ timestamp[1] = 1
  108. /\ vs[1] = AllNodes
  109. /\ lastCommit[1] = EmptyNodeSet
  110. /\ \A h \in Heights \ {1}:
  111. /\ lastCommit[h] \subseteq vs[h - 1] \* the non-validators cannot commit
  112. /\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes
  113. /\ IsCorrectPower(Faulty, vs[h]) \* the correct validators have >2/3 of power
  114. /\ timestamp[h] > timestamp[h - 1] \* the time grows monotonically
  115. /\ timestamp[h] < timestamp[h - 1] + TRUSTING_PERIOD \* but not too fast
  116. \* form the block chain out of validator sets and commits (this makes apalache faster)
  117. /\ blockchain = [h \in Heights |->
  118. [height |-> h,
  119. time |-> timestamp[h],
  120. VS |-> vs[h],
  121. NextVS |-> IF h < ULTIMATE_HEIGHT THEN vs[h + 1] ELSE AllNodes,
  122. lastCommit |-> lastCommit[h]]
  123. ] \******
  124. (* is the blockchain in the faulty zone where the Tendermint security model does not apply *)
  125. InFaultyZone ==
  126. ~FaultAssumption(Faulty, now, blockchain)
  127. (********************* BLOCKCHAIN ACTIONS ********************************)
  128. (*
  129. Advance the clock by zero or more time units.
  130. *)
  131. AdvanceTime ==
  132. \E tm \in Int: tm >= now /\ now' = tm
  133. /\ UNCHANGED <<blockchain, Faulty>>
  134. (*
  135. One more process fails. As a result, the blockchain may move into the faulty zone.
  136. The light client is not using this action, as the faults are picked in the initial state.
  137. However, this action may be useful when reasoning about fork detection.
  138. *)
  139. OneMoreFault ==
  140. /\ \E n \in AllNodes \ Faulty:
  141. /\ Faulty' = Faulty \cup {n}
  142. /\ Faulty' /= AllNodes \* at least process remains non-faulty
  143. /\ UNCHANGED <<now, blockchain>>
  144. =============================================================================
  145. \* Modification History
  146. \* Last modified Wed Jun 10 14:10:54 CEST 2020 by igor
  147. \* Created Fri Oct 11 15:45:11 CEST 2019 by igor