You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
373 lines
16 KiB
373 lines
16 KiB
-------------------------- 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 <<a, b>> 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 == <<state, blockchain, localClock, refClock, Faulty,
|
|
fetchedLightBlocks1, fetchedLightBlocks2, fetchedLightBlocks1b,
|
|
commonHeight, nextHeightToTry, evidences >>
|
|
|
|
\* (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 <<commonHeight, nextHeightToTry>>
|
|
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 <<blockchain, Faulty,
|
|
fetchedLightBlocks1, fetchedLightBlocks1b, evidences>>
|
|
|
|
|
|
\* 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 <<commonHeight, nextHeightToTry, evidences>>
|
|
\* 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 <<commonHeight, nextHeightToTry>>
|
|
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 <<blockchain, refClock, Faulty, localClock,
|
|
fetchedLightBlocks1, fetchedLightBlocks2, fetchedLightBlocks1b,
|
|
commonHeight, evidences >>
|
|
|
|
|
|
CreateEvidenceForSecondary ==
|
|
/\ CreateEvidence("SECONDARY", IS_SECONDARY_CORRECT,
|
|
fetchedLightBlocks1, fetchedLightBlocks2')
|
|
/\ UNCHANGED <<blockchain, refClock, Faulty, localClock,
|
|
fetchedLightBlocks1, fetchedLightBlocks1b>>
|
|
|
|
CreateEvidenceForPrimary ==
|
|
/\ CreateEvidence("PRIMARY", IS_PRIMARY_CORRECT,
|
|
fetchedLightBlocks2,
|
|
fetchedLightBlocks1b')
|
|
/\ UNCHANGED <<blockchain, Faulty,
|
|
fetchedLightBlocks1, fetchedLightBlocks2>>
|
|
|
|
(*
|
|
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}
|
|
|
|
====================================================================================
|