diff --git a/rust-spec/lightclient/README.md b/rust-spec/lightclient/README.md index 9dbc81f3b..6441e8ed6 100644 --- a/rust-spec/lightclient/README.md +++ b/rust-spec/lightclient/README.md @@ -34,27 +34,36 @@ many intermediate headers by exploiting overlap in trusted and untrusted validat When there is not enough overlap, a bisection routine can be used to find a minimal set of headers that do provide the required overlap. -The [TLA+ specification](verification/Lightclient_A_1.tla) is a formal description of the +The [TLA+ specification ver. 001](verification/Lightclient_A_1.tla) +is a formal description of the commit verification protocol executed by a client, including the safety and -liveness properties, which can be model checked with Apalache. +termination, which can be model checked with Apalache. + +A more detailed TLA+ specification of +[Light client verification ver. 003](verification/Lightclient_003_draft.tla) +is currently under peer review. The `MC*.tla` files contain concrete parameters for the [TLA+ specification](verification/Lightclient_A_1.tla), in order to do model checking. For instance, [MC4_3_faulty.tla](verification/MC4_3_faulty.tla) contains the following parameters -for the nodes, heights, the trusting period, and correctness of the primary node: +for the nodes, heights, the trusting period, the clock drifts, +correctness of the primary node, and the ratio of the faulty processes: ```tla AllNodes == {"n1", "n2", "n3", "n4"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 3 -TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +TRUSTING_PERIOD == 1400 \* the trusting period in some time units +CLOCK_DRIFT = 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT = 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE +FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators ``` To run a complete set of experiments, clone [apalache](https://github.com/informalsystems/apalache) and [apalache-tests](https://github.com/informalsystems/apalache-tests) into a directory `$DIR` and run the following commands: ```sh -$DIR/apalache-tests/scripts/mk-run.py --memlimit 28 001bmc-apalache.csv $DIR/apalache . out +$DIR/apalache-tests/scripts/mk-run.py --memlimit 28 002bmc-apalache-ok.csv $DIR/apalache . out ./out/run-all.sh ``` @@ -65,7 +74,23 @@ cd ./out $DIR/apalache-tests/scripts/parse-logs.py --human . ``` -The following table summarizes the experimental results. The TLA+ properties can be found in the +All lines in `results.csv` should report `Deadlock`, which means that the algorithm +has terminated and no invariant violation was found. + +Similar to [002bmc-apalache-ok.csv](verification/002bmc-apalache-ok.csv), +file [003bmc-apalache-error.csv](verification/003bmc-apalache-error.csv) specifies +the set of experiments that should result in counterexamples: + +```sh +$DIR/apalache-tests/scripts/mk-run.py --memlimit 28 003bmc-apalache-error.csv $DIR/apalache . out +./out/run-all.sh +``` + +All lines in `results.csv` should report `Error`. + + +The following table summarizes the experimental results for Light client verification +version 001. The TLA+ properties can be found in the [TLA+ specification](verification/Lightclient_A_1.tla). The experiments were run in an AWS instance equipped with 32GB RAM and a 4-core Intel® Xeon® CPU E5-2686 v4 @ 2.30GHz CPU. @@ -74,6 +99,8 @@ no bug is reported up to depth k. ![Experimental results](experiments.png) +The experimental results for version 003 are to be added. + ## Attack Detection The [English specification](detection/detection_003_reviewed.md) @@ -92,7 +119,61 @@ and generates of misbehavior that can be submitted to a full node so that the faulty validators can be punished. -There is no TLA+ yet. +The [TLA+ specification](detection/LCDetector_003_draft.tla) +is a formal description of the +detection protocol for two peers, including the safety and +termination, which can be model checked with Apalache. + + +The `LCD_MC*.tla` files contain concrete parameters for the +[TLA+ specification](detection/LCDetector_003_draft.tla), +in order to run the model checker. +For instance, [LCD_MC4_4_faulty.tla](detection/MC4_4_faulty.tla) +contains the following parameters +for the nodes, heights, the trusting period, the clock drifts, +correctness of the nodes, and the ratio of the faulty processes: + +```tla +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 3 +TRUSTING_PERIOD == 1400 \* the trusting period in some time units +CLOCK_DRIFT = 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT = 3 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == FALSE +IS_SECONDARY_CORRECT == FALSE +FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators +``` + +To run a complete set of experiments, clone [apalache](https://github.com/informalsystems/apalache) and [apalache-tests](https://github.com/informalsystems/apalache-tests) into a directory `$DIR` and run the following commands: + +```sh +$DIR/apalache-tests/scripts/mk-run.py --memlimit 28 004bmc-apalache-ok.csv $DIR/apalache . out +./out/run-all.sh +``` + +After the experiments have finished, you can collect the logs by executing the following command: + +```sh +cd ./out +$DIR/apalache-tests/scripts/parse-logs.py --human . +``` + +All lines in `results.csv` should report `Deadlock`, which means that the algorithm +has terminated and no invariant violation was found. + +Similar to [004bmc-apalache-ok.csv](verification/004bmc-apalache-ok.csv), +file [005bmc-apalache-error.csv](verification/005bmc-apalache-error.csv) specifies +the set of experiments that should result in counterexamples: + +```sh +$DIR/apalache-tests/scripts/mk-run.py --memlimit 28 005bmc-apalache-error.csv $DIR/apalache . out +./out/run-all.sh +``` + +All lines in `results.csv` should report `Error`. + +The detailed experimental results are to be added soon. ## Fork Accountability diff --git a/rust-spec/lightclient/detection/004bmc-apalache-ok.csv b/rust-spec/lightclient/detection/004bmc-apalache-ok.csv new file mode 100644 index 000000000..bf4f53ea2 --- /dev/null +++ b/rust-spec/lightclient/detection/004bmc-apalache-ok.csv @@ -0,0 +1,10 @@ +no;filename;tool;timeout;init;inv;next;args +1;LCD_MC3_3_faulty.tla;apalache;1h;;CommonHeightOnEvidenceInv;;--length=10 +2;LCD_MC3_3_faulty.tla;apalache;1h;;AccuracyInv;;--length=10 +3;LCD_MC3_3_faulty.tla;apalache;1h;;PrecisionInvLocal;;--length=10 +4;LCD_MC3_4_faulty.tla;apalache;1h;;CommonHeightOnEvidenceInv;;--length=10 +5;LCD_MC3_4_faulty.tla;apalache;1h;;AccuracyInv;;--length=10 +6;LCD_MC3_4_faulty.tla;apalache;1h;;PrecisionInvLocal;;--length=10 +7;LCD_MC4_4_faulty.tla;apalache;1h;;CommonHeightOnEvidenceInv;;--length=10 +8;LCD_MC4_4_faulty.tla;apalache;1h;;AccuracyInv;;--length=10 +9;LCD_MC4_4_faulty.tla;apalache;1h;;PrecisionInvLocal;;--length=10 diff --git a/rust-spec/lightclient/detection/005bmc-apalache-error.csv b/rust-spec/lightclient/detection/005bmc-apalache-error.csv new file mode 100644 index 000000000..1b9dd05ca --- /dev/null +++ b/rust-spec/lightclient/detection/005bmc-apalache-error.csv @@ -0,0 +1,4 @@ +no;filename;tool;timeout;init;inv;next;args +1;LCD_MC3_3_faulty.tla;apalache;1h;;PrecisionInvGrayZone;;--length=10 +2;LCD_MC3_4_faulty.tla;apalache;1h;;PrecisionInvGrayZone;;--length=10 +3;LCD_MC4_4_faulty.tla;apalache;1h;;PrecisionInvGrayZone;;--length=10 diff --git a/rust-spec/lightclient/detection/Blockchain_003_draft.tla b/rust-spec/lightclient/detection/Blockchain_003_draft.tla new file mode 100644 index 000000000..2b37c1b18 --- /dev/null +++ b/rust-spec/lightclient/detection/Blockchain_003_draft.tla @@ -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 + 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 == <> + +(* 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 <> 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 <> 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]: + \* 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 <> + +============================================================================= +\* 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/rust-spec/lightclient/detection/LCD_MC3_3_faulty.tla b/rust-spec/lightclient/detection/LCD_MC3_3_faulty.tla new file mode 100644 index 000000000..cef1df4d3 --- /dev/null +++ b/rust-spec/lightclient/detection/LCD_MC3_3_faulty.tla @@ -0,0 +1,27 @@ +------------------------- MODULE LCD_MC3_3_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 3 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == FALSE +IS_SECONDARY_CORRECT == TRUE +FAULTY_RATIO == <<2, 3>> \* < 1 / 3 faulty validators + +VARIABLES + blockchain, (* the reference blockchain *) + localClock, (* current time in the light client *) + refClock, (* current time in the reference blockchain *) + Faulty, (* the set of faulty validators *) + state, (* the state of the light client detector *) + fetchedLightBlocks1, (* a function from heights to LightBlocks *) + fetchedLightBlocks2, (* a function from heights to LightBlocks *) + fetchedLightBlocks1b, (* a function from heights to LightBlocks *) + commonHeight, (* the height that is trusted in CreateEvidenceForPeer *) + nextHeightToTry, (* the index in CreateEvidenceForPeer *) + evidences + +INSTANCE LCDetector_003_draft +============================================================================ diff --git a/rust-spec/lightclient/detection/LCD_MC3_4_faulty.tla b/rust-spec/lightclient/detection/LCD_MC3_4_faulty.tla new file mode 100644 index 000000000..06bcdee13 --- /dev/null +++ b/rust-spec/lightclient/detection/LCD_MC3_4_faulty.tla @@ -0,0 +1,27 @@ +------------------------- MODULE LCD_MC3_4_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 4 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == FALSE +IS_SECONDARY_CORRECT == TRUE +FAULTY_RATIO == <<2, 3>> \* < 1 / 3 faulty validators + +VARIABLES + blockchain, (* the reference blockchain *) + localClock, (* current time in the light client *) + refClock, (* current time in the reference blockchain *) + Faulty, (* the set of faulty validators *) + state, (* the state of the light client detector *) + fetchedLightBlocks1, (* a function from heights to LightBlocks *) + fetchedLightBlocks2, (* a function from heights to LightBlocks *) + fetchedLightBlocks1b, (* a function from heights to LightBlocks *) + commonHeight, (* the height that is trusted in CreateEvidenceForPeer *) + nextHeightToTry, (* the index in CreateEvidenceForPeer *) + evidences + +INSTANCE LCDetector_003_draft +============================================================================ diff --git a/rust-spec/lightclient/detection/LCD_MC4_4_faulty.tla b/rust-spec/lightclient/detection/LCD_MC4_4_faulty.tla new file mode 100644 index 000000000..fdb97d961 --- /dev/null +++ b/rust-spec/lightclient/detection/LCD_MC4_4_faulty.tla @@ -0,0 +1,27 @@ +------------------------- MODULE LCD_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 :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == FALSE +IS_SECONDARY_CORRECT == TRUE +FAULTY_RATIO == <<2, 3>> \* < 2 / 3 faulty validators + +VARIABLES + blockchain, (* the reference blockchain *) + localClock, (* current time in the light client *) + refClock, (* current time in the reference blockchain *) + Faulty, (* the set of faulty validators *) + state, (* the state of the light client detector *) + fetchedLightBlocks1, (* a function from heights to LightBlocks *) + fetchedLightBlocks2, (* a function from heights to LightBlocks *) + fetchedLightBlocks1b, (* a function from heights to LightBlocks *) + commonHeight, (* the height that is trusted in CreateEvidenceForPeer *) + nextHeightToTry, (* the index in CreateEvidenceForPeer *) + evidences + +INSTANCE LCDetector_003_draft +============================================================================ diff --git a/rust-spec/lightclient/detection/LCD_MC5_5_faulty.tla b/rust-spec/lightclient/detection/LCD_MC5_5_faulty.tla new file mode 100644 index 000000000..fdbd87b8b --- /dev/null +++ b/rust-spec/lightclient/detection/LCD_MC5_5_faulty.tla @@ -0,0 +1,27 @@ +------------------------- MODULE LCD_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 :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == FALSE +IS_SECONDARY_CORRECT == TRUE +FAULTY_RATIO == <<2, 3>> \* < 1 / 3 faulty validators + +VARIABLES + blockchain, (* the reference blockchain *) + localClock, (* current time in the light client *) + refClock, (* current time in the reference blockchain *) + Faulty, (* the set of faulty validators *) + state, (* the state of the light client detector *) + fetchedLightBlocks1, (* a function from heights to LightBlocks *) + fetchedLightBlocks2, (* a function from heights to LightBlocks *) + fetchedLightBlocks1b, (* a function from heights to LightBlocks *) + commonHeight, (* the height that is trusted in CreateEvidenceForPeer *) + nextHeightToTry, (* the index in CreateEvidenceForPeer *) + evidences + +INSTANCE LCDetector_003_draft +============================================================================ diff --git a/rust-spec/lightclient/detection/LCDetector_003_draft.tla b/rust-spec/lightclient/detection/LCDetector_003_draft.tla new file mode 100644 index 000000000..e2d32e996 --- /dev/null +++ b/rust-spec/lightclient/detection/LCDetector_003_draft.tla @@ -0,0 +1,373 @@ +-------------------------- MODULE LCDetector_003_draft ----------------------------- +(** + * This is a specification of the light client detector module. + * It follows the English specification: + * + * https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md + * + * The assumptions made in this specification: + * + * - light client connects to one primary and one secondary peer + * + * - the light client has its own local clock that can drift from the reference clock + * within the envelope [refClock - CLOCK_DRIFT, refClock + CLOCK_DRIFT]. + * The local clock may increase as well as decrease in the the envelope + * (similar to clock synchronization). + * + * - the ratio of the faulty validators is set as the parameter. + * + * Igor Konnov, Josef Widder, 2020 + *) + +EXTENDS Integers + +\* the parameters of Light Client +CONSTANTS + AllNodes, + (* a set of all nodes that can act as validators (correct and faulty) *) + 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 *) + 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 <> that limits that ratio of faulty validator in the blockchain + from above (exclusive). Tendermint security model prescribes 1 / 3. *) + IS_PRIMARY_CORRECT, + IS_SECONDARY_CORRECT + +VARIABLES + blockchain, (* the reference blockchain *) + localClock, (* the local clock of the light client *) + refClock, (* the reference clock in the reference blockchain *) + Faulty, (* the set of faulty validators *) + state, (* the state of the light client detector *) + fetchedLightBlocks1, (* a function from heights to LightBlocks *) + fetchedLightBlocks2, (* a function from heights to LightBlocks *) + fetchedLightBlocks1b, (* a function from heights to LightBlocks *) + commonHeight, (* the height that is trusted in CreateEvidenceForPeer *) + nextHeightToTry, (* the index in CreateEvidenceForPeer *) + evidences (* a set of evidences *) + +vars == <> + +\* (old) type annotations in Apalache +a <: b == a + + +\* instantiate a reference chain +ULTIMATE_HEIGHT == TARGET_HEIGHT + 1 +BC == INSTANCE Blockchain_003_draft + WITH ULTIMATE_HEIGHT <- (TARGET_HEIGHT + 1) + +\* use the light client API +LC == INSTANCE LCVerificationApi_003_draft + +\* evidence type +ET == [peer |-> STRING, conflictingBlock |-> BC!LBT, commonHeight |-> Int] + +\* is the algorithm in the terminating state +IsTerminated == + state \in { <<"NoEvidence", "PRIMARY">>, + <<"NoEvidence", "SECONDARY">>, + <<"FaultyPeer", "PRIMARY">>, + <<"FaultyPeer", "SECONDARY">>, + <<"FoundEvidence", "PRIMARY">> } + + +(********************************* Initialization ******************************) + +\* initialization for the light blocks data structure +InitLightBlocks(lb, Heights) == + \* BC!LightBlocks is an infinite set, as time is not restricted. + \* Hence, we initialize the light blocks by picking the sets inside. + \E vs, nextVS, lastCommit, commit \in [Heights -> SUBSET AllNodes]: + \* although [Heights -> Int] is an infinite set, + \* Apalache needs just one instance of this set, so it does not complain. + \E timestamp \in [Heights -> Int]: + LET hdr(h) == + [height |-> h, + time |-> timestamp[h], + VS |-> vs[h], + NextVS |-> nextVS[h], + lastCommit |-> lastCommit[h]] + IN + LET lightHdr(h) == + [header |-> hdr(h), Commits |-> commit[h]] + IN + lb = [ h \in Heights |-> lightHdr(h) ] + +\* initialize the detector algorithm +Init == + \* initialize the blockchain to TARGET_HEIGHT + 1 + /\ BC!InitToHeight(FAULTY_RATIO) + /\ \E tm \in Int: + tm >= 0 /\ LC!IsLocalClockWithinDrift(tm, refClock) /\ localClock = tm + \* start with the secondary looking for evidence + /\ state = <<"Init", "SECONDARY">> /\ commonHeight = 0 /\ nextHeightToTry = 0 + /\ evidences = {} <: {ET} + \* Precompute a possible result of light client verification for the primary. + \* It is the input to the detection algorithm. + /\ \E Heights1 \in SUBSET(TRUSTED_HEIGHT..TARGET_HEIGHT): + /\ TRUSTED_HEIGHT \in Heights1 + /\ TARGET_HEIGHT \in Heights1 + /\ InitLightBlocks(fetchedLightBlocks1, Heights1) + \* As we have a non-deterministic scheduler, for every trace that has + \* an unverified block, there is a filtered trace that only has verified + \* blocks. This is a deep observation. + /\ LET status == [h \in Heights1 |-> "StateVerified"] IN + LC!VerifyToTargetPost(blockchain, IS_PRIMARY_CORRECT, + fetchedLightBlocks1, status, + TRUSTED_HEIGHT, TARGET_HEIGHT, "finishedSuccess") + \* initialize the other data structures to the default values + /\ LET trustedBlock == blockchain[TRUSTED_HEIGHT] + trustedLightBlock == [header |-> trustedBlock, Commits |-> AllNodes] + IN + /\ fetchedLightBlocks2 = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock] + /\ fetchedLightBlocks1b = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock] + + +(********************************* Transitions ******************************) + +\* a 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(isPeerCorrect, block, height) == + IF isPeerCorrect + THEN CopyLightBlockFromChain(block, height) + ELSE BC!IsLightBlockAllowedByDigitalSignatures(height, block) + + +(** + * Pick the next height, for which there is a block. + *) +PickNextHeight(fetchedBlocks, height) == + LET largerHeights == { h \in DOMAIN fetchedBlocks: h > height } IN + IF largerHeights = ({} <: {Int}) + THEN -1 + ELSE CHOOSE h \in largerHeights: + \A h2 \in largerHeights: h <= h2 + + +(** + * Check, whether the target header matches at the secondary and primary. + *) +CompareLast == + /\ state = <<"Init", "SECONDARY">> + \* fetch a block from the secondary: + \* non-deterministically pick a block that matches the constraints + /\ \E latest \in BC!LightBlocks: + \* for the moment, we ignore the possibility of a timeout when fetching a block + /\ FetchLightBlockInto(IS_SECONDARY_CORRECT, latest, TARGET_HEIGHT) + /\ IF latest.header = fetchedLightBlocks1[TARGET_HEIGHT].header + THEN \* if the headers match, CreateEvidence is not called + /\ state' = <<"NoEvidence", "SECONDARY">> + \* save the retrieved block for further analysis + /\ fetchedLightBlocks2' = + [h \in (DOMAIN fetchedLightBlocks2) \union {TARGET_HEIGHT} |-> + IF h = TARGET_HEIGHT THEN latest ELSE fetchedLightBlocks2[h]] + /\ UNCHANGED <> + ELSE \* prepare the parameters for CreateEvidence + /\ commonHeight' = TRUSTED_HEIGHT + /\ nextHeightToTry' = PickNextHeight(fetchedLightBlocks1, TRUSTED_HEIGHT) + /\ state' = IF nextHeightToTry' >= 0 + THEN <<"CreateEvidence", "SECONDARY">> + ELSE <<"FaultyPeer", "SECONDARY">> + /\ UNCHANGED fetchedLightBlocks2 + + /\ UNCHANGED <> + + +\* the actual loop in CreateEvidence +CreateEvidence(peer, isPeerCorrect, refBlocks, targetBlocks) == + /\ state = <<"CreateEvidence", peer>> + \* precompute a possible result of light client verification for the secondary + \* we have to introduce HeightRange, because Apalache can only handle a..b + \* for constant a and b + /\ LET HeightRange == { h \in TRUSTED_HEIGHT..TARGET_HEIGHT: + commonHeight <= h /\ h <= nextHeightToTry } IN + \E HeightsRange \in SUBSET(HeightRange): + /\ commonHeight \in HeightsRange /\ nextHeightToTry \in HeightsRange + /\ InitLightBlocks(targetBlocks, HeightsRange) + \* As we have a non-deterministic scheduler, for every trace that has + \* an unverified block, there is a filtered trace that only has verified + \* blocks. This is a deep observation. + /\ \E result \in {"finishedSuccess", "finishedFailure"}: + LET targetStatus == [h \in HeightsRange |-> "StateVerified"] IN + \* call VerifyToTarget for (commonHeight, nextHeightToTry). + /\ LC!VerifyToTargetPost(blockchain, isPeerCorrect, + targetBlocks, targetStatus, + commonHeight, nextHeightToTry, result) + \* case 1: the peer has failed (or the trusting period has expired) + /\ \/ /\ result /= "finishedSuccess" + /\ state' = <<"FaultyPeer", peer>> + /\ UNCHANGED <> + \* case 2: success + \/ /\ result = "finishedSuccess" + /\ LET block1 == refBlocks[nextHeightToTry] IN + LET block2 == targetBlocks[nextHeightToTry] IN + IF block1.header /= block2.header + THEN \* the target blocks do not match + /\ state' = <<"FoundEvidence", peer>> + /\ evidences' = evidences \union + {[peer |-> peer, + conflictingBlock |-> block1, + commonHeight |-> commonHeight]} + /\ UNCHANGED <> + ELSE \* the target blocks match + /\ nextHeightToTry' = PickNextHeight(refBlocks, nextHeightToTry) + /\ commonHeight' = nextHeightToTry + /\ state' = IF nextHeightToTry' >= 0 + THEN state + ELSE <<"NoEvidence", peer>> + /\ UNCHANGED evidences + +SwitchToPrimary == + /\ state = <<"FoundEvidence", "SECONDARY">> + /\ nextHeightToTry' = PickNextHeight(fetchedLightBlocks2, commonHeight) + /\ state' = <<"CreateEvidence", "PRIMARY">> + /\ UNCHANGED <> + + +CreateEvidenceForSecondary == + /\ CreateEvidence("SECONDARY", IS_SECONDARY_CORRECT, + fetchedLightBlocks1, fetchedLightBlocks2') + /\ UNCHANGED <> + +CreateEvidenceForPrimary == + /\ CreateEvidence("PRIMARY", IS_PRIMARY_CORRECT, + fetchedLightBlocks2, + fetchedLightBlocks1b') + /\ UNCHANGED <> + +(* + The local and global clocks can be updated. They can also drift from each other. + Note that the local clock can actually go backwards in time. + However, it still stays in the drift envelope + of [refClock - REAL_CLOCK_DRIFT, refClock + REAL_CLOCK_DRIFT]. + *) +AdvanceClocks == + /\ \E tm \in Int: + tm >= refClock /\ refClock' = tm + /\ \E tm \in Int: + /\ tm >= localClock + /\ LC!IsLocalClockWithinDrift(tm, refClock') + /\ localClock' = tm + +(** + Execute AttackDetector for one secondary. + + [LCD-FUNC-DETECTOR.2::LOOP.1] + *) +Next == + /\ AdvanceClocks + /\ \/ CompareLast + \/ CreateEvidenceForSecondary + \/ SwitchToPrimary + \/ CreateEvidenceForPrimary + + +\* simple invariants to see the progress of the detector +NeverNoEvidence == state[1] /= "NoEvidence" +NeverFoundEvidence == state[1] /= "FoundEvidence" +NeverFaultyPeer == state[1] /= "FaultyPeer" +NeverCreateEvidence == state[1] /= "CreateEvidence" + +NeverFoundEvidencePrimary == state /= <<"FoundEvidence", "PRIMARY">> + +NeverReachTargetHeight == nextHeightToTry < TARGET_HEIGHT + +EvidenceWhenFaultyInv == + (state[1] = "FoundEvidence") => (~IS_PRIMARY_CORRECT \/ ~IS_SECONDARY_CORRECT) + +NoEvidenceForCorrectInv == + IS_PRIMARY_CORRECT /\ IS_SECONDARY_CORRECT => evidences = {} <: {ET} + +(** + * If we find an evidence by peer A, peer B has ineded given us a corrupted + * header following the common height. Also, we have a verification trace by peer A. + *) +CommonHeightOnEvidenceInv == + \A e \in evidences: + LET conflicting == e.conflictingBlock IN + LET conflictingHeader == conflicting.header IN + \* the evidence by suspectingPeer can be verified by suspectingPeer in one step + LET SoundEvidence(suspectingPeer, peerBlocks) == + \/ e.peer /= suspectingPeer + \* the conflicting block from another peer verifies against the common height + \/ /\ "SUCCESS" = + LC!ValidAndVerifiedUntimed(peerBlocks[e.commonHeight], conflicting) + \* and the headers of the same height by the two peers do not match + /\ peerBlocks[conflictingHeader.height].header /= conflictingHeader + IN + /\ SoundEvidence("PRIMARY", fetchedLightBlocks1b) + /\ SoundEvidence("SECONDARY", fetchedLightBlocks2) + +(** + * If the light client does not find an evidence, + * then there is no attack on the light client. + *) +AccuracyInv == + (LC!InTrustingPeriodLocal(fetchedLightBlocks1[TARGET_HEIGHT].header) + /\ state = <<"NoEvidence", "SECONDARY">>) + => + (fetchedLightBlocks1[TARGET_HEIGHT].header = blockchain[TARGET_HEIGHT] + /\ fetchedLightBlocks2[TARGET_HEIGHT].header = blockchain[TARGET_HEIGHT]) + +(** + * The primary reports a corrupted block at the target height. If the secondary is + * correct and the algorithm has terminated, we should get the evidence. + * This property is violated due to clock drift. VerifyToTarget may fail with + * the correct secondary within the trusting period (due to clock drift, locally + * we think that we are outside of the trusting period). + *) +PrecisionInvGrayZone == + (/\ fetchedLightBlocks1[TARGET_HEIGHT].header /= blockchain[TARGET_HEIGHT] + /\ BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) + /\ IS_SECONDARY_CORRECT + /\ IsTerminated) + => + evidences /= {} <: {ET} + +(** + * The primary reports a corrupted block at the target height. If the secondary is + * correct and the algorithm has terminated, we should get the evidence. + * This invariant does not fail, as we are using the local clock to check the trusting + * period. + *) +PrecisionInvLocal == + (/\ fetchedLightBlocks1[TARGET_HEIGHT].header /= blockchain[TARGET_HEIGHT] + /\ LC!InTrustingPeriodLocalSurely(blockchain[TRUSTED_HEIGHT]) + /\ IS_SECONDARY_CORRECT + /\ IsTerminated) + => + evidences /= {} <: {ET} + +==================================================================================== diff --git a/rust-spec/lightclient/detection/LCVerificationApi_003_draft.tla b/rust-spec/lightclient/detection/LCVerificationApi_003_draft.tla new file mode 100644 index 000000000..909eab92b --- /dev/null +++ b/rust-spec/lightclient/detection/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 <> 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) + + +================================================================================== diff --git a/rust-spec/lightclient/verification/002bmc-apalache-ok.csv b/rust-spec/lightclient/verification/002bmc-apalache-ok.csv new file mode 100644 index 000000000..eb26aa89e --- /dev/null +++ b/rust-spec/lightclient/verification/002bmc-apalache-ok.csv @@ -0,0 +1,55 @@ +no;filename;tool;timeout;init;inv;next;args +1;MC4_3_correct.tla;apalache;1h;;TargetHeightOnSuccessInv;;--length=5 +2;MC4_3_correct.tla;apalache;1h;;StoredHeadersAreVerifiedOrNotTrustedInv;;--length=5 +3;MC4_3_correct.tla;apalache;1h;;CorrectnessInv;;--length=5 +4;MC4_3_correct.tla;apalache;1h;;NoTrustOnFaultyBlockInv;;--length=5 +5;MC4_3_correct.tla;apalache;1h;;ProofOfChainOfTrustInv;;--length=5 +6;MC4_3_correct.tla;apalache;1h;;NoFailedBlocksOnSuccessInv;;--length=5 +7;MC4_3_correct.tla;apalache;1h;;Complexity;;--length=5 +8;MC4_3_correct.tla;apalache;1h;;ApiPostInv;;--length=5 +9;MC4_4_correct.tla;apalache;1h;;TargetHeightOnSuccessInv;;--length=7 +10;MC4_4_correct.tla;apalache;1h;;CorrectnessInv;;--length=7 +11;MC4_4_correct.tla;apalache;1h;;NoTrustOnFaultyBlockInv;;--length=7 +12;MC4_4_correct.tla;apalache;1h;;ProofOfChainOfTrustInv;;--length=7 +13;MC4_4_correct.tla;apalache;1h;;NoFailedBlocksOnSuccessInv;;--length=7 +14;MC4_4_correct.tla;apalache;1h;;Complexity;;--length=7 +15;MC4_4_correct.tla;apalache;1h;;ApiPostInv;;--length=7 +16;MC4_5_correct.tla;apalache;1h;;TargetHeightOnSuccessInv;;--length=11 +17;MC4_5_correct.tla;apalache;1h;;CorrectnessInv;;--length=11 +18;MC4_5_correct.tla;apalache;1h;;NoTrustOnFaultyBlockInv;;--length=11 +19;MC4_5_correct.tla;apalache;1h;;ProofOfChainOfTrustInv;;--length=11 +20;MC4_5_correct.tla;apalache;1h;;NoFailedBlocksOnSuccessInv;;--length=11 +21;MC4_5_correct.tla;apalache;1h;;Complexity;;--length=11 +22;MC4_5_correct.tla;apalache;1h;;ApiPostInv;;--length=11 +23;MC5_5_correct.tla;apalache;1h;;TargetHeightOnSuccessInv;;--length=11 +24;MC5_5_correct.tla;apalache;1h;;CorrectnessInv;;--length=11 +25;MC5_5_correct.tla;apalache;1h;;NoTrustOnFaultyBlockInv;;--length=11 +26;MC5_5_correct.tla;apalache;1h;;ProofOfChainOfTrustInv;;--length=11 +27;MC5_5_correct.tla;apalache;1h;;NoFailedBlocksOnSuccessInv;;--length=11 +28;MC5_5_correct.tla;apalache;1h;;Complexity;;--length=11 +29;MC5_5_correct.tla;apalache;1h;;ApiPostInv;;--length=11 +30;MC4_3_faulty.tla;apalache;1h;;TargetHeightOnSuccessInv;;--length=5 +31;MC4_3_faulty.tla;apalache;1h;;StoredHeadersAreVerifiedOrNotTrustedInv;;--length=5 +32;MC4_3_faulty.tla;apalache;1h;;CorrectnessInv;;--length=5 +33;MC4_3_faulty.tla;apalache;1h;;NoTrustOnFaultyBlockInv;;--length=5 +34;MC4_3_faulty.tla;apalache;1h;;ProofOfChainOfTrustInv;;--length=5 +35;MC4_3_faulty.tla;apalache;1h;;NoFailedBlocksOnSuccessInv;;--length=5 +36;MC4_3_faulty.tla;apalache;1h;;Complexity;;--length=5 +37;MC4_3_faulty.tla;apalache;1h;;ApiPostInv;;--length=5 +38;MC4_4_faulty.tla;apalache;1h;;TargetHeightOnSuccessInv;;--length=7 +39;MC4_4_faulty.tla;apalache;1h;;StoredHeadersAreVerifiedOrNotTrustedInv;;--length=7 +40;MC4_4_faulty.tla;apalache;1h;;CorrectnessInv;;--length=7 +41;MC4_4_faulty.tla;apalache;1h;;NoTrustOnFaultyBlockInv;;--length=7 +42;MC4_4_faulty.tla;apalache;1h;;ProofOfChainOfTrustInv;;--length=7 +43;MC4_4_faulty.tla;apalache;1h;;NoFailedBlocksOnSuccessInv;;--length=7 +44;MC4_4_faulty.tla;apalache;1h;;Complexity;;--length=7 +45;MC4_4_faulty.tla;apalache;1h;;ApiPostInv;;--length=7 +46;MC4_5_faulty.tla;apalache;1h;;TargetHeightOnSuccessInv;;--length=11 +47;MC4_5_faulty.tla;apalache;1h;;StoredHeadersAreVerifiedOrNotTrustedInv;;--length=11 +48;MC4_5_faulty.tla;apalache;1h;;CorrectnessInv;;--length=11 +49;MC4_5_faulty.tla;apalache;1h;;NoTrustOnFaultyBlockInv;;--length=11 +50;MC4_5_faulty.tla;apalache;1h;;ProofOfChainOfTrustInv;;--length=11 +51;MC4_5_faulty.tla;apalache;1h;;NoFailedBlocksOnSuccessInv;;--length=11 +52;MC4_5_faulty.tla;apalache;1h;;Complexity;;--length=11 +53;MC4_5_faulty.tla;apalache;1h;;ApiPostInv;;--length=11 + diff --git a/rust-spec/lightclient/verification/003bmc-apalache-error.csv b/rust-spec/lightclient/verification/003bmc-apalache-error.csv new file mode 100644 index 000000000..ad5ef9654 --- /dev/null +++ b/rust-spec/lightclient/verification/003bmc-apalache-error.csv @@ -0,0 +1,45 @@ +no;filename;tool;timeout;init;inv;next;args +1;MC4_3_correct.tla;apalache;1h;;StoredHeadersAreVerifiedInv;;--length=5 +2;MC4_3_correct.tla;apalache;1h;;PositiveBeforeTrustedHeaderExpires;;--length=5 +3;MC4_3_correct.tla;apalache;1h;;CorrectPrimaryAndTimeliness;;--length=5 +4;MC4_3_correct.tla;apalache;1h;;PrecisionInv;;--length=5 +5;MC4_3_correct.tla;apalache;1h;;PrecisionBuggyInv;;--length=5 +6;MC4_3_correct.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustGlobal;;--length=5 +7;MC4_3_correct.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustLocal;;--length=5 +8;MC4_4_correct.tla;apalache;1h;;StoredHeadersAreVerifiedInv;;--length=7 +9;MC4_4_correct.tla;apalache;1h;;PositiveBeforeTrustedHeaderExpires;;--length=7 +10;MC4_4_correct.tla;apalache;1h;;CorrectPrimaryAndTimeliness;;--length=7 +11;MC4_4_correct.tla;apalache;1h;;PrecisionInv;;--length=7 +12;MC4_4_correct.tla;apalache;1h;;PrecisionBuggyInv;;--length=7 +13;MC4_4_correct.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustGlobal;;--length=7 +14;MC4_4_correct.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustLocal;;--length=7 +15;MC4_5_correct.tla;apalache;1h;;StoredHeadersAreVerifiedInv;;--length=11 +16;MC4_5_correct.tla;apalache;1h;;PositiveBeforeTrustedHeaderExpires;;--length=11 +17;MC4_5_correct.tla;apalache;1h;;CorrectPrimaryAndTimeliness;;--length=11 +18;MC4_5_correct.tla;apalache;1h;;PrecisionInv;;--length=11 +19;MC4_5_correct.tla;apalache;1h;;PrecisionBuggyInv;;--length=11 +20;MC4_5_correct.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustGlobal;;--length=11 +21;MC4_5_correct.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustLocal;;--length=11 +22;MC4_5_correct.tla;apalache;1h;;StoredHeadersAreVerifiedOrNotTrustedInv;;--length=11 +23;MC4_3_faulty.tla;apalache;1h;;StoredHeadersAreVerifiedInv;;--length=5 +24;MC4_3_faulty.tla;apalache;1h;;PositiveBeforeTrustedHeaderExpires;;--length=5 +25;MC4_3_faulty.tla;apalache;1h;;CorrectPrimaryAndTimeliness;;--length=5 +26;MC4_3_faulty.tla;apalache;1h;;PrecisionInv;;--length=5 +27;MC4_3_faulty.tla;apalache;1h;;PrecisionBuggyInv;;--length=5 +28;MC4_3_faulty.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustGlobal;;--length=5 +29;MC4_3_faulty.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustLocal;;--length=5 +30;MC4_4_faulty.tla;apalache;1h;;StoredHeadersAreVerifiedInv;;--length=7 +31;MC4_4_faulty.tla;apalache;1h;;PositiveBeforeTrustedHeaderExpires;;--length=7 +32;MC4_4_faulty.tla;apalache;1h;;CorrectPrimaryAndTimeliness;;--length=7 +33;MC4_4_faulty.tla;apalache;1h;;PrecisionInv;;--length=7 +34;MC4_4_faulty.tla;apalache;1h;;PrecisionBuggyInv;;--length=7 +35;MC4_4_faulty.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustGlobal;;--length=7 +36;MC4_4_faulty.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustLocal;;--length=7 +37;MC4_5_faulty.tla;apalache;1h;;StoredHeadersAreVerifiedInv;;--length=11 +38;MC4_5_faulty.tla;apalache;1h;;PositiveBeforeTrustedHeaderExpires;;--length=11 +39;MC4_5_faulty.tla;apalache;1h;;CorrectPrimaryAndTimeliness;;--length=11 +40;MC4_5_faulty.tla;apalache;1h;;PrecisionInv;;--length=11 +41;MC4_5_faulty.tla;apalache;1h;;PrecisionBuggyInv;;--length=11 +42;MC4_5_faulty.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustGlobal;;--length=11 +43;MC4_5_faulty.tla;apalache;1h;;SuccessOnCorrectPrimaryAndChainOfTrustLocal;;--length=11 +44;MC4_5_faulty.tla;apalache;1h;;StoredHeadersAreVerifiedOrNotTrustedInv;;--length=11 diff --git a/rust-spec/lightclient/verification/004bmc-apalache-ok.csv b/rust-spec/lightclient/verification/004bmc-apalache-ok.csv new file mode 100644 index 000000000..bf4f53ea2 --- /dev/null +++ b/rust-spec/lightclient/verification/004bmc-apalache-ok.csv @@ -0,0 +1,10 @@ +no;filename;tool;timeout;init;inv;next;args +1;LCD_MC3_3_faulty.tla;apalache;1h;;CommonHeightOnEvidenceInv;;--length=10 +2;LCD_MC3_3_faulty.tla;apalache;1h;;AccuracyInv;;--length=10 +3;LCD_MC3_3_faulty.tla;apalache;1h;;PrecisionInvLocal;;--length=10 +4;LCD_MC3_4_faulty.tla;apalache;1h;;CommonHeightOnEvidenceInv;;--length=10 +5;LCD_MC3_4_faulty.tla;apalache;1h;;AccuracyInv;;--length=10 +6;LCD_MC3_4_faulty.tla;apalache;1h;;PrecisionInvLocal;;--length=10 +7;LCD_MC4_4_faulty.tla;apalache;1h;;CommonHeightOnEvidenceInv;;--length=10 +8;LCD_MC4_4_faulty.tla;apalache;1h;;AccuracyInv;;--length=10 +9;LCD_MC4_4_faulty.tla;apalache;1h;;PrecisionInvLocal;;--length=10 diff --git a/rust-spec/lightclient/verification/005bmc-apalache-error.csv b/rust-spec/lightclient/verification/005bmc-apalache-error.csv new file mode 100644 index 000000000..1b9dd05ca --- /dev/null +++ b/rust-spec/lightclient/verification/005bmc-apalache-error.csv @@ -0,0 +1,4 @@ +no;filename;tool;timeout;init;inv;next;args +1;LCD_MC3_3_faulty.tla;apalache;1h;;PrecisionInvGrayZone;;--length=10 +2;LCD_MC3_4_faulty.tla;apalache;1h;;PrecisionInvGrayZone;;--length=10 +3;LCD_MC4_4_faulty.tla;apalache;1h;;PrecisionInvGrayZone;;--length=10 diff --git a/rust-spec/lightclient/verification/Blockchain_003_draft.tla b/rust-spec/lightclient/verification/Blockchain_003_draft.tla index e80fbae56..2b37c1b18 100644 --- a/rust-spec/lightclient/verification/Blockchain_003_draft.tla +++ b/rust-spec/lightclient/verification/Blockchain_003_draft.tla @@ -44,8 +44,8 @@ BlockHeaders == [ LightBlocks == [header: BlockHeaders, Commits: Commits] VARIABLES - now, - (* the current global time in integer units *) + 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 @@ -54,7 +54,7 @@ VARIABLES connect using a different id. *) (* all variables, to be used with UNCHANGED *) -vars == <> +vars == <> (* The set of all correct nodes in a state *) Corr == AllNodes \ Faulty @@ -75,7 +75,7 @@ LBT == [header |-> BT, Commits |-> {NT}] (* the header is still within the trusting period *) InTrustingPeriod(header) == - now < header.time + TRUSTING_PERIOD + refClock < header.time + TRUSTING_PERIOD (* Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes @@ -128,8 +128,8 @@ InitToHeight(pMaxFaultyRatioExclusive) == \* 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] + \* 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 @@ -155,7 +155,7 @@ InitToHeight(pMaxFaultyRatioExclusive) == Advance the clock by zero or more time units. *) AdvanceTime == - \E tm \in Int: tm >= now /\ now' = tm + /\ \E tm \in Int: tm >= refClock /\ refClock' = tm /\ UNCHANGED <> ============================================================================= diff --git a/rust-spec/lightclient/verification/LCVerificationApi_003_draft.tla b/rust-spec/lightclient/verification/LCVerificationApi_003_draft.tla new file mode 100644 index 000000000..909eab92b --- /dev/null +++ b/rust-spec/lightclient/verification/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 <> 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) + + +================================================================================== diff --git a/rust-spec/lightclient/verification/Lightclient_003_draft.tla b/rust-spec/lightclient/verification/Lightclient_003_draft.tla index 873f76d30..e17a88491 100644 --- a/rust-spec/lightclient/verification/Lightclient_003_draft.tla +++ b/rust-spec/lightclient/verification/Lightclient_003_draft.tla @@ -1,6 +1,7 @@ -------------------------- MODULE Lightclient_003_draft ---------------------------- (** - * A state-machine specification of the lite client, following the English spec: + * A state-machine specification of the lite client verification, + * following the English spec: * * https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md *) @@ -15,6 +16,11 @@ CONSTANTS (* an index of the block header that the light client tries to verify *) 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) *) IS_PRIMARY_CORRECT, (* is primary correct? *) FAULTY_RATIO @@ -22,6 +28,7 @@ CONSTANTS from above (exclusive). Tendermint security model prescribes 1 / 3. *) VARIABLES (* see TypeOK below for the variable types *) + localClock, (* the local clock of the light client *) 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 *) @@ -33,25 +40,26 @@ VARIABLES latestVerified (* the latest verified block *) (* the variables of the lite client *) -lcvars == <> +lcvars == <> (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict -InitMonitor(verified, current, now, verdict) == +InitMonitor(verified, current, pLocalClock, verdict) == /\ prevVerified = verified /\ prevCurrent = current - /\ prevNow = now + /\ prevLocalClock = pLocalClock /\ prevVerdict = verdict -NextMonitor(verified, current, now, verdict) == +NextMonitor(verified, current, pLocalClock, verdict) == /\ prevVerified' = verified /\ prevCurrent' = current - /\ prevNow' = now + /\ prevLocalClock' = pLocalClock /\ prevVerdict' = verdict @@ -63,10 +71,10 @@ CONSTANTS (* 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 +VARIABLES refClock, blockchain, Faulty \* All the variables of Blockchain. For some reason, BC!vars does not work -bcvars == <> +bcvars == <> (* Create an instance of Blockchain. We could write EXTENDS Blockchain, but then all the constants and state variables @@ -75,7 +83,7 @@ bcvars == <> ULTIMATE_HEIGHT == TARGET_HEIGHT + 1 BC == INSTANCE Blockchain_003_draft WITH - now <- now, blockchain <- blockchain, Faulty <- Faulty + refClock <- refClock, blockchain <- blockchain, Faulty <- Faulty (************************** Lite client ************************************) @@ -85,69 +93,17 @@ 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) - *) +\* The verification functions are implemented in the API +API == INSTANCE LCVerificationApi_003_draft -(** - * 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 == + /\ \E tm \in Int: + tm >= 0 /\ API!IsLocalClockWithinDrift(tm, refClock) /\ localClock = tm /\ state = "working" /\ nextHeight = TARGET_HEIGHT /\ nprobes = 0 \* no tests have been done so far @@ -160,7 +116,7 @@ LCInit == /\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"] \* the latest verified block the the trusted block /\ latestVerified = trustedLightBlock - /\ InitMonitor(trustedLightBlock, trustedLightBlock, now, "SUCCESS") + /\ InitMonitor(trustedLightBlock, trustedLightBlock, localClock, "SUCCESS") \* block should contain a copy of the block from the reference chain, with a matching commit CopyLightBlockFromChain(block, height) == @@ -232,8 +188,8 @@ VerifyToTargetLoop == \* 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) /\ + /\ LET verdict == API!ValidAndVerified(latestVerified, current, TRUE) IN + NextMonitor(latestVerified, current, localClock, verdict) /\ \* Decide whether/how to continue CASE verdict = "SUCCESS" -> /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified") @@ -272,7 +228,22 @@ VerifyToTargetDone == /\ latestVerified.header.height >= TARGET_HEIGHT /\ state' = "finishedSuccess" /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> + +(* + The local and global clocks can be updated. They can also drift from each other. + Note that the local clock can actually go backwards in time. + However, it still stays in the drift envelope + of [refClock - REAL_CLOCK_DRIFT, refClock + REAL_CLOCK_DRIFT]. + *) +AdvanceClocks == + /\ BC!AdvanceTime + /\ \E tm \in Int: + /\ tm >= 0 + /\ API!IsLocalClockWithinDrift(tm, refClock') + /\ localClock' = tm + \* if you like the clock to always grow monotonically, uncomment the next line: + \*/\ localClock' > localClock (********************* Lite client + Blockchain *******************) Init == @@ -290,11 +261,13 @@ Init == Next == /\ state = "working" /\ VerifyToTargetLoop \/ VerifyToTargetDone - /\ BC!AdvanceTime \* the global clock is advanced by zero or more time units + /\ AdvanceClocks (************************* Types ******************************************) TypeOK == /\ state \in States + /\ localClock \in Nat + /\ refClock \in Nat /\ nextHeight \in HEIGHTS /\ latestVerified \in BC!LightBlocks /\ \E HS \in SUBSET HEIGHTS: @@ -316,7 +289,6 @@ NeverFinishNegative == \* 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" @@ -324,6 +296,15 @@ NeverFinishNegativeWhenTrusted == NeverFinishPositive == state /= "finishedSuccess" + +(** + Check that the target height has been reached upon successful termination. + *) +TargetHeightOnSuccessInv == + state = "finishedSuccess" => + /\ TARGET_HEIGHT \in DOMAIN fetchedLightBlocks + /\ lightBlockStatus[TARGET_HEIGHT] = "StateVerified" + (** Correctness states that all the obtained headers are exactly like in the blockchain. @@ -338,7 +319,8 @@ CorrectnessInv == fetchedLightBlocks[h].header = blockchain[h] (** - + No faulty block was used to construct a proof. This invariant holds, + only if FAULTY_RATIO < 1/3. *) NoTrustOnFaultyBlockInv == (state = "finishedSuccess" @@ -358,11 +340,16 @@ StoredHeadersAreVerifiedInv == \/ \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]) + \/ "SUCCESS" = API!ValidAndVerified(fetchedLightBlocks[lh], + fetchedLightBlocks[rh], FALSE) -\* An improved version of StoredHeadersAreSound, assuming that a header may be not trusted. +\* An improved version of StoredHeadersAreVerifiedInv, +\* 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. +\* This property is violated under two conditions: +\* (1) the primary is faulty and there are at least 4 blocks, +\* (2) the primary is correct and there are at least 5 blocks. StoredHeadersAreVerifiedOrNotTrustedInv == state = "finishedSuccess" => @@ -372,14 +359,15 @@ StoredHeadersAreVerifiedOrNotTrustedInv == \/ \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]) + \/ "SUCCESS" = API!ValidAndVerified(fetchedLightBlocks[lh], + fetchedLightBlocks[rh], FALSE) \* or the left header is outside the trusting period, so no guarantees - \/ ~BC!InTrustingPeriod(fetchedLightBlocks[lh].header) + \/ ~API!InTrustingPeriodLocal(fetchedLightBlocks[lh].header) (** * An improved version of StoredHeadersAreSoundOrNotTrusted, * checking the property only for the verified headers. - * This invariant holds true. + * This invariant holds true if CLOCK_DRIFT <= REAL_CLOCK_DRIFT. *) ProofOfChainOfTrustInv == state = "finishedSuccess" @@ -393,9 +381,10 @@ ProofOfChainOfTrustInv == \/ \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)) + \/ ~(API!InTrustingPeriodLocal(fetchedLightBlocks[lh].header)) \* or we can verify the right one using the left one - \/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh]) + \/ "SUCCESS" = API!ValidAndVerified(fetchedLightBlocks[lh], + fetchedLightBlocks[rh], FALSE) (** * When the light client terminates, there are no failed blocks. (Otherwise, someone lied to us.) @@ -409,10 +398,12 @@ NoFailedBlocksOnSuccessInv == \* 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]) + (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" +\* then whenever the algorithm terminates, it reports "success". +\* This property fails. CorrectPrimaryAndTimeliness == (BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) /\ state /= "working" /\ IS_PRIMARY_CORRECT) => @@ -421,10 +412,25 @@ CorrectPrimaryAndTimeliness == (** If the primary is correct and there is a trusted block that has not expired, then whenever the algorithm terminates, it reports "success". + This property only holds true, if the local clock is always growing monotonically. + If the local clock can go backwards in the envelope + [refClock - CLOCK_DRIFT, refClock + CLOCK_DRIFT], then the property fails. [LCV-DIST-LIVE.1::SUCCESS-CORR-PRIMARY-CHAIN-OF-TRUST.1] *) -SuccessOnCorrectPrimaryAndChainOfTrust == +SuccessOnCorrectPrimaryAndChainOfTrustLocal == + (\E h \in DOMAIN fetchedLightBlocks: + /\ lightBlockStatus[h] = "StateVerified" + /\ API!InTrustingPeriodLocal(blockchain[h]) + /\ state /= "working" /\ IS_PRIMARY_CORRECT) => + state = "finishedSuccess" + +(** + Similar to SuccessOnCorrectPrimaryAndChainOfTrust, but using the blockchain clock. + It fails because the local clock of the client drifted away, so it rejects a block + that has not expired yet (according to the local clock). + *) +SuccessOnCorrectPrimaryAndChainOfTrustGlobal == (\E h \in DOMAIN fetchedLightBlocks: lightBlockStatus[h] = "StateVerified" /\ BC!InTrustingPeriod(blockchain[h]) /\ state /= "working" /\ IS_PRIMARY_CORRECT) => @@ -439,6 +445,8 @@ SuccessOnCorrectPrimaryAndChainOfTrust == \* 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. +\* +\* This property holds only when CLOCK_DRIFT = 0 and REAL_CLOCK_DRIFT = 0. PrecisionInv == (state = "finishedFailure") => \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period @@ -464,6 +472,15 @@ Complexity == state /= "working" => (2 * nprobes <= N * (N - 1)) +(** + If the light client has terminated, then the expected postcondition holds true. + *) +ApiPostInv == + state /= "working" => + API!VerifyToTargetPost(blockchain, IS_PRIMARY_CORRECT, + fetchedLightBlocks, lightBlockStatus, + TRUSTED_HEIGHT, TARGET_HEIGHT, state) + (* We omit termination, as the algorithm deadlocks in the end. So termination can be demonstrated by finding a deadlock. diff --git a/rust-spec/lightclient/verification/MC4_3_correct.tla b/rust-spec/lightclient/verification/MC4_3_correct.tla index 534f9963e..a27d8de05 100644 --- a/rust-spec/lightclient/verification/MC4_3_correct.tla +++ b/rust-spec/lightclient/verification/MC4_3_correct.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 3 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == TRUE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, nprobes, - now, blockchain, Faulty + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC4_3_faulty.tla b/rust-spec/lightclient/verification/MC4_3_faulty.tla index ae82cb7e7..74b278900 100644 --- a/rust-spec/lightclient/verification/MC4_3_faulty.tla +++ b/rust-spec/lightclient/verification/MC4_3_faulty.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 3 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, nprobes, - now, blockchain, Faulty + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC4_4_correct.tla b/rust-spec/lightclient/verification/MC4_4_correct.tla new file mode 100644 index 000000000..0a8d96b59 --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_4_correct.tla @@ -0,0 +1,26 @@ +------------------------- MODULE MC4_4_correct --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 4 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == TRUE +FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty + +(* the light client previous state components, used for monitoring *) +VARIABLES + prevVerified, + prevCurrent, + prevLocalClock, + prevVerdict + +INSTANCE Lightclient_003_draft +============================================================================ diff --git a/rust-spec/lightclient/verification/MC4_4_correct_drifted.tla b/rust-spec/lightclient/verification/MC4_4_correct_drifted.tla new file mode 100644 index 000000000..7fefe349e --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_4_correct_drifted.tla @@ -0,0 +1,26 @@ +---------------------- MODULE MC4_4_correct_drifted --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 4 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 30 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == TRUE +FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty + +(* the light client previous state components, used for monitoring *) +VARIABLES + prevVerified, + prevCurrent, + prevLocalClock, + prevVerdict + +INSTANCE Lightclient_003_draft +============================================================================== diff --git a/rust-spec/lightclient/verification/MC4_4_faulty.tla b/rust-spec/lightclient/verification/MC4_4_faulty.tla index 8836a1359..167fa61fb 100644 --- a/rust-spec/lightclient/verification/MC4_4_faulty.tla +++ b/rust-spec/lightclient/verification/MC4_4_faulty.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 4 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, nprobes, - now, blockchain, Faulty + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC4_4_faulty_drifted.tla b/rust-spec/lightclient/verification/MC4_4_faulty_drifted.tla new file mode 100644 index 000000000..e37c3cb40 --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_4_faulty_drifted.tla @@ -0,0 +1,26 @@ +---------------------- MODULE MC4_4_faulty_drifted --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 4 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 30 \* how much the local clock is actually drifting +IS_PRIMARY_CORRECT == FALSE +FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty + +(* the light client previous state components, used for monitoring *) +VARIABLES + prevVerified, + prevCurrent, + prevLocalClock, + prevVerdict + +INSTANCE Lightclient_003_draft +============================================================================== diff --git a/rust-spec/lightclient/verification/MC4_5_correct.tla b/rust-spec/lightclient/verification/MC4_5_correct.tla index dd1b1298a..cffb22cc8 100644 --- a/rust-spec/lightclient/verification/MC4_5_correct.tla +++ b/rust-spec/lightclient/verification/MC4_5_correct.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 5 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == TRUE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, nprobes, - now, blockchain, Faulty + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC4_5_faulty.tla b/rust-spec/lightclient/verification/MC4_5_faulty.tla index a7a5ca8f8..3d3a00290 100644 --- a/rust-spec/lightclient/verification/MC4_5_faulty.tla +++ b/rust-spec/lightclient/verification/MC4_5_faulty.tla @@ -4,19 +4,22 @@ 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 +IS_PRICLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting +MARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES - state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, - latestVerified, nprobes, - now, blockchain, Faulty + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC4_6_faulty.tla b/rust-spec/lightclient/verification/MC4_6_faulty.tla index 14eced4d9..64f164854 100644 --- a/rust-spec/lightclient/verification/MC4_6_faulty.tla +++ b/rust-spec/lightclient/verification/MC4_6_faulty.tla @@ -4,19 +4,22 @@ 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 +IS_PRCLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting +IMARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, nprobes, - now, blockchain, Faulty + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC4_7_faulty.tla b/rust-spec/lightclient/verification/MC4_7_faulty.tla index d6214b868..dc6a94eb1 100644 --- a/rust-spec/lightclient/verification/MC4_7_faulty.tla +++ b/rust-spec/lightclient/verification/MC4_7_faulty.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 7 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, nprobes, - now, blockchain, Faulty + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC5_5_correct.tla b/rust-spec/lightclient/verification/MC5_5_correct.tla index f78c60eb5..00b4151f7 100644 --- a/rust-spec/lightclient/verification/MC5_5_correct.tla +++ b/rust-spec/lightclient/verification/MC5_5_correct.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4", "n5"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 5 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == TRUE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES - state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, - latestVerified, nprobes, - now, blockchain, Faulty + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC5_5_correct_peer_two_thirds_faulty.tla b/rust-spec/lightclient/verification/MC5_5_correct_peer_two_thirds_faulty.tla index 41b906660..d4212032f 100644 --- a/rust-spec/lightclient/verification/MC5_5_correct_peer_two_thirds_faulty.tla +++ b/rust-spec/lightclient/verification/MC5_5_correct_peer_two_thirds_faulty.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4", "n5"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 5 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == TRUE FAULTY_RATIO == <<2, 3>> \* < 1 / 3 faulty validators VARIABLES - state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, - latestVerified, nprobes, - now, blockchain, Faulty + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC5_5_faulty.tla b/rust-spec/lightclient/verification/MC5_5_faulty.tla index 5a124959f..f63d175a1 100644 --- a/rust-spec/lightclient/verification/MC5_5_faulty.tla +++ b/rust-spec/lightclient/verification/MC5_5_faulty.tla @@ -1,22 +1,25 @@ ------------------ MODULE MC5_5_faulty_peers_two_thirds_faulty --------------------- +----------------- 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 :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<2, 3>> \* < 1 / 3 faulty validators VARIABLES - state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, - latestVerified, nprobes, - now, blockchain, Faulty + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC5_5_faulty_peer_two_thirds_faulty.tla b/rust-spec/lightclient/verification/MC5_5_faulty_peer_two_thirds_faulty.tla index 9dadbcb31..ef9974d06 100644 --- a/rust-spec/lightclient/verification/MC5_5_faulty_peer_two_thirds_faulty.tla +++ b/rust-spec/lightclient/verification/MC5_5_faulty_peer_two_thirds_faulty.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4", "n5"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 5 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<2, 3>> \* < 2 / 3 faulty validators VARIABLES - state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, - latestVerified, nprobes, - now, blockchain, Faulty + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC5_7_faulty.tla b/rust-spec/lightclient/verification/MC5_7_faulty.tla index e8cde75e6..63461b0c8 100644 --- a/rust-spec/lightclient/verification/MC5_7_faulty.tla +++ b/rust-spec/lightclient/verification/MC5_7_faulty.tla @@ -4,19 +4,22 @@ AllNodes == {"n1", "n2", "n3", "n4", "n5"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 7 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES - state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, - latestVerified, nprobes, - now, blockchain, Faulty + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC7_5_faulty.tla b/rust-spec/lightclient/verification/MC7_5_faulty.tla index 855415b26..860f9c0aa 100644 --- a/rust-spec/lightclient/verification/MC7_5_faulty.tla +++ b/rust-spec/lightclient/verification/MC7_5_faulty.tla @@ -4,19 +4,22 @@ 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 :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES - state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, - latestVerified, nprobes, - now, blockchain, Faulty + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft diff --git a/rust-spec/lightclient/verification/MC7_7_faulty.tla b/rust-spec/lightclient/verification/MC7_7_faulty.tla index ea6fcec1f..79e328f14 100644 --- a/rust-spec/lightclient/verification/MC7_7_faulty.tla +++ b/rust-spec/lightclient/verification/MC7_7_faulty.tla @@ -4,19 +4,22 @@ 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 :-) +CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting +REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == FALSE FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators VARIABLES state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, nprobes, - now, blockchain, Faulty + localClock, + refClock, blockchain, Faulty (* the light client previous state components, used for monitoring *) VARIABLES prevVerified, prevCurrent, - prevNow, + prevLocalClock, prevVerdict INSTANCE Lightclient_003_draft