Browse Source
Extending the blockchain specification (in the light client) to produce different ratios of faults (#183)
* cleaning unused definitions * introduced the ratio of faulty processespull/7804/head
Igor Konnov
4 years ago
committed by
GitHub
GitHub
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
16 changed files with 796 additions and 14 deletions
Split View
Diff Options
-
+164 -0rust-spec/lightclient/verification/Blockchain_003_draft.tla
-
+476 -0rust-spec/lightclient/verification/Lightclient_003_draft.tla
-
+9 -1rust-spec/lightclient/verification/MC4_3_correct.tla
-
+9 -1rust-spec/lightclient/verification/MC4_3_faulty.tla
-
+9 -1rust-spec/lightclient/verification/MC4_4_faulty.tla
-
+9 -1rust-spec/lightclient/verification/MC4_5_correct.tla
-
+9 -1rust-spec/lightclient/verification/MC4_5_faulty.tla
-
+9 -1rust-spec/lightclient/verification/MC4_6_faulty.tla
-
+9 -1rust-spec/lightclient/verification/MC4_7_faulty.tla
-
+10 -2rust-spec/lightclient/verification/MC5_5_correct.tla
-
+23 -0rust-spec/lightclient/verification/MC5_5_correct_peer_two_thirds_faulty.tla
-
+10 -2rust-spec/lightclient/verification/MC5_5_faulty.tla
-
+23 -0rust-spec/lightclient/verification/MC5_5_faulty_peer_two_thirds_faulty.tla
-
+9 -1rust-spec/lightclient/verification/MC5_7_faulty.tla
-
+9 -1rust-spec/lightclient/verification/MC7_5_faulty.tla
-
+9 -1rust-spec/lightclient/verification/MC7_7_faulty.tla
+ 164
- 0
rust-spec/lightclient/verification/Blockchain_003_draft.tla
View File
| @ -0,0 +1,164 @@ | |||
| ------------------------ 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 | |||
| 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 | |||
| now, | |||
| (* the current global time in integer units *) | |||
| 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 == <<now, 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) == | |||
| now < 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) == | |||
| /\ Faulty \in SUBSET AllNodes \* some nodes may fail | |||
| \* pick the validator sets and last commits | |||
| /\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]: | |||
| \E timestamp \in [Heights -> Int]: | |||
| \* now is at least as early as the timestamp in the last block | |||
| /\ \E tm \in Int: now = 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 >= now /\ now' = 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 | |||
+ 476
- 0
rust-spec/lightclient/verification/Lightclient_003_draft.tla
View File
| @ -0,0 +1,476 @@ | |||
| -------------------------- MODULE Lightclient_003_draft ---------------------------- | |||
| (** | |||
| * A state-machine specification of the lite client, following the English spec: | |||
| * | |||
| * https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md | |||
| *) | |||
| EXTENDS Integers, FiniteSets | |||
| \* the parameters of Light Client | |||
| CONSTANTS | |||
| TRUSTED_HEIGHT, | |||
| (* an index of the block header that the light client trusts by social consensus *) | |||
| TARGET_HEIGHT, | |||
| (* an index of the block header that the light client tries to verify *) | |||
| TRUSTING_PERIOD, | |||
| (* the period within which the validators are trusted *) | |||
| IS_PRIMARY_CORRECT, | |||
| (* is primary correct? *) | |||
| 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 (* see TypeOK below for the variable types *) | |||
| state, (* the current state of the light client *) | |||
| nextHeight, (* the next height to explore by the light client *) | |||
| nprobes (* the lite client iteration, or the number of block tests *) | |||
| (* the light store *) | |||
| VARIABLES | |||
| fetchedLightBlocks, (* a function from heights to LightBlocks *) | |||
| lightBlockStatus, (* a function from heights to block statuses *) | |||
| latestVerified (* the latest verified block *) | |||
| (* the variables of the lite client *) | |||
| lcvars == <<state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified>> | |||
| (* the light client previous state components, used for monitoring *) | |||
| VARIABLES | |||
| prevVerified, | |||
| prevCurrent, | |||
| prevNow, | |||
| prevVerdict | |||
| InitMonitor(verified, current, now, verdict) == | |||
| /\ prevVerified = verified | |||
| /\ prevCurrent = current | |||
| /\ prevNow = now | |||
| /\ prevVerdict = verdict | |||
| NextMonitor(verified, current, now, verdict) == | |||
| /\ prevVerified' = verified | |||
| /\ prevCurrent' = current | |||
| /\ prevNow' = now | |||
| /\ prevVerdict' = verdict | |||
| (******************* Blockchain instance ***********************************) | |||
| \* the parameters that are propagated into Blockchain | |||
| CONSTANTS | |||
| AllNodes | |||
| (* a set of all nodes that can act as validators (correct and faulty) *) | |||
| \* the state variables of Blockchain, see Blockchain.tla for the details | |||
| VARIABLES now, blockchain, Faulty | |||
| \* All the variables of Blockchain. For some reason, BC!vars does not work | |||
| bcvars == <<now, blockchain, Faulty>> | |||
| (* Create an instance of Blockchain. | |||
| We could write EXTENDS Blockchain, but then all the constants and state variables | |||
| would be hidden inside the Blockchain module. | |||
| *) | |||
| ULTIMATE_HEIGHT == TARGET_HEIGHT + 1 | |||
| BC == INSTANCE Blockchain_003_draft WITH | |||
| now <- now, blockchain <- blockchain, Faulty <- Faulty | |||
| (************************** Lite client ************************************) | |||
| (* the heights on which the light client is working *) | |||
| HEIGHTS == TRUSTED_HEIGHT..TARGET_HEIGHT | |||
| (* the control states of the lite client *) | |||
| States == { "working", "finishedSuccess", "finishedFailure" } | |||
| (** | |||
| Check the precondition of ValidAndVerified. | |||
| [LCV-FUNC-VALID.1::TLA-PRE.1] | |||
| *) | |||
| ValidAndVerifiedPre(trusted, untrusted) == | |||
| LET thdr == trusted.header | |||
| uhdr == untrusted.header | |||
| IN | |||
| /\ BC!InTrustingPeriod(thdr) | |||
| /\ thdr.height < uhdr.height | |||
| \* the trusted block has been created earlier (no drift here) | |||
| /\ thdr.time < uhdr.time | |||
| \* the untrusted block is not from the future | |||
| /\ uhdr.time < now | |||
| /\ 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 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 | |||
| (** | |||
| Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header. | |||
| [LCV-FUNC-VALID.1::TLA.1] | |||
| *) | |||
| ValidAndVerified(trusted, untrusted) == | |||
| IF ~ValidAndVerifiedPre(trusted, untrusted) | |||
| THEN "INVALID" | |||
| ELSE IF ~BC!InTrustingPeriod(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" | |||
| (* | |||
| Initial states of the light client. | |||
| Initially, only the trusted light block is present. | |||
| *) | |||
| LCInit == | |||
| /\ state = "working" | |||
| /\ nextHeight = TARGET_HEIGHT | |||
| /\ nprobes = 0 \* no tests have been done so far | |||
| /\ LET trustedBlock == blockchain[TRUSTED_HEIGHT] | |||
| trustedLightBlock == [header |-> trustedBlock, Commits |-> AllNodes] | |||
| IN | |||
| \* initially, fetchedLightBlocks is a function of one element, i.e., TRUSTED_HEIGHT | |||
| /\ fetchedLightBlocks = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock] | |||
| \* initially, lightBlockStatus is a function of one element, i.e., TRUSTED_HEIGHT | |||
| /\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"] | |||
| \* the latest verified block the the trusted block | |||
| /\ latestVerified = trustedLightBlock | |||
| /\ InitMonitor(trustedLightBlock, trustedLightBlock, now, "SUCCESS") | |||
| \* block should contain a copy of the block from the reference chain, with a matching commit | |||
| CopyLightBlockFromChain(block, height) == | |||
| LET ref == blockchain[height] | |||
| lastCommit == | |||
| IF height < ULTIMATE_HEIGHT | |||
| THEN blockchain[height + 1].lastCommit | |||
| \* for the ultimate block, which we never use, as ULTIMATE_HEIGHT = TARGET_HEIGHT + 1 | |||
| ELSE blockchain[height].VS | |||
| IN | |||
| block = [header |-> ref, Commits |-> lastCommit] | |||
| \* Either the primary is correct and the block comes from the reference chain, | |||
| \* or the block is produced by a faulty primary. | |||
| \* | |||
| \* [LCV-FUNC-FETCH.1::TLA.1] | |||
| FetchLightBlockInto(block, height) == | |||
| IF IS_PRIMARY_CORRECT | |||
| THEN CopyLightBlockFromChain(block, height) | |||
| ELSE BC!IsLightBlockAllowedByDigitalSignatures(height, block) | |||
| \* add a block into the light store | |||
| \* | |||
| \* [LCV-FUNC-UPDATE.1::TLA.1] | |||
| LightStoreUpdateBlocks(lightBlocks, block) == | |||
| LET ht == block.header.height IN | |||
| [h \in DOMAIN lightBlocks \union {ht} |-> | |||
| IF h = ht THEN block ELSE lightBlocks[h]] | |||
| \* update the state of a light block | |||
| \* | |||
| \* [LCV-FUNC-UPDATE.1::TLA.1] | |||
| LightStoreUpdateStates(statuses, ht, blockState) == | |||
| [h \in DOMAIN statuses \union {ht} |-> | |||
| IF h = ht THEN blockState ELSE statuses[h]] | |||
| \* Check, whether newHeight is a possible next height for the light client. | |||
| \* | |||
| \* [LCV-FUNC-SCHEDULE.1::TLA.1] | |||
| CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) == | |||
| LET ht == pLatestVerified.header.height IN | |||
| \/ /\ ht = pNextHeight | |||
| /\ ht < pTargetHeight | |||
| /\ pNextHeight < newHeight | |||
| /\ newHeight <= pTargetHeight | |||
| \/ /\ ht < pNextHeight | |||
| /\ ht < pTargetHeight | |||
| /\ ht < newHeight | |||
| /\ newHeight < pNextHeight | |||
| \/ /\ ht = pTargetHeight | |||
| /\ newHeight = pTargetHeight | |||
| \* The loop of VerifyToTarget. | |||
| \* | |||
| \* [LCV-FUNC-MAIN.1::TLA-LOOP.1] | |||
| VerifyToTargetLoop == | |||
| \* the loop condition is true | |||
| /\ latestVerified.header.height < TARGET_HEIGHT | |||
| \* pick a light block, which will be constrained later | |||
| /\ \E current \in BC!LightBlocks: | |||
| \* Get next LightBlock for verification | |||
| /\ IF nextHeight \in DOMAIN fetchedLightBlocks | |||
| THEN \* copy the block from the light store | |||
| /\ current = fetchedLightBlocks[nextHeight] | |||
| /\ UNCHANGED fetchedLightBlocks | |||
| ELSE \* retrieve a light block and save it in the light store | |||
| /\ FetchLightBlockInto(current, nextHeight) | |||
| /\ fetchedLightBlocks' = LightStoreUpdateBlocks(fetchedLightBlocks, current) | |||
| \* Record that one more probe has been done (for complexity and model checking) | |||
| /\ nprobes' = nprobes + 1 | |||
| \* Verify the current block | |||
| /\ LET verdict == ValidAndVerified(latestVerified, current) IN | |||
| NextMonitor(latestVerified, current, now, verdict) /\ | |||
| \* Decide whether/how to continue | |||
| CASE verdict = "SUCCESS" -> | |||
| /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified") | |||
| /\ latestVerified' = current | |||
| /\ state' = | |||
| IF latestVerified'.header.height < TARGET_HEIGHT | |||
| THEN "working" | |||
| ELSE "finishedSuccess" | |||
| /\ \E newHeight \in HEIGHTS: | |||
| /\ CanScheduleTo(newHeight, current, nextHeight, TARGET_HEIGHT) | |||
| /\ nextHeight' = newHeight | |||
| [] verdict = "NOT_ENOUGH_TRUST" -> | |||
| (* | |||
| do nothing: the light block current passed validation, but the validator | |||
| set is too different to verify it. We keep the state of | |||
| current at StateUnverified. For a later iteration, Schedule | |||
| might decide to try verification of that light block again. | |||
| *) | |||
| /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateUnverified") | |||
| /\ \E newHeight \in HEIGHTS: | |||
| /\ CanScheduleTo(newHeight, latestVerified, nextHeight, TARGET_HEIGHT) | |||
| /\ nextHeight' = newHeight | |||
| /\ UNCHANGED <<latestVerified, state>> | |||
| [] OTHER -> | |||
| \* verdict is some error code | |||
| /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateFailed") | |||
| /\ state' = "finishedFailure" | |||
| /\ UNCHANGED <<latestVerified, nextHeight>> | |||
| \* The terminating condition of VerifyToTarget. | |||
| \* | |||
| \* [LCV-FUNC-MAIN.1::TLA-LOOPCOND.1] | |||
| VerifyToTargetDone == | |||
| /\ latestVerified.header.height >= TARGET_HEIGHT | |||
| /\ state' = "finishedSuccess" | |||
| /\ UNCHANGED <<nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, latestVerified>> | |||
| /\ UNCHANGED <<prevVerified, prevCurrent, prevNow, prevVerdict>> | |||
| (********************* Lite client + Blockchain *******************) | |||
| Init == | |||
| \* the blockchain is initialized immediately to the ULTIMATE_HEIGHT | |||
| /\ BC!InitToHeight(FAULTY_RATIO) | |||
| \* the light client starts | |||
| /\ LCInit | |||
| (* | |||
| The system step is very simple. | |||
| The light client is either executing VerifyToTarget, or it has terminated. | |||
| (In the latter case, a model checker reports a deadlock.) | |||
| Simultaneously, the global clock may advance. | |||
| *) | |||
| Next == | |||
| /\ state = "working" | |||
| /\ VerifyToTargetLoop \/ VerifyToTargetDone | |||
| /\ BC!AdvanceTime \* the global clock is advanced by zero or more time units | |||
| (************************* Types ******************************************) | |||
| TypeOK == | |||
| /\ state \in States | |||
| /\ nextHeight \in HEIGHTS | |||
| /\ latestVerified \in BC!LightBlocks | |||
| /\ \E HS \in SUBSET HEIGHTS: | |||
| /\ fetchedLightBlocks \in [HS -> BC!LightBlocks] | |||
| /\ lightBlockStatus | |||
| \in [HS -> {"StateVerified", "StateUnverified", "StateFailed"}] | |||
| (************************* Properties ******************************************) | |||
| (* The properties to check *) | |||
| \* this invariant candidate is false | |||
| NeverFinish == | |||
| state = "working" | |||
| \* this invariant candidate is false | |||
| NeverFinishNegative == | |||
| state /= "finishedFailure" | |||
| \* This invariant holds true, when the primary is correct. | |||
| \* This invariant candidate is false when the primary is faulty. | |||
| NeverFinishNegativeWhenTrusted == | |||
| (*(minTrustedHeight <= TRUSTED_HEIGHT)*) | |||
| BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) | |||
| => state /= "finishedFailure" | |||
| \* this invariant candidate is false | |||
| NeverFinishPositive == | |||
| state /= "finishedSuccess" | |||
| (** | |||
| 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 == | |||
| \A h \in DOMAIN fetchedLightBlocks: | |||
| lightBlockStatus[h] = "StateVerified" => | |||
| fetchedLightBlocks[h].header = blockchain[h] | |||
| (** | |||
| *) | |||
| NoTrustOnFaultyBlockInv == | |||
| (state = "finishedSuccess" | |||
| /\ fetchedLightBlocks[TARGET_HEIGHT].header = blockchain[TARGET_HEIGHT]) | |||
| => CorrectnessInv | |||
| (** | |||
| Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "SUCCESS" pairwise | |||
| This property is easily violated, whenever a header cannot be trusted anymore. | |||
| *) | |||
| StoredHeadersAreVerifiedInv == | |||
| state = "finishedSuccess" | |||
| => | |||
| \A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers | |||
| \/ lh >= rh | |||
| \* either there is a header between them | |||
| \/ \E mh \in DOMAIN fetchedLightBlocks: | |||
| lh < mh /\ mh < rh | |||
| \* or we can verify the right one using the left one | |||
| \/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh]) | |||
| \* An improved version of StoredHeadersAreSound, assuming that a header may be not trusted. | |||
| \* This invariant candidate is also violated, | |||
| \* as there may be some unverified blocks left in the middle. | |||
| StoredHeadersAreVerifiedOrNotTrustedInv == | |||
| state = "finishedSuccess" | |||
| => | |||
| \A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers | |||
| \/ lh >= rh | |||
| \* either there is a header between them | |||
| \/ \E mh \in DOMAIN fetchedLightBlocks: | |||
| lh < mh /\ mh < rh | |||
| \* or we can verify the right one using the left one | |||
| \/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh]) | |||
| \* or the left header is outside the trusting period, so no guarantees | |||
| \/ ~BC!InTrustingPeriod(fetchedLightBlocks[lh].header) | |||
| (** | |||
| * An improved version of StoredHeadersAreSoundOrNotTrusted, | |||
| * checking the property only for the verified headers. | |||
| * This invariant holds true. | |||
| *) | |||
| ProofOfChainOfTrustInv == | |||
| state = "finishedSuccess" | |||
| => | |||
| \A lh, rh \in DOMAIN fetchedLightBlocks: | |||
| \* for every pair of stored headers that have been verified | |||
| \/ lh >= rh | |||
| \/ lightBlockStatus[lh] = "StateUnverified" | |||
| \/ lightBlockStatus[rh] = "StateUnverified" | |||
| \* 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 | |||
| \/ ~(BC!InTrustingPeriod(fetchedLightBlocks[lh].header)) | |||
| \* or we can verify the right one using the left one | |||
| \/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh]) | |||
| (** | |||
| * When the light client terminates, there are no failed blocks. (Otherwise, someone lied to us.) | |||
| *) | |||
| NoFailedBlocksOnSuccessInv == | |||
| state = "finishedSuccess" => | |||
| \A h \in DOMAIN fetchedLightBlocks: | |||
| lightBlockStatus[h] /= "StateFailed" | |||
| \* This property states that whenever the light client finishes with a positive outcome, | |||
| \* the trusted header is still within the trusting period. | |||
| \* We expect this property to be violated. And Apalache shows us a counterexample. | |||
| PositiveBeforeTrustedHeaderExpires == | |||
| (state = "finishedSuccess") => BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) | |||
| \* If the primary is correct and the initial trusted block has not expired, | |||
| \* then whenever the algorithm terminates, it reports "success" | |||
| CorrectPrimaryAndTimeliness == | |||
| (BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) | |||
| /\ state /= "working" /\ IS_PRIMARY_CORRECT) => | |||
| state = "finishedSuccess" | |||
| (** | |||
| If the primary is correct and there is a trusted block that has not expired, | |||
| then whenever the algorithm terminates, it reports "success". | |||
| [LCV-DIST-LIVE.1::SUCCESS-CORR-PRIMARY-CHAIN-OF-TRUST.1] | |||
| *) | |||
| SuccessOnCorrectPrimaryAndChainOfTrust == | |||
| (\E h \in DOMAIN fetchedLightBlocks: | |||
| lightBlockStatus[h] = "StateVerified" /\ BC!InTrustingPeriod(blockchain[h]) | |||
| /\ state /= "working" /\ IS_PRIMARY_CORRECT) => | |||
| state = "finishedSuccess" | |||
| \* Lite Client Completeness: If header h was correctly generated by an instance | |||
| \* of Tendermint consensus (and its age is less than the trusting period), | |||
| \* then the lite client should eventually set trust(h) to true. | |||
| \* | |||
| \* Note that Completeness assumes that the lite client communicates with a correct full node. | |||
| \* | |||
| \* We decompose completeness into Termination (liveness) and Precision (safety). | |||
| \* Once again, Precision is an inverse version of the safety property in Completeness, | |||
| \* as A => B is logically equivalent to ~B => ~A. | |||
| PrecisionInv == | |||
| (state = "finishedFailure") | |||
| => \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period | |||
| \/ \E h \in DOMAIN fetchedLightBlocks: | |||
| LET lightBlock == fetchedLightBlocks[h] IN | |||
| \* the full node lied to the lite client about the block header | |||
| \/ lightBlock.header /= blockchain[h] | |||
| \* the full node lied to the lite client about the commits | |||
| \/ lightBlock.Commits /= lightBlock.header.VS | |||
| \* the old invariant that was found to be buggy by TLC | |||
| PrecisionBuggyInv == | |||
| (state = "finishedFailure") | |||
| => \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period | |||
| \/ \E h \in DOMAIN fetchedLightBlocks: | |||
| LET lightBlock == fetchedLightBlocks[h] IN | |||
| \* the full node lied to the lite client about the block header | |||
| lightBlock.header /= blockchain[h] | |||
| \* the worst complexity | |||
| Complexity == | |||
| LET N == TARGET_HEIGHT - TRUSTED_HEIGHT + 1 IN | |||
| state /= "working" => | |||
| (2 * nprobes <= N * (N - 1)) | |||
| (* | |||
| We omit termination, as the algorithm deadlocks in the end. | |||
| So termination can be demonstrated by finding a deadlock. | |||
| Of course, one has to analyze the deadlocked state and see that | |||
| the algorithm has indeed terminated there. | |||
| *) | |||
| ============================================================================= | |||
| \* Modification History | |||
| \* Last modified Fri Jun 26 12:08:28 CEST 2020 by igor | |||
| \* Created Wed Oct 02 16:39:42 CEST 2019 by igor | |||
+ 9
- 1
rust-spec/lightclient/verification/MC4_3_correct.tla
View File
+ 9
- 1
rust-spec/lightclient/verification/MC4_3_faulty.tla
View File
+ 9
- 1
rust-spec/lightclient/verification/MC4_4_faulty.tla
View File
+ 9
- 1
rust-spec/lightclient/verification/MC4_5_correct.tla
View File
+ 9
- 1
rust-spec/lightclient/verification/MC4_5_faulty.tla
View File
+ 9
- 1
rust-spec/lightclient/verification/MC4_6_faulty.tla
View File
+ 9
- 1
rust-spec/lightclient/verification/MC4_7_faulty.tla
View File
+ 10
- 2
rust-spec/lightclient/verification/MC5_5_correct.tla
View File
+ 23
- 0
rust-spec/lightclient/verification/MC5_5_correct_peer_two_thirds_faulty.tla
View File
| @ -0,0 +1,23 @@ | |||
| ------------------- MODULE MC5_5_correct_peer_two_thirds_faulty ---------------------- | |||
| AllNodes == {"n1", "n2", "n3", "n4", "n5"} | |||
| TRUSTED_HEIGHT == 1 | |||
| TARGET_HEIGHT == 5 | |||
| TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) | |||
| IS_PRIMARY_CORRECT == TRUE | |||
| FAULTY_RATIO == <<2, 3>> \* < 1 / 3 faulty validators | |||
| VARIABLES | |||
| state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, | |||
| latestVerified, nprobes, | |||
| now, blockchain, Faulty | |||
| (* the light client previous state components, used for monitoring *) | |||
| VARIABLES | |||
| prevVerified, | |||
| prevCurrent, | |||
| prevNow, | |||
| prevVerdict | |||
| INSTANCE Lightclient_003_draft | |||
| ============================================================================ | |||
+ 10
- 2
rust-spec/lightclient/verification/MC5_5_faulty.tla
View File
| @ -1,15 +1,23 @@ | |||
| ------------------------- MODULE MC5_5_faulty --------------------------- | |||
| ----------------- MODULE MC5_5_faulty_peers_two_thirds_faulty --------------------- | |||
| AllNodes == {"n1", "n2", "n3", "n4", "n5"} | |||
| TRUSTED_HEIGHT == 1 | |||
| TARGET_HEIGHT == 5 | |||
| TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) | |||
| IS_PRIMARY_CORRECT == FALSE | |||
| FAULTY_RATIO == <<2, 3>> \* < 1 / 3 faulty validators | |||
| VARIABLES | |||
| state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, | |||
| latestVerified, nprobes, | |||
| now, blockchain, Faulty | |||
| INSTANCE Lightclient_A_1 | |||
| (* the light client previous state components, used for monitoring *) | |||
| VARIABLES | |||
| prevVerified, | |||
| prevCurrent, | |||
| prevNow, | |||
| prevVerdict | |||
| INSTANCE Lightclient_003_draft | |||
| ============================================================================ | |||
+ 23
- 0
rust-spec/lightclient/verification/MC5_5_faulty_peer_two_thirds_faulty.tla
View File
| @ -0,0 +1,23 @@ | |||
| ----------------- MODULE MC5_5_faulty_peer_two_thirds_faulty --------------------- | |||
| AllNodes == {"n1", "n2", "n3", "n4", "n5"} | |||
| TRUSTED_HEIGHT == 1 | |||
| TARGET_HEIGHT == 5 | |||
| TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) | |||
| IS_PRIMARY_CORRECT == FALSE | |||
| FAULTY_RATIO == <<2, 3>> \* < 2 / 3 faulty validators | |||
| VARIABLES | |||
| state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, | |||
| latestVerified, nprobes, | |||
| now, blockchain, Faulty | |||
| (* the light client previous state components, used for monitoring *) | |||
| VARIABLES | |||
| prevVerified, | |||
| prevCurrent, | |||
| prevNow, | |||
| prevVerdict | |||
| INSTANCE Lightclient_003_draft | |||
| ============================================================================ | |||