From bb86a3d508bc9e66ec7875a9d96c4d4fac041706 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 26 Jun 2020 15:00:36 +0200 Subject: [PATCH] Light Client TLA+ Specification (#314) * the initial version from the old light client bisection * an intermediate version * the first version that Josef and I believe is ok * something is working * a workaround for #148 in apalache * super fast encoding: the blockchain is initialized, time is integer * more realistic time resolution * the complexity bound and other cool things * comments on the light client spec * cleaned up the MC models * removed the now redundant height * fixed a bug in Next and simplified it * updating the experimental setup for the AFT paper * reordering the experiments * updates after review by Anca --- docs/spec/lightclient/001bmc-apalache.csv | 49 +++ docs/spec/lightclient/Blockchain_A_1.tla | 171 +++++++++ docs/spec/lightclient/Lightclient_A_1.tla | 440 ++++++++++++++++++++++ docs/spec/lightclient/MC4_3_correct.tla | 15 + docs/spec/lightclient/MC4_3_faulty.tla | 15 + docs/spec/lightclient/MC4_4_faulty.tla | 15 + docs/spec/lightclient/MC4_5_correct.tla | 15 + docs/spec/lightclient/MC4_5_faulty.tla | 15 + docs/spec/lightclient/MC4_6_faulty.tla | 15 + docs/spec/lightclient/MC4_7_faulty.tla | 15 + docs/spec/lightclient/MC5_5_correct.tla | 15 + docs/spec/lightclient/MC5_5_faulty.tla | 15 + docs/spec/lightclient/MC5_7_faulty.tla | 15 + docs/spec/lightclient/MC7_5_faulty.tla | 15 + docs/spec/lightclient/MC7_7_faulty.tla | 15 + 15 files changed, 840 insertions(+) create mode 100644 docs/spec/lightclient/001bmc-apalache.csv create mode 100644 docs/spec/lightclient/Blockchain_A_1.tla create mode 100644 docs/spec/lightclient/Lightclient_A_1.tla create mode 100644 docs/spec/lightclient/MC4_3_correct.tla create mode 100644 docs/spec/lightclient/MC4_3_faulty.tla create mode 100644 docs/spec/lightclient/MC4_4_faulty.tla create mode 100644 docs/spec/lightclient/MC4_5_correct.tla create mode 100644 docs/spec/lightclient/MC4_5_faulty.tla create mode 100644 docs/spec/lightclient/MC4_6_faulty.tla create mode 100644 docs/spec/lightclient/MC4_7_faulty.tla create mode 100644 docs/spec/lightclient/MC5_5_correct.tla create mode 100644 docs/spec/lightclient/MC5_5_faulty.tla create mode 100644 docs/spec/lightclient/MC5_7_faulty.tla create mode 100644 docs/spec/lightclient/MC7_5_faulty.tla create mode 100644 docs/spec/lightclient/MC7_7_faulty.tla diff --git a/docs/spec/lightclient/001bmc-apalache.csv b/docs/spec/lightclient/001bmc-apalache.csv new file mode 100644 index 000000000..8d5ad8ea3 --- /dev/null +++ b/docs/spec/lightclient/001bmc-apalache.csv @@ -0,0 +1,49 @@ +no,filename,tool,timeout,init,inv,next,args +1,MC4_3_correct.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30 +2,MC4_3_correct.tla,apalache,1h,,CorrectnessInv,,--length=30 +3,MC4_3_correct.tla,apalache,1h,,PrecisionInv,,--length=30 +4,MC4_3_correct.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30 +5,MC4_3_correct.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30 +6,MC4_3_correct.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30 +7,MC4_3_correct.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30 +8,MC4_3_correct.tla,apalache,1h,,Complexity,,--length=30 +9,MC4_3_faulty.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30 +10,MC4_3_faulty.tla,apalache,1h,,CorrectnessInv,,--length=30 +11,MC4_3_faulty.tla,apalache,1h,,PrecisionInv,,--length=30 +12,MC4_3_faulty.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30 +13,MC4_3_faulty.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30 +14,MC4_3_faulty.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30 +15,MC4_3_faulty.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30 +16,MC4_3_faulty.tla,apalache,1h,,Complexity,,--length=30 +17,MC5_5_correct.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30 +18,MC5_5_correct.tla,apalache,1h,,CorrectnessInv,,--length=30 +19,MC5_5_correct.tla,apalache,1h,,PrecisionInv,,--length=30 +20,MC5_5_correct.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30 +21,MC5_5_correct.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30 +22,MC5_5_correct.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30 +23,MC5_5_correct.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30 +24,MC5_5_correct.tla,apalache,1h,,Complexity,,--length=30 +25,MC5_5_faulty.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30 +26,MC5_5_faulty.tla,apalache,1h,,CorrectnessInv,,--length=30 +27,MC5_5_faulty.tla,apalache,1h,,PrecisionInv,,--length=30 +28,MC5_5_faulty.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30 +29,MC5_5_faulty.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30 +30,MC5_5_faulty.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30 +31,MC5_5_faulty.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30 +32,MC5_5_faulty.tla,apalache,1h,,Complexity,,--length=30 +33,MC7_5_faulty.tla,apalache,10h,,PositiveBeforeTrustedHeaderExpires,,--length=30 +34,MC7_5_faulty.tla,apalache,10h,,CorrectnessInv,,--length=30 +35,MC7_5_faulty.tla,apalache,10h,,PrecisionInv,,--length=30 +36,MC7_5_faulty.tla,apalache,10h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30 +37,MC7_5_faulty.tla,apalache,10h,,NoFailedBlocksOnSuccessInv,,--length=30 +38,MC7_5_faulty.tla,apalache,10h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30 +39,MC7_5_faulty.tla,apalache,10h,,CorrectPrimaryAndTimeliness,,--length=30 +40,MC7_5_faulty.tla,apalache,10h,,Complexity,,--length=30 +41,MC4_7_faulty.tla,apalache,10h,,PositiveBeforeTrustedHeaderExpires,,--length=30 +42,MC4_7_faulty.tla,apalache,10h,,CorrectnessInv,,--length=30 +43,MC4_7_faulty.tla,apalache,10h,,PrecisionInv,,--length=30 +44,MC4_7_faulty.tla,apalache,10h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30 +45,MC4_7_faulty.tla,apalache,10h,,NoFailedBlocksOnSuccessInv,,--length=30 +46,MC4_7_faulty.tla,apalache,10h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30 +47,MC4_7_faulty.tla,apalache,10h,,CorrectPrimaryAndTimeliness,,--length=30 +48,MC4_7_faulty.tla,apalache,10h,,Complexity,,--length=30 diff --git a/docs/spec/lightclient/Blockchain_A_1.tla b/docs/spec/lightclient/Blockchain_A_1.tla new file mode 100644 index 000000000..70f59bf97 --- /dev/null +++ b/docs/spec/lightclient/Blockchain_A_1.tla @@ -0,0 +1,171 @@ +------------------------ MODULE Blockchain_A_1 ----------------------------- +(* + 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 == <> + +(* 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. + *) +IsCorrectPower(pFaultyNodes, pVS) == + 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, so we write CP > 2.0 / 3 * TP as follows: + CP > 2 * FP \* Note: when FP = 0, this implies CP > 0. + +(* This is what we believe is the assumption about failures in Tendermint *) +FaultAssumption(pFaultyNodes, pNow, pBlockchain) == + \A h \in Heights: + pBlockchain[h].time + TRUSTING_PERIOD > pNow => + IsCorrectPower(pFaultyNodes, pBlockchain[h].NextVS) + +(* 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 \* 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. + *) +InitToHeight == + /\ 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 + /\ IsCorrectPower(Faulty, vs[h]) \* the correct validators have >2/3 of power + /\ 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]] + ] \****** + + +(* is the blockchain in the faulty zone where the Tendermint security model does not apply *) +InFaultyZone == + ~FaultAssumption(Faulty, now, blockchain) + +(********************* BLOCKCHAIN ACTIONS ********************************) +(* + Advance the clock by zero or more time units. + *) +AdvanceTime == + \E tm \in Int: tm >= now /\ now' = tm + /\ UNCHANGED <> + +(* + One more process fails. As a result, the blockchain may move into the faulty zone. + The light client is not using this action, as the faults are picked in the initial state. + However, this action may be useful when reasoning about fork detection. + *) +OneMoreFault == + /\ \E n \in AllNodes \ Faulty: + /\ Faulty' = Faulty \cup {n} + /\ Faulty' /= AllNodes \* at least process remains non-faulty + /\ UNCHANGED <> +============================================================================= +\* 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 diff --git a/docs/spec/lightclient/Lightclient_A_1.tla b/docs/spec/lightclient/Lightclient_A_1.tla new file mode 100644 index 000000000..f4034d7b9 --- /dev/null +++ b/docs/spec/lightclient/Lightclient_A_1.tla @@ -0,0 +1,440 @@ +-------------------------- MODULE Lightclient_A_1 ---------------------------- +(** + * 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? *) + +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 == <> + +(******************* 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 == <> + +(* 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_A_1 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. + + TODO: add a traceability tag as soon as the English spec has one + *) +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 + /\ 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. + + TODO: add traceability tag as soon as the English spec has one + *) +ValidAndVerified(trusted, untrusted) == + IF ~ValidAndVerifiedPre(trusted, untrusted) + THEN "FAILED_VERIFICATION" + 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 "OK" + ELSE "CANNOT_VERIFY" + +(* + 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 + +\* 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. +\* +\* TODO: add a traceability tag when Josef adds it in the English spec +FetchLightBlockInto(block, height) == + IF IS_PRIMARY_CORRECT + THEN CopyLightBlockFromChain(block, height) + ELSE BC!IsLightBlockAllowedByDigitalSignatures(height, block) + +\* add a block into the light store +\* +\* TODO: add a traceability tag when Josef adds it in the English spec +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 +\* +\* TODO: add a traceability tag when Josef adds it in the English spec +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. +\* +\* TODO: add a traceability tag when Josef adds it in the English spec +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. +\* +\* TODO: add a traceability tag when Josef adds it in the English spec +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 + \* Decide whether/how to continue + CASE verdict = "OK" -> + /\ 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 = "CANNOT_VERIFY" -> + (* + 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 <> + + [] OTHER -> + \* verdict is some error code + /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateFailed") + /\ state' = "finishedFailure" + /\ UNCHANGED <> + +\* The terminating condition of VerifyToTarget. +\* +\* TODO: add a traceability tag when Josef adds it in the English spec +VerifyToTargetDone == + /\ latestVerified.header.height >= TARGET_HEIGHT + /\ state' = "finishedSuccess" + /\ UNCHANGED <> + +(********************* Lite client + Blockchain *******************) +Init == + \* the blockchain is initialized immediately to the ULTIMATE_HEIGHT + /\ BC!InitToHeight + \* 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] + +(** + Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "OK" 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 + \/ "OK" = 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 + \/ "OK" = 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 + \/ "OK" = 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 diff --git a/docs/spec/lightclient/MC4_3_correct.tla b/docs/spec/lightclient/MC4_3_correct.tla new file mode 100644 index 000000000..951a471da --- /dev/null +++ b/docs/spec/lightclient/MC4_3_correct.tla @@ -0,0 +1,15 @@ +---------------------------- MODULE MC4_3_correct --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 3 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == TRUE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================== diff --git a/docs/spec/lightclient/MC4_3_faulty.tla b/docs/spec/lightclient/MC4_3_faulty.tla new file mode 100644 index 000000000..c711ee9b8 --- /dev/null +++ b/docs/spec/lightclient/MC4_3_faulty.tla @@ -0,0 +1,15 @@ +---------------------------- MODULE MC4_3_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 3 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================== diff --git a/docs/spec/lightclient/MC4_4_faulty.tla b/docs/spec/lightclient/MC4_4_faulty.tla new file mode 100644 index 000000000..8b8d25ece --- /dev/null +++ b/docs/spec/lightclient/MC4_4_faulty.tla @@ -0,0 +1,15 @@ +---------------------------- MODULE MC4_4_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 4 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================== diff --git a/docs/spec/lightclient/MC4_5_correct.tla b/docs/spec/lightclient/MC4_5_correct.tla new file mode 100644 index 000000000..04489ec7f --- /dev/null +++ b/docs/spec/lightclient/MC4_5_correct.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_5_correct --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == TRUE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC4_5_faulty.tla b/docs/spec/lightclient/MC4_5_faulty.tla new file mode 100644 index 000000000..11dbd2ec6 --- /dev/null +++ b/docs/spec/lightclient/MC4_5_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_5_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC4_6_faulty.tla b/docs/spec/lightclient/MC4_6_faulty.tla new file mode 100644 index 000000000..d0d98444f --- /dev/null +++ b/docs/spec/lightclient/MC4_6_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_6_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 6 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC4_7_faulty.tla b/docs/spec/lightclient/MC4_7_faulty.tla new file mode 100644 index 000000000..60dcd3c5d --- /dev/null +++ b/docs/spec/lightclient/MC4_7_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_7_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 7 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC5_5_correct.tla b/docs/spec/lightclient/MC5_5_correct.tla new file mode 100644 index 000000000..926501761 --- /dev/null +++ b/docs/spec/lightclient/MC5_5_correct.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC5_5_correct --------------------------- + +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 + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC5_5_faulty.tla b/docs/spec/lightclient/MC5_5_faulty.tla new file mode 100644 index 000000000..abf5e8c72 --- /dev/null +++ b/docs/spec/lightclient/MC5_5_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC5_5_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 + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC5_7_faulty.tla b/docs/spec/lightclient/MC5_7_faulty.tla new file mode 100644 index 000000000..5d3d265ab --- /dev/null +++ b/docs/spec/lightclient/MC5_7_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC5_7_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 7 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC7_5_faulty.tla b/docs/spec/lightclient/MC7_5_faulty.tla new file mode 100644 index 000000000..ae8af692a --- /dev/null +++ b/docs/spec/lightclient/MC7_5_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC7_5_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5", "n6", "n7"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/docs/spec/lightclient/MC7_7_faulty.tla b/docs/spec/lightclient/MC7_7_faulty.tla new file mode 100644 index 000000000..84065214e --- /dev/null +++ b/docs/spec/lightclient/MC7_7_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC7_7_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5", "n6", "n7"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 7 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================