mirror of
https://github.com/tendermint/tendermint.git
synced 2026-09-19 14:34:17 +00:00
spec: merge rust-spec (#252)
This commit is contained in:
Marko
@@ -0,0 +1,49 @@
|
||||
no,filename,tool,timeout,init,inv,next,args
|
||||
1,MC4_3_correct.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30
|
||||
2,MC4_3_correct.tla,apalache,1h,,CorrectnessInv,,--length=30
|
||||
3,MC4_3_correct.tla,apalache,1h,,PrecisionInv,,--length=30
|
||||
4,MC4_3_correct.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30
|
||||
5,MC4_3_correct.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30
|
||||
6,MC4_3_correct.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30
|
||||
7,MC4_3_correct.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30
|
||||
8,MC4_3_correct.tla,apalache,1h,,Complexity,,--length=30
|
||||
9,MC4_3_faulty.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30
|
||||
10,MC4_3_faulty.tla,apalache,1h,,CorrectnessInv,,--length=30
|
||||
11,MC4_3_faulty.tla,apalache,1h,,PrecisionInv,,--length=30
|
||||
12,MC4_3_faulty.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30
|
||||
13,MC4_3_faulty.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30
|
||||
14,MC4_3_faulty.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30
|
||||
15,MC4_3_faulty.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30
|
||||
16,MC4_3_faulty.tla,apalache,1h,,Complexity,,--length=30
|
||||
17,MC5_5_correct.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30
|
||||
18,MC5_5_correct.tla,apalache,1h,,CorrectnessInv,,--length=30
|
||||
19,MC5_5_correct.tla,apalache,1h,,PrecisionInv,,--length=30
|
||||
20,MC5_5_correct.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30
|
||||
21,MC5_5_correct.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30
|
||||
22,MC5_5_correct.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30
|
||||
23,MC5_5_correct.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30
|
||||
24,MC5_5_correct.tla,apalache,1h,,Complexity,,--length=30
|
||||
25,MC5_5_faulty.tla,apalache,1h,,PositiveBeforeTrustedHeaderExpires,,--length=30
|
||||
26,MC5_5_faulty.tla,apalache,1h,,CorrectnessInv,,--length=30
|
||||
27,MC5_5_faulty.tla,apalache,1h,,PrecisionInv,,--length=30
|
||||
28,MC5_5_faulty.tla,apalache,1h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30
|
||||
29,MC5_5_faulty.tla,apalache,1h,,NoFailedBlocksOnSuccessInv,,--length=30
|
||||
30,MC5_5_faulty.tla,apalache,1h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30
|
||||
31,MC5_5_faulty.tla,apalache,1h,,CorrectPrimaryAndTimeliness,,--length=30
|
||||
32,MC5_5_faulty.tla,apalache,1h,,Complexity,,--length=30
|
||||
33,MC7_5_faulty.tla,apalache,10h,,PositiveBeforeTrustedHeaderExpires,,--length=30
|
||||
34,MC7_5_faulty.tla,apalache,10h,,CorrectnessInv,,--length=30
|
||||
35,MC7_5_faulty.tla,apalache,10h,,PrecisionInv,,--length=30
|
||||
36,MC7_5_faulty.tla,apalache,10h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30
|
||||
37,MC7_5_faulty.tla,apalache,10h,,NoFailedBlocksOnSuccessInv,,--length=30
|
||||
38,MC7_5_faulty.tla,apalache,10h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30
|
||||
39,MC7_5_faulty.tla,apalache,10h,,CorrectPrimaryAndTimeliness,,--length=30
|
||||
40,MC7_5_faulty.tla,apalache,10h,,Complexity,,--length=30
|
||||
41,MC4_7_faulty.tla,apalache,10h,,PositiveBeforeTrustedHeaderExpires,,--length=30
|
||||
42,MC4_7_faulty.tla,apalache,10h,,CorrectnessInv,,--length=30
|
||||
43,MC4_7_faulty.tla,apalache,10h,,PrecisionInv,,--length=30
|
||||
44,MC4_7_faulty.tla,apalache,10h,,SuccessOnCorrectPrimaryAndChainOfTrust,,--length=30
|
||||
45,MC4_7_faulty.tla,apalache,10h,,NoFailedBlocksOnSuccessInv,,--length=30
|
||||
46,MC4_7_faulty.tla,apalache,10h,,StoredHeadersAreVerifiedOrNotTrustedInv,,--length=30
|
||||
47,MC4_7_faulty.tla,apalache,10h,,CorrectPrimaryAndTimeliness,,--length=30
|
||||
48,MC4_7_faulty.tla,apalache,10h,,Complexity,,--length=30
|
||||
|
@@ -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
|
||||
|
||||
|
@@ -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
|
||||
|
@@ -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
|
||||
|
@@ -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
|
||||
|
@@ -0,0 +1,171 @@
|
||||
------------------------ MODULE Blockchain_002_draft -----------------------------
|
||||
(*
|
||||
This is a high-level specification of Tendermint blockchain
|
||||
that is designed specifically for the light client.
|
||||
Validators have the voting power of one. If you like to model various
|
||||
voting powers, introduce multiple copies of the same validator
|
||||
(do not forget to give them unique names though).
|
||||
*)
|
||||
EXTENDS Integers, FiniteSets
|
||||
|
||||
Min(a, b) == IF a < b THEN a ELSE b
|
||||
|
||||
CONSTANT
|
||||
AllNodes,
|
||||
(* a set of all nodes that can act as validators (correct and faulty) *)
|
||||
ULTIMATE_HEIGHT,
|
||||
(* a maximal height that can be ever reached (modelling artifact) *)
|
||||
TRUSTING_PERIOD
|
||||
(* the period within which the validators are trusted *)
|
||||
|
||||
Heights == 1..ULTIMATE_HEIGHT (* possible heights *)
|
||||
|
||||
(* A commit is just a set of nodes who have committed the block *)
|
||||
Commits == SUBSET AllNodes
|
||||
|
||||
(* The set of all block headers that can be on the blockchain.
|
||||
This is a simplified version of the Block data structure in the actual implementation. *)
|
||||
BlockHeaders == [
|
||||
height: Heights,
|
||||
\* the block height
|
||||
time: Int,
|
||||
\* the block timestamp in some integer units
|
||||
lastCommit: Commits,
|
||||
\* the nodes who have voted on the previous block, the set itself instead of a hash
|
||||
(* in the implementation, only the hashes of V and NextV are stored in a block,
|
||||
as V and NextV are stored in the application state *)
|
||||
VS: SUBSET AllNodes,
|
||||
\* the validators of this bloc. We store the validators instead of the hash.
|
||||
NextVS: SUBSET AllNodes
|
||||
\* the validators of the next block. We store the next validators instead of the hash.
|
||||
]
|
||||
|
||||
(* A signed header is just a header together with a set of commits *)
|
||||
LightBlocks == [header: BlockHeaders, Commits: Commits]
|
||||
|
||||
VARIABLES
|
||||
now,
|
||||
(* the current global time in integer units *)
|
||||
blockchain,
|
||||
(* A sequence of BlockHeaders, which gives us a bird view of the blockchain. *)
|
||||
Faulty
|
||||
(* A set of faulty nodes, which can act as validators. We assume that the set
|
||||
of faulty processes is non-decreasing. If a process has recovered, it should
|
||||
connect using a different id. *)
|
||||
|
||||
(* all variables, to be used with UNCHANGED *)
|
||||
vars == <<now, blockchain, Faulty>>
|
||||
|
||||
(* The set of all correct nodes in a state *)
|
||||
Corr == AllNodes \ Faulty
|
||||
|
||||
(* APALACHE annotations *)
|
||||
a <: b == a \* type annotation
|
||||
|
||||
NT == STRING
|
||||
NodeSet(S) == S <: {NT}
|
||||
EmptyNodeSet == NodeSet({})
|
||||
|
||||
BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}]
|
||||
|
||||
LBT == [header |-> BT, Commits |-> {NT}]
|
||||
(* end of APALACHE annotations *)
|
||||
|
||||
(****************************** BLOCKCHAIN ************************************)
|
||||
|
||||
(* the header is still within the trusting period *)
|
||||
InTrustingPeriod(header) ==
|
||||
now < header.time + TRUSTING_PERIOD
|
||||
|
||||
(*
|
||||
Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes
|
||||
and pNodes \subseteq D, test whether the set pNodes \subseteq AllNodes has
|
||||
more than 2/3 of voting power among the nodes in D.
|
||||
*)
|
||||
TwoThirds(pVS, pNodes) ==
|
||||
LET TP == Cardinality(pVS)
|
||||
SP == Cardinality(pVS \intersect pNodes)
|
||||
IN
|
||||
3 * SP > 2 * TP \* when thinking in real numbers, not integers: SP > 2.0 / 3.0 * TP
|
||||
|
||||
(*
|
||||
Given a set of FaultyNodes, test whether the voting power of the correct nodes in D
|
||||
is more than 2/3 of the voting power of the faulty nodes in D.
|
||||
*)
|
||||
IsCorrectPower(pFaultyNodes, pVS) ==
|
||||
LET FN == pFaultyNodes \intersect pVS \* faulty nodes in pNodes
|
||||
CN == pVS \ pFaultyNodes \* correct nodes in pNodes
|
||||
CP == Cardinality(CN) \* power of the correct nodes
|
||||
FP == Cardinality(FN) \* power of the faulty nodes
|
||||
IN
|
||||
\* CP + FP = TP is the total voting power, so we write CP > 2.0 / 3 * TP as follows:
|
||||
CP > 2 * FP \* Note: when FP = 0, this implies CP > 0.
|
||||
|
||||
(* This is what we believe is the assumption about failures in Tendermint *)
|
||||
FaultAssumption(pFaultyNodes, pNow, pBlockchain) ==
|
||||
\A h \in Heights:
|
||||
pBlockchain[h].time + TRUSTING_PERIOD > pNow =>
|
||||
IsCorrectPower(pFaultyNodes, pBlockchain[h].NextVS)
|
||||
|
||||
(* Can a block be produced by a correct peer, or an authenticated Byzantine peer *)
|
||||
IsLightBlockAllowedByDigitalSignatures(ht, block) ==
|
||||
\/ block.header = blockchain[ht] \* signed by correct and faulty (maybe)
|
||||
\/ block.Commits \subseteq Faulty /\ block.header.height = ht /\ 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.
|
||||
*)
|
||||
InitToHeight ==
|
||||
/\ Faulty \in SUBSET AllNodes \* some nodes may fail
|
||||
\* pick the validator sets and last commits
|
||||
/\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]:
|
||||
\E timestamp \in [Heights -> Int]:
|
||||
\* now is at least as early as the timestamp in the last block
|
||||
/\ \E tm \in Int: now = tm /\ tm >= timestamp[ULTIMATE_HEIGHT]
|
||||
\* the genesis starts on day 1
|
||||
/\ timestamp[1] = 1
|
||||
/\ vs[1] = AllNodes
|
||||
/\ lastCommit[1] = EmptyNodeSet
|
||||
/\ \A h \in Heights \ {1}:
|
||||
/\ lastCommit[h] \subseteq vs[h - 1] \* the non-validators cannot commit
|
||||
/\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes
|
||||
/\ IsCorrectPower(Faulty, vs[h]) \* the correct validators have >2/3 of power
|
||||
/\ timestamp[h] > timestamp[h - 1] \* the time grows monotonically
|
||||
/\ timestamp[h] < timestamp[h - 1] + TRUSTING_PERIOD \* but not too fast
|
||||
\* form the block chain out of validator sets and commits (this makes apalache faster)
|
||||
/\ blockchain = [h \in Heights |->
|
||||
[height |-> h,
|
||||
time |-> timestamp[h],
|
||||
VS |-> vs[h],
|
||||
NextVS |-> IF h < ULTIMATE_HEIGHT THEN vs[h + 1] ELSE AllNodes,
|
||||
lastCommit |-> lastCommit[h]]
|
||||
] \******
|
||||
|
||||
|
||||
(* is the blockchain in the faulty zone where the Tendermint security model does not apply *)
|
||||
InFaultyZone ==
|
||||
~FaultAssumption(Faulty, now, blockchain)
|
||||
|
||||
(********************* BLOCKCHAIN ACTIONS ********************************)
|
||||
(*
|
||||
Advance the clock by zero or more time units.
|
||||
*)
|
||||
AdvanceTime ==
|
||||
\E tm \in Int: tm >= now /\ now' = tm
|
||||
/\ UNCHANGED <<blockchain, Faulty>>
|
||||
|
||||
(*
|
||||
One more process fails. As a result, the blockchain may move into the faulty zone.
|
||||
The light client is not using this action, as the faults are picked in the initial state.
|
||||
However, this action may be useful when reasoning about fork detection.
|
||||
*)
|
||||
OneMoreFault ==
|
||||
/\ \E n \in AllNodes \ Faulty:
|
||||
/\ Faulty' = Faulty \cup {n}
|
||||
/\ Faulty' /= AllNodes \* at least process remains non-faulty
|
||||
/\ UNCHANGED <<now, blockchain>>
|
||||
=============================================================================
|
||||
\* 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
|
||||
@@ -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 == <<refClock, blockchain, Faulty>>
|
||||
|
||||
(* The set of all correct nodes in a state *)
|
||||
Corr == AllNodes \ Faulty
|
||||
|
||||
(* APALACHE annotations *)
|
||||
a <: b == a \* type annotation
|
||||
|
||||
NT == STRING
|
||||
NodeSet(S) == S <: {NT}
|
||||
EmptyNodeSet == NodeSet({})
|
||||
|
||||
BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}]
|
||||
|
||||
LBT == [header |-> BT, Commits |-> {NT}]
|
||||
(* end of APALACHE annotations *)
|
||||
|
||||
(****************************** BLOCKCHAIN ************************************)
|
||||
|
||||
(* the header is still within the trusting period *)
|
||||
InTrustingPeriod(header) ==
|
||||
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 <<a, b>> that limits the ratio a / b of the faulty
|
||||
validators from above (exclusive)
|
||||
*)
|
||||
FaultyValidatorsFewerThan(pFaultyNodes, pVS, maxRatio) ==
|
||||
LET FN == pFaultyNodes \intersect pVS \* faulty nodes in pNodes
|
||||
CN == pVS \ pFaultyNodes \* correct nodes in pNodes
|
||||
CP == Cardinality(CN) \* power of the correct nodes
|
||||
FP == Cardinality(FN) \* power of the faulty nodes
|
||||
IN
|
||||
\* CP + FP = TP is the total voting power
|
||||
LET TP == CP + FP IN
|
||||
FP * maxRatio[2] < TP * maxRatio[1]
|
||||
|
||||
(* Can a block be produced by a correct peer, or an authenticated Byzantine peer *)
|
||||
IsLightBlockAllowedByDigitalSignatures(ht, block) ==
|
||||
\/ block.header = blockchain[ht] \* signed by correct and faulty (maybe)
|
||||
\/ /\ block.Commits \subseteq Faulty
|
||||
/\ block.header.height = ht
|
||||
/\ block.header.time >= 0 \* signed only by faulty
|
||||
|
||||
(*
|
||||
Initialize the blockchain to the ultimate height right in the initial states.
|
||||
We pick the faulty validators statically, but that should not affect the light client.
|
||||
|
||||
Parameters:
|
||||
- pMaxFaultyRatioExclusive is a pair <<a, b>> that bound the number of
|
||||
faulty validators in each block by the ratio a / b (exclusive)
|
||||
*)
|
||||
InitToHeight(pMaxFaultyRatioExclusive) ==
|
||||
/\ Faulty \in SUBSET AllNodes \* some nodes may fail
|
||||
\* pick the validator sets and last commits
|
||||
/\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]:
|
||||
\E timestamp \in [Heights -> Int]:
|
||||
\* 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 <<blockchain, Faulty>>
|
||||
|
||||
=============================================================================
|
||||
\* Modification History
|
||||
\* Last modified Wed Jun 10 14:10:54 CEST 2020 by igor
|
||||
\* Created Fri Oct 11 15:45:11 CEST 2019 by igor
|
||||
@@ -0,0 +1,171 @@
|
||||
------------------------ MODULE Blockchain_A_1 -----------------------------
|
||||
(*
|
||||
This is a high-level specification of Tendermint blockchain
|
||||
that is designed specifically for the light client.
|
||||
Validators have the voting power of one. If you like to model various
|
||||
voting powers, introduce multiple copies of the same validator
|
||||
(do not forget to give them unique names though).
|
||||
*)
|
||||
EXTENDS Integers, FiniteSets
|
||||
|
||||
Min(a, b) == IF a < b THEN a ELSE b
|
||||
|
||||
CONSTANT
|
||||
AllNodes,
|
||||
(* a set of all nodes that can act as validators (correct and faulty) *)
|
||||
ULTIMATE_HEIGHT,
|
||||
(* a maximal height that can be ever reached (modelling artifact) *)
|
||||
TRUSTING_PERIOD
|
||||
(* the period within which the validators are trusted *)
|
||||
|
||||
Heights == 1..ULTIMATE_HEIGHT (* possible heights *)
|
||||
|
||||
(* A commit is just a set of nodes who have committed the block *)
|
||||
Commits == SUBSET AllNodes
|
||||
|
||||
(* The set of all block headers that can be on the blockchain.
|
||||
This is a simplified version of the Block data structure in the actual implementation. *)
|
||||
BlockHeaders == [
|
||||
height: Heights,
|
||||
\* the block height
|
||||
time: Int,
|
||||
\* the block timestamp in some integer units
|
||||
lastCommit: Commits,
|
||||
\* the nodes who have voted on the previous block, the set itself instead of a hash
|
||||
(* in the implementation, only the hashes of V and NextV are stored in a block,
|
||||
as V and NextV are stored in the application state *)
|
||||
VS: SUBSET AllNodes,
|
||||
\* the validators of this bloc. We store the validators instead of the hash.
|
||||
NextVS: SUBSET AllNodes
|
||||
\* the validators of the next block. We store the next validators instead of the hash.
|
||||
]
|
||||
|
||||
(* A signed header is just a header together with a set of commits *)
|
||||
LightBlocks == [header: BlockHeaders, Commits: Commits]
|
||||
|
||||
VARIABLES
|
||||
now,
|
||||
(* the current global time in integer units *)
|
||||
blockchain,
|
||||
(* A sequence of BlockHeaders, which gives us a bird view of the blockchain. *)
|
||||
Faulty
|
||||
(* A set of faulty nodes, which can act as validators. We assume that the set
|
||||
of faulty processes is non-decreasing. If a process has recovered, it should
|
||||
connect using a different id. *)
|
||||
|
||||
(* all variables, to be used with UNCHANGED *)
|
||||
vars == <<now, blockchain, Faulty>>
|
||||
|
||||
(* The set of all correct nodes in a state *)
|
||||
Corr == AllNodes \ Faulty
|
||||
|
||||
(* APALACHE annotations *)
|
||||
a <: b == a \* type annotation
|
||||
|
||||
NT == STRING
|
||||
NodeSet(S) == S <: {NT}
|
||||
EmptyNodeSet == NodeSet({})
|
||||
|
||||
BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}]
|
||||
|
||||
LBT == [header |-> BT, Commits |-> {NT}]
|
||||
(* end of APALACHE annotations *)
|
||||
|
||||
(****************************** BLOCKCHAIN ************************************)
|
||||
|
||||
(* the header is still within the trusting period *)
|
||||
InTrustingPeriod(header) ==
|
||||
now <= header.time + TRUSTING_PERIOD
|
||||
|
||||
(*
|
||||
Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes
|
||||
and pNodes \subseteq D, test whether the set pNodes \subseteq AllNodes has
|
||||
more than 2/3 of voting power among the nodes in D.
|
||||
*)
|
||||
TwoThirds(pVS, pNodes) ==
|
||||
LET TP == Cardinality(pVS)
|
||||
SP == Cardinality(pVS \intersect pNodes)
|
||||
IN
|
||||
3 * SP > 2 * TP \* when thinking in real numbers, not integers: SP > 2.0 / 3.0 * TP
|
||||
|
||||
(*
|
||||
Given a set of FaultyNodes, test whether the voting power of the correct nodes in D
|
||||
is more than 2/3 of the voting power of the faulty nodes in D.
|
||||
*)
|
||||
IsCorrectPower(pFaultyNodes, pVS) ==
|
||||
LET FN == pFaultyNodes \intersect pVS \* faulty nodes in pNodes
|
||||
CN == pVS \ pFaultyNodes \* correct nodes in pNodes
|
||||
CP == Cardinality(CN) \* power of the correct nodes
|
||||
FP == Cardinality(FN) \* power of the faulty nodes
|
||||
IN
|
||||
\* CP + FP = TP is the total voting power, so we write CP > 2.0 / 3 * TP as follows:
|
||||
CP > 2 * FP \* Note: when FP = 0, this implies CP > 0.
|
||||
|
||||
(* This is what we believe is the assumption about failures in Tendermint *)
|
||||
FaultAssumption(pFaultyNodes, pNow, pBlockchain) ==
|
||||
\A h \in Heights:
|
||||
pBlockchain[h].time + TRUSTING_PERIOD > pNow =>
|
||||
IsCorrectPower(pFaultyNodes, pBlockchain[h].NextVS)
|
||||
|
||||
(* Can a block be produced by a correct peer, or an authenticated Byzantine peer *)
|
||||
IsLightBlockAllowedByDigitalSignatures(ht, block) ==
|
||||
\/ block.header = blockchain[ht] \* signed by correct and faulty (maybe)
|
||||
\/ block.Commits \subseteq Faulty /\ block.header.height = ht \* signed only by faulty
|
||||
|
||||
(*
|
||||
Initialize the blockchain to the ultimate height right in the initial states.
|
||||
We pick the faulty validators statically, but that should not affect the light client.
|
||||
*)
|
||||
InitToHeight ==
|
||||
/\ Faulty \in SUBSET AllNodes \* some nodes may fail
|
||||
\* pick the validator sets and last commits
|
||||
/\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]:
|
||||
\E timestamp \in [Heights -> Int]:
|
||||
\* now is at least as early as the timestamp in the last block
|
||||
/\ \E tm \in Int: now = tm /\ tm >= timestamp[ULTIMATE_HEIGHT]
|
||||
\* the genesis starts on day 1
|
||||
/\ timestamp[1] = 1
|
||||
/\ vs[1] = AllNodes
|
||||
/\ lastCommit[1] = EmptyNodeSet
|
||||
/\ \A h \in Heights \ {1}:
|
||||
/\ lastCommit[h] \subseteq vs[h - 1] \* the non-validators cannot commit
|
||||
/\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes
|
||||
/\ IsCorrectPower(Faulty, vs[h]) \* the correct validators have >2/3 of power
|
||||
/\ timestamp[h] > timestamp[h - 1] \* the time grows monotonically
|
||||
/\ timestamp[h] < timestamp[h - 1] + TRUSTING_PERIOD \* but not too fast
|
||||
\* form the block chain out of validator sets and commits (this makes apalache faster)
|
||||
/\ blockchain = [h \in Heights |->
|
||||
[height |-> h,
|
||||
time |-> timestamp[h],
|
||||
VS |-> vs[h],
|
||||
NextVS |-> IF h < ULTIMATE_HEIGHT THEN vs[h + 1] ELSE AllNodes,
|
||||
lastCommit |-> lastCommit[h]]
|
||||
] \******
|
||||
|
||||
|
||||
(* is the blockchain in the faulty zone where the Tendermint security model does not apply *)
|
||||
InFaultyZone ==
|
||||
~FaultAssumption(Faulty, now, blockchain)
|
||||
|
||||
(********************* BLOCKCHAIN ACTIONS ********************************)
|
||||
(*
|
||||
Advance the clock by zero or more time units.
|
||||
*)
|
||||
AdvanceTime ==
|
||||
\E tm \in Int: tm >= now /\ now' = tm
|
||||
/\ UNCHANGED <<blockchain, Faulty>>
|
||||
|
||||
(*
|
||||
One more process fails. As a result, the blockchain may move into the faulty zone.
|
||||
The light client is not using this action, as the faults are picked in the initial state.
|
||||
However, this action may be useful when reasoning about fork detection.
|
||||
*)
|
||||
OneMoreFault ==
|
||||
/\ \E n \in AllNodes \ Faulty:
|
||||
/\ Faulty' = Faulty \cup {n}
|
||||
/\ Faulty' /= AllNodes \* at least process remains non-faulty
|
||||
/\ UNCHANGED <<now, blockchain>>
|
||||
=============================================================================
|
||||
\* 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
|
||||
@@ -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 <<a, b>> 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)
|
||||
|
||||
|
||||
==================================================================================
|
||||
@@ -0,0 +1,465 @@
|
||||
-------------------------- MODULE Lightclient_002_draft ----------------------------
|
||||
(**
|
||||
* A state-machine specification of the lite client, following the English spec:
|
||||
*
|
||||
* https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md
|
||||
*)
|
||||
|
||||
EXTENDS Integers, FiniteSets
|
||||
|
||||
\* the parameters of Light Client
|
||||
CONSTANTS
|
||||
TRUSTED_HEIGHT,
|
||||
(* an index of the block header that the light client trusts by social consensus *)
|
||||
TARGET_HEIGHT,
|
||||
(* an index of the block header that the light client tries to verify *)
|
||||
TRUSTING_PERIOD,
|
||||
(* the period within which the validators are trusted *)
|
||||
IS_PRIMARY_CORRECT
|
||||
(* is primary correct? *)
|
||||
|
||||
VARIABLES (* see TypeOK below for the variable types *)
|
||||
state, (* the current state of the light client *)
|
||||
nextHeight, (* the next height to explore by the light client *)
|
||||
nprobes (* the lite client iteration, or the number of block tests *)
|
||||
|
||||
(* the light store *)
|
||||
VARIABLES
|
||||
fetchedLightBlocks, (* a function from heights to LightBlocks *)
|
||||
lightBlockStatus, (* a function from heights to block statuses *)
|
||||
latestVerified (* the latest verified block *)
|
||||
|
||||
(* the variables of the lite client *)
|
||||
lcvars == <<state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified>>
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevNow,
|
||||
prevVerdict
|
||||
|
||||
InitMonitor(verified, current, now, verdict) ==
|
||||
/\ prevVerified = verified
|
||||
/\ prevCurrent = current
|
||||
/\ prevNow = now
|
||||
/\ prevVerdict = verdict
|
||||
|
||||
NextMonitor(verified, current, now, verdict) ==
|
||||
/\ prevVerified' = verified
|
||||
/\ prevCurrent' = current
|
||||
/\ prevNow' = now
|
||||
/\ prevVerdict' = verdict
|
||||
|
||||
|
||||
(******************* Blockchain instance ***********************************)
|
||||
|
||||
\* the parameters that are propagated into Blockchain
|
||||
CONSTANTS
|
||||
AllNodes
|
||||
(* a set of all nodes that can act as validators (correct and faulty) *)
|
||||
|
||||
\* the state variables of Blockchain, see Blockchain.tla for the details
|
||||
VARIABLES now, blockchain, Faulty
|
||||
|
||||
\* All the variables of Blockchain. For some reason, BC!vars does not work
|
||||
bcvars == <<now, blockchain, Faulty>>
|
||||
|
||||
(* Create an instance of Blockchain.
|
||||
We could write EXTENDS Blockchain, but then all the constants and state variables
|
||||
would be hidden inside the Blockchain module.
|
||||
*)
|
||||
ULTIMATE_HEIGHT == TARGET_HEIGHT + 1
|
||||
|
||||
BC == INSTANCE Blockchain_002_draft WITH
|
||||
now <- now, blockchain <- blockchain, Faulty <- Faulty
|
||||
|
||||
(************************** Lite client ************************************)
|
||||
|
||||
(* the heights on which the light client is working *)
|
||||
HEIGHTS == TRUSTED_HEIGHT..TARGET_HEIGHT
|
||||
|
||||
(* the control states of the lite client *)
|
||||
States == { "working", "finishedSuccess", "finishedFailure" }
|
||||
|
||||
(**
|
||||
Check the precondition of ValidAndVerified.
|
||||
|
||||
[LCV-FUNC-VALID.1::TLA-PRE.1]
|
||||
*)
|
||||
ValidAndVerifiedPre(trusted, untrusted) ==
|
||||
LET thdr == trusted.header
|
||||
uhdr == untrusted.header
|
||||
IN
|
||||
/\ BC!InTrustingPeriod(thdr)
|
||||
/\ thdr.height < uhdr.height
|
||||
\* the trusted block has been created earlier (no drift here)
|
||||
/\ thdr.time < uhdr.time
|
||||
\* the untrusted block is not from the future
|
||||
/\ uhdr.time < now
|
||||
/\ untrusted.Commits \subseteq uhdr.VS
|
||||
/\ LET TP == Cardinality(uhdr.VS)
|
||||
SP == Cardinality(untrusted.Commits)
|
||||
IN
|
||||
3 * SP > 2 * TP
|
||||
/\ thdr.height + 1 = uhdr.height => thdr.NextVS = uhdr.VS
|
||||
(* As we do not have explicit hashes we ignore these three checks of the English spec:
|
||||
|
||||
1. "trusted.Commit is a commit is for the header trusted.Header,
|
||||
i.e. it contains the correct hash of the header".
|
||||
2. untrusted.Validators = hash(untrusted.Header.Validators)
|
||||
3. untrusted.NextValidators = hash(untrusted.Header.NextValidators)
|
||||
*)
|
||||
|
||||
(**
|
||||
* Check that the commits in an untrusted block form 1/3 of the next validators
|
||||
* in a trusted header.
|
||||
*)
|
||||
SignedByOneThirdOfTrusted(trusted, untrusted) ==
|
||||
LET TP == Cardinality(trusted.header.NextVS)
|
||||
SP == Cardinality(untrusted.Commits \intersect trusted.header.NextVS)
|
||||
IN
|
||||
3 * SP > TP
|
||||
|
||||
(**
|
||||
Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header.
|
||||
|
||||
[LCV-FUNC-VALID.1::TLA.1]
|
||||
*)
|
||||
ValidAndVerified(trusted, untrusted) ==
|
||||
IF ~ValidAndVerifiedPre(trusted, untrusted)
|
||||
THEN "INVALID"
|
||||
ELSE IF ~BC!InTrustingPeriod(untrusted.header)
|
||||
(* We leave the following test for the documentation purposes.
|
||||
The implementation should do this test, as signature verification may be slow.
|
||||
In the TLA+ specification, ValidAndVerified happens in no time.
|
||||
*)
|
||||
THEN "FAILED_TRUSTING_PERIOD"
|
||||
ELSE IF untrusted.header.height = trusted.header.height + 1
|
||||
\/ SignedByOneThirdOfTrusted(trusted, untrusted)
|
||||
THEN "SUCCESS"
|
||||
ELSE "NOT_ENOUGH_TRUST"
|
||||
|
||||
(*
|
||||
Initial states of the light client.
|
||||
Initially, only the trusted light block is present.
|
||||
*)
|
||||
LCInit ==
|
||||
/\ state = "working"
|
||||
/\ nextHeight = TARGET_HEIGHT
|
||||
/\ nprobes = 0 \* no tests have been done so far
|
||||
/\ LET trustedBlock == blockchain[TRUSTED_HEIGHT]
|
||||
trustedLightBlock == [header |-> trustedBlock, Commits |-> AllNodes]
|
||||
IN
|
||||
\* initially, fetchedLightBlocks is a function of one element, i.e., TRUSTED_HEIGHT
|
||||
/\ fetchedLightBlocks = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock]
|
||||
\* initially, lightBlockStatus is a function of one element, i.e., TRUSTED_HEIGHT
|
||||
/\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"]
|
||||
\* the latest verified block the the trusted block
|
||||
/\ latestVerified = trustedLightBlock
|
||||
/\ InitMonitor(trustedLightBlock, trustedLightBlock, now, "SUCCESS")
|
||||
|
||||
\* block should contain a copy of the block from the reference chain, with a matching commit
|
||||
CopyLightBlockFromChain(block, height) ==
|
||||
LET ref == blockchain[height]
|
||||
lastCommit ==
|
||||
IF height < ULTIMATE_HEIGHT
|
||||
THEN blockchain[height + 1].lastCommit
|
||||
\* for the ultimate block, which we never use, as ULTIMATE_HEIGHT = TARGET_HEIGHT + 1
|
||||
ELSE blockchain[height].VS
|
||||
IN
|
||||
block = [header |-> ref, Commits |-> lastCommit]
|
||||
|
||||
\* Either the primary is correct and the block comes from the reference chain,
|
||||
\* or the block is produced by a faulty primary.
|
||||
\*
|
||||
\* [LCV-FUNC-FETCH.1::TLA.1]
|
||||
FetchLightBlockInto(block, height) ==
|
||||
IF IS_PRIMARY_CORRECT
|
||||
THEN CopyLightBlockFromChain(block, height)
|
||||
ELSE BC!IsLightBlockAllowedByDigitalSignatures(height, block)
|
||||
|
||||
\* add a block into the light store
|
||||
\*
|
||||
\* [LCV-FUNC-UPDATE.1::TLA.1]
|
||||
LightStoreUpdateBlocks(lightBlocks, block) ==
|
||||
LET ht == block.header.height IN
|
||||
[h \in DOMAIN lightBlocks \union {ht} |->
|
||||
IF h = ht THEN block ELSE lightBlocks[h]]
|
||||
|
||||
\* update the state of a light block
|
||||
\*
|
||||
\* [LCV-FUNC-UPDATE.1::TLA.1]
|
||||
LightStoreUpdateStates(statuses, ht, blockState) ==
|
||||
[h \in DOMAIN statuses \union {ht} |->
|
||||
IF h = ht THEN blockState ELSE statuses[h]]
|
||||
|
||||
\* Check, whether newHeight is a possible next height for the light client.
|
||||
\*
|
||||
\* [LCV-FUNC-SCHEDULE.1::TLA.1]
|
||||
CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) ==
|
||||
LET ht == pLatestVerified.header.height IN
|
||||
\/ /\ ht = pNextHeight
|
||||
/\ ht < pTargetHeight
|
||||
/\ pNextHeight < newHeight
|
||||
/\ newHeight <= pTargetHeight
|
||||
\/ /\ ht < pNextHeight
|
||||
/\ ht < pTargetHeight
|
||||
/\ ht < newHeight
|
||||
/\ newHeight < pNextHeight
|
||||
\/ /\ ht = pTargetHeight
|
||||
/\ newHeight = pTargetHeight
|
||||
|
||||
\* The loop of VerifyToTarget.
|
||||
\*
|
||||
\* [LCV-FUNC-MAIN.1::TLA-LOOP.1]
|
||||
VerifyToTargetLoop ==
|
||||
\* the loop condition is true
|
||||
/\ latestVerified.header.height < TARGET_HEIGHT
|
||||
\* pick a light block, which will be constrained later
|
||||
/\ \E current \in BC!LightBlocks:
|
||||
\* Get next LightBlock for verification
|
||||
/\ IF nextHeight \in DOMAIN fetchedLightBlocks
|
||||
THEN \* copy the block from the light store
|
||||
/\ current = fetchedLightBlocks[nextHeight]
|
||||
/\ UNCHANGED fetchedLightBlocks
|
||||
ELSE \* retrieve a light block and save it in the light store
|
||||
/\ FetchLightBlockInto(current, nextHeight)
|
||||
/\ fetchedLightBlocks' = LightStoreUpdateBlocks(fetchedLightBlocks, current)
|
||||
\* Record that one more probe has been done (for complexity and model checking)
|
||||
/\ nprobes' = nprobes + 1
|
||||
\* Verify the current block
|
||||
/\ LET verdict == ValidAndVerified(latestVerified, current) IN
|
||||
NextMonitor(latestVerified, current, now, verdict) /\
|
||||
\* Decide whether/how to continue
|
||||
CASE verdict = "SUCCESS" ->
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified")
|
||||
/\ latestVerified' = current
|
||||
/\ state' =
|
||||
IF latestVerified'.header.height < TARGET_HEIGHT
|
||||
THEN "working"
|
||||
ELSE "finishedSuccess"
|
||||
/\ \E newHeight \in HEIGHTS:
|
||||
/\ CanScheduleTo(newHeight, current, nextHeight, TARGET_HEIGHT)
|
||||
/\ nextHeight' = newHeight
|
||||
|
||||
[] verdict = "NOT_ENOUGH_TRUST" ->
|
||||
(*
|
||||
do nothing: the light block current passed validation, but the validator
|
||||
set is too different to verify it. We keep the state of
|
||||
current at StateUnverified. For a later iteration, Schedule
|
||||
might decide to try verification of that light block again.
|
||||
*)
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateUnverified")
|
||||
/\ \E newHeight \in HEIGHTS:
|
||||
/\ CanScheduleTo(newHeight, latestVerified, nextHeight, TARGET_HEIGHT)
|
||||
/\ nextHeight' = newHeight
|
||||
/\ UNCHANGED <<latestVerified, state>>
|
||||
|
||||
[] OTHER ->
|
||||
\* verdict is some error code
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateFailed")
|
||||
/\ state' = "finishedFailure"
|
||||
/\ UNCHANGED <<latestVerified, nextHeight>>
|
||||
|
||||
\* The terminating condition of VerifyToTarget.
|
||||
\*
|
||||
\* [LCV-FUNC-MAIN.1::TLA-LOOPCOND.1]
|
||||
VerifyToTargetDone ==
|
||||
/\ latestVerified.header.height >= TARGET_HEIGHT
|
||||
/\ state' = "finishedSuccess"
|
||||
/\ UNCHANGED <<nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, latestVerified>>
|
||||
/\ UNCHANGED <<prevVerified, prevCurrent, prevNow, prevVerdict>>
|
||||
|
||||
(********************* Lite client + Blockchain *******************)
|
||||
Init ==
|
||||
\* the blockchain is initialized immediately to the ULTIMATE_HEIGHT
|
||||
/\ BC!InitToHeight
|
||||
\* the light client starts
|
||||
/\ LCInit
|
||||
|
||||
(*
|
||||
The system step is very simple.
|
||||
The light client is either executing VerifyToTarget, or it has terminated.
|
||||
(In the latter case, a model checker reports a deadlock.)
|
||||
Simultaneously, the global clock may advance.
|
||||
*)
|
||||
Next ==
|
||||
/\ state = "working"
|
||||
/\ VerifyToTargetLoop \/ VerifyToTargetDone
|
||||
/\ BC!AdvanceTime \* the global clock is advanced by zero or more time units
|
||||
|
||||
(************************* Types ******************************************)
|
||||
TypeOK ==
|
||||
/\ state \in States
|
||||
/\ nextHeight \in HEIGHTS
|
||||
/\ latestVerified \in BC!LightBlocks
|
||||
/\ \E HS \in SUBSET HEIGHTS:
|
||||
/\ fetchedLightBlocks \in [HS -> BC!LightBlocks]
|
||||
/\ lightBlockStatus
|
||||
\in [HS -> {"StateVerified", "StateUnverified", "StateFailed"}]
|
||||
|
||||
(************************* Properties ******************************************)
|
||||
|
||||
(* The properties to check *)
|
||||
\* this invariant candidate is false
|
||||
NeverFinish ==
|
||||
state = "working"
|
||||
|
||||
\* this invariant candidate is false
|
||||
NeverFinishNegative ==
|
||||
state /= "finishedFailure"
|
||||
|
||||
\* This invariant holds true, when the primary is correct.
|
||||
\* This invariant candidate is false when the primary is faulty.
|
||||
NeverFinishNegativeWhenTrusted ==
|
||||
(*(minTrustedHeight <= TRUSTED_HEIGHT)*)
|
||||
BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
=> state /= "finishedFailure"
|
||||
|
||||
\* this invariant candidate is false
|
||||
NeverFinishPositive ==
|
||||
state /= "finishedSuccess"
|
||||
|
||||
(**
|
||||
Correctness states that all the obtained headers are exactly like in the blockchain.
|
||||
|
||||
It is always the case that every verified header in LightStore was generated by
|
||||
an instance of Tendermint consensus.
|
||||
|
||||
[LCV-DIST-SAFE.1::CORRECTNESS-INV.1]
|
||||
*)
|
||||
CorrectnessInv ==
|
||||
\A h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] = "StateVerified" =>
|
||||
fetchedLightBlocks[h].header = blockchain[h]
|
||||
|
||||
(**
|
||||
Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "SUCCESS" pairwise
|
||||
This property is easily violated, whenever a header cannot be trusted anymore.
|
||||
*)
|
||||
StoredHeadersAreVerifiedInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers
|
||||
\/ lh >= rh
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
|
||||
|
||||
\* An improved version of StoredHeadersAreSound, assuming that a header may be not trusted.
|
||||
\* This invariant candidate is also violated,
|
||||
\* as there may be some unverified blocks left in the middle.
|
||||
StoredHeadersAreVerifiedOrNotTrustedInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers
|
||||
\/ lh >= rh
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
|
||||
\* or the left header is outside the trusting period, so no guarantees
|
||||
\/ ~BC!InTrustingPeriod(fetchedLightBlocks[lh].header)
|
||||
|
||||
(**
|
||||
* An improved version of StoredHeadersAreSoundOrNotTrusted,
|
||||
* checking the property only for the verified headers.
|
||||
* This invariant holds true.
|
||||
*)
|
||||
ProofOfChainOfTrustInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks:
|
||||
\* for every pair of stored headers that have been verified
|
||||
\/ lh >= rh
|
||||
\/ lightBlockStatus[lh] = "StateUnverified"
|
||||
\/ lightBlockStatus[rh] = "StateUnverified"
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh /\ lightBlockStatus[mh] = "StateVerified"
|
||||
\* or the left header is outside the trusting period, so no guarantees
|
||||
\/ ~(BC!InTrustingPeriod(fetchedLightBlocks[lh].header))
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
|
||||
|
||||
(**
|
||||
* When the light client terminates, there are no failed blocks. (Otherwise, someone lied to us.)
|
||||
*)
|
||||
NoFailedBlocksOnSuccessInv ==
|
||||
state = "finishedSuccess" =>
|
||||
\A h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] /= "StateFailed"
|
||||
|
||||
\* This property states that whenever the light client finishes with a positive outcome,
|
||||
\* the trusted header is still within the trusting period.
|
||||
\* We expect this property to be violated. And Apalache shows us a counterexample.
|
||||
PositiveBeforeTrustedHeaderExpires ==
|
||||
(state = "finishedSuccess") => BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
|
||||
\* If the primary is correct and the initial trusted block has not expired,
|
||||
\* then whenever the algorithm terminates, it reports "success"
|
||||
CorrectPrimaryAndTimeliness ==
|
||||
(BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
/\ state /= "working" /\ IS_PRIMARY_CORRECT) =>
|
||||
state = "finishedSuccess"
|
||||
|
||||
(**
|
||||
If the primary is correct and there is a trusted block that has not expired,
|
||||
then whenever the algorithm terminates, it reports "success".
|
||||
|
||||
[LCV-DIST-LIVE.1::SUCCESS-CORR-PRIMARY-CHAIN-OF-TRUST.1]
|
||||
*)
|
||||
SuccessOnCorrectPrimaryAndChainOfTrust ==
|
||||
(\E h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] = "StateVerified" /\ BC!InTrustingPeriod(blockchain[h])
|
||||
/\ state /= "working" /\ IS_PRIMARY_CORRECT) =>
|
||||
state = "finishedSuccess"
|
||||
|
||||
\* Lite Client Completeness: If header h was correctly generated by an instance
|
||||
\* of Tendermint consensus (and its age is less than the trusting period),
|
||||
\* then the lite client should eventually set trust(h) to true.
|
||||
\*
|
||||
\* Note that Completeness assumes that the lite client communicates with a correct full node.
|
||||
\*
|
||||
\* We decompose completeness into Termination (liveness) and Precision (safety).
|
||||
\* Once again, Precision is an inverse version of the safety property in Completeness,
|
||||
\* as A => B is logically equivalent to ~B => ~A.
|
||||
PrecisionInv ==
|
||||
(state = "finishedFailure")
|
||||
=> \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period
|
||||
\/ \E h \in DOMAIN fetchedLightBlocks:
|
||||
LET lightBlock == fetchedLightBlocks[h] IN
|
||||
\* the full node lied to the lite client about the block header
|
||||
\/ lightBlock.header /= blockchain[h]
|
||||
\* the full node lied to the lite client about the commits
|
||||
\/ lightBlock.Commits /= lightBlock.header.VS
|
||||
|
||||
\* the old invariant that was found to be buggy by TLC
|
||||
PrecisionBuggyInv ==
|
||||
(state = "finishedFailure")
|
||||
=> \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period
|
||||
\/ \E h \in DOMAIN fetchedLightBlocks:
|
||||
LET lightBlock == fetchedLightBlocks[h] IN
|
||||
\* the full node lied to the lite client about the block header
|
||||
lightBlock.header /= blockchain[h]
|
||||
|
||||
\* the worst complexity
|
||||
Complexity ==
|
||||
LET N == TARGET_HEIGHT - TRUSTED_HEIGHT + 1 IN
|
||||
state /= "working" =>
|
||||
(2 * nprobes <= N * (N - 1))
|
||||
|
||||
(*
|
||||
We omit termination, as the algorithm deadlocks in the end.
|
||||
So termination can be demonstrated by finding a deadlock.
|
||||
Of course, one has to analyze the deadlocked state and see that
|
||||
the algorithm has indeed terminated there.
|
||||
*)
|
||||
=============================================================================
|
||||
\* Modification History
|
||||
\* Last modified Fri Jun 26 12:08:28 CEST 2020 by igor
|
||||
\* Created Wed Oct 02 16:39:42 CEST 2019 by igor
|
||||
@@ -0,0 +1,493 @@
|
||||
-------------------------- MODULE Lightclient_003_draft ----------------------------
|
||||
(**
|
||||
* 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
|
||||
*)
|
||||
|
||||
EXTENDS Integers, FiniteSets
|
||||
|
||||
\* the parameters of Light Client
|
||||
CONSTANTS
|
||||
TRUSTED_HEIGHT,
|
||||
(* an index of the block header that the light client trusts by social consensus *)
|
||||
TARGET_HEIGHT,
|
||||
(* an index of the block header that the light client tries to verify *)
|
||||
TRUSTING_PERIOD,
|
||||
(* the period within which the validators are trusted *)
|
||||
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
|
||||
(* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
|
||||
from above (exclusive). Tendermint security model prescribes 1 / 3. *)
|
||||
|
||||
VARIABLES (* see TypeOK below for the variable types *)
|
||||
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 *)
|
||||
|
||||
(* the light store *)
|
||||
VARIABLES
|
||||
fetchedLightBlocks, (* a function from heights to LightBlocks *)
|
||||
lightBlockStatus, (* a function from heights to block statuses *)
|
||||
latestVerified (* the latest verified block *)
|
||||
|
||||
(* the variables of the lite client *)
|
||||
lcvars == <<localClock, state, nextHeight,
|
||||
fetchedLightBlocks, lightBlockStatus, latestVerified>>
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
InitMonitor(verified, current, pLocalClock, verdict) ==
|
||||
/\ prevVerified = verified
|
||||
/\ prevCurrent = current
|
||||
/\ prevLocalClock = pLocalClock
|
||||
/\ prevVerdict = verdict
|
||||
|
||||
NextMonitor(verified, current, pLocalClock, verdict) ==
|
||||
/\ prevVerified' = verified
|
||||
/\ prevCurrent' = current
|
||||
/\ prevLocalClock' = pLocalClock
|
||||
/\ prevVerdict' = verdict
|
||||
|
||||
|
||||
(******************* Blockchain instance ***********************************)
|
||||
|
||||
\* the parameters that are propagated into Blockchain
|
||||
CONSTANTS
|
||||
AllNodes
|
||||
(* a set of all nodes that can act as validators (correct and faulty) *)
|
||||
|
||||
\* the state variables of Blockchain, see Blockchain.tla for the details
|
||||
VARIABLES refClock, blockchain, Faulty
|
||||
|
||||
\* All the variables of Blockchain. For some reason, BC!vars does not work
|
||||
bcvars == <<refClock, blockchain, Faulty>>
|
||||
|
||||
(* Create an instance of Blockchain.
|
||||
We could write EXTENDS Blockchain, but then all the constants and state variables
|
||||
would be hidden inside the Blockchain module.
|
||||
*)
|
||||
ULTIMATE_HEIGHT == TARGET_HEIGHT + 1
|
||||
|
||||
BC == INSTANCE Blockchain_003_draft WITH
|
||||
refClock <- refClock, blockchain <- blockchain, Faulty <- Faulty
|
||||
|
||||
(************************** Lite client ************************************)
|
||||
|
||||
(* the heights on which the light client is working *)
|
||||
HEIGHTS == TRUSTED_HEIGHT..TARGET_HEIGHT
|
||||
|
||||
(* the control states of the lite client *)
|
||||
States == { "working", "finishedSuccess", "finishedFailure" }
|
||||
|
||||
\* The verification functions are implemented in the API
|
||||
API == INSTANCE LCVerificationApi_003_draft
|
||||
|
||||
|
||||
(*
|
||||
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
|
||||
/\ LET trustedBlock == blockchain[TRUSTED_HEIGHT]
|
||||
trustedLightBlock == [header |-> trustedBlock, Commits |-> AllNodes]
|
||||
IN
|
||||
\* initially, fetchedLightBlocks is a function of one element, i.e., TRUSTED_HEIGHT
|
||||
/\ fetchedLightBlocks = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock]
|
||||
\* initially, lightBlockStatus is a function of one element, i.e., TRUSTED_HEIGHT
|
||||
/\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"]
|
||||
\* the latest verified block the the trusted block
|
||||
/\ latestVerified = trustedLightBlock
|
||||
/\ InitMonitor(trustedLightBlock, trustedLightBlock, localClock, "SUCCESS")
|
||||
|
||||
\* block should contain a copy of the block from the reference chain, with a matching commit
|
||||
CopyLightBlockFromChain(block, height) ==
|
||||
LET ref == blockchain[height]
|
||||
lastCommit ==
|
||||
IF height < ULTIMATE_HEIGHT
|
||||
THEN blockchain[height + 1].lastCommit
|
||||
\* for the ultimate block, which we never use, as ULTIMATE_HEIGHT = TARGET_HEIGHT + 1
|
||||
ELSE blockchain[height].VS
|
||||
IN
|
||||
block = [header |-> ref, Commits |-> lastCommit]
|
||||
|
||||
\* Either the primary is correct and the block comes from the reference chain,
|
||||
\* or the block is produced by a faulty primary.
|
||||
\*
|
||||
\* [LCV-FUNC-FETCH.1::TLA.1]
|
||||
FetchLightBlockInto(block, height) ==
|
||||
IF IS_PRIMARY_CORRECT
|
||||
THEN CopyLightBlockFromChain(block, height)
|
||||
ELSE BC!IsLightBlockAllowedByDigitalSignatures(height, block)
|
||||
|
||||
\* add a block into the light store
|
||||
\*
|
||||
\* [LCV-FUNC-UPDATE.1::TLA.1]
|
||||
LightStoreUpdateBlocks(lightBlocks, block) ==
|
||||
LET ht == block.header.height IN
|
||||
[h \in DOMAIN lightBlocks \union {ht} |->
|
||||
IF h = ht THEN block ELSE lightBlocks[h]]
|
||||
|
||||
\* update the state of a light block
|
||||
\*
|
||||
\* [LCV-FUNC-UPDATE.1::TLA.1]
|
||||
LightStoreUpdateStates(statuses, ht, blockState) ==
|
||||
[h \in DOMAIN statuses \union {ht} |->
|
||||
IF h = ht THEN blockState ELSE statuses[h]]
|
||||
|
||||
\* Check, whether newHeight is a possible next height for the light client.
|
||||
\*
|
||||
\* [LCV-FUNC-SCHEDULE.1::TLA.1]
|
||||
CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) ==
|
||||
LET ht == pLatestVerified.header.height IN
|
||||
\/ /\ ht = pNextHeight
|
||||
/\ ht < pTargetHeight
|
||||
/\ pNextHeight < newHeight
|
||||
/\ newHeight <= pTargetHeight
|
||||
\/ /\ ht < pNextHeight
|
||||
/\ ht < pTargetHeight
|
||||
/\ ht < newHeight
|
||||
/\ newHeight < pNextHeight
|
||||
\/ /\ ht = pTargetHeight
|
||||
/\ newHeight = pTargetHeight
|
||||
|
||||
\* The loop of VerifyToTarget.
|
||||
\*
|
||||
\* [LCV-FUNC-MAIN.1::TLA-LOOP.1]
|
||||
VerifyToTargetLoop ==
|
||||
\* the loop condition is true
|
||||
/\ latestVerified.header.height < TARGET_HEIGHT
|
||||
\* pick a light block, which will be constrained later
|
||||
/\ \E current \in BC!LightBlocks:
|
||||
\* Get next LightBlock for verification
|
||||
/\ IF nextHeight \in DOMAIN fetchedLightBlocks
|
||||
THEN \* copy the block from the light store
|
||||
/\ current = fetchedLightBlocks[nextHeight]
|
||||
/\ UNCHANGED fetchedLightBlocks
|
||||
ELSE \* retrieve a light block and save it in the light store
|
||||
/\ FetchLightBlockInto(current, nextHeight)
|
||||
/\ fetchedLightBlocks' = LightStoreUpdateBlocks(fetchedLightBlocks, current)
|
||||
\* Record that one more probe has been done (for complexity and model checking)
|
||||
/\ nprobes' = nprobes + 1
|
||||
\* Verify the current block
|
||||
/\ LET verdict == API!ValidAndVerified(latestVerified, current, TRUE) IN
|
||||
NextMonitor(latestVerified, current, localClock, verdict) /\
|
||||
\* Decide whether/how to continue
|
||||
CASE verdict = "SUCCESS" ->
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified")
|
||||
/\ latestVerified' = current
|
||||
/\ state' =
|
||||
IF latestVerified'.header.height < TARGET_HEIGHT
|
||||
THEN "working"
|
||||
ELSE "finishedSuccess"
|
||||
/\ \E newHeight \in HEIGHTS:
|
||||
/\ CanScheduleTo(newHeight, current, nextHeight, TARGET_HEIGHT)
|
||||
/\ nextHeight' = newHeight
|
||||
|
||||
[] verdict = "NOT_ENOUGH_TRUST" ->
|
||||
(*
|
||||
do nothing: the light block current passed validation, but the validator
|
||||
set is too different to verify it. We keep the state of
|
||||
current at StateUnverified. For a later iteration, Schedule
|
||||
might decide to try verification of that light block again.
|
||||
*)
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateUnverified")
|
||||
/\ \E newHeight \in HEIGHTS:
|
||||
/\ CanScheduleTo(newHeight, latestVerified, nextHeight, TARGET_HEIGHT)
|
||||
/\ nextHeight' = newHeight
|
||||
/\ UNCHANGED <<latestVerified, state>>
|
||||
|
||||
[] OTHER ->
|
||||
\* verdict is some error code
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateFailed")
|
||||
/\ state' = "finishedFailure"
|
||||
/\ UNCHANGED <<latestVerified, nextHeight>>
|
||||
|
||||
\* The terminating condition of VerifyToTarget.
|
||||
\*
|
||||
\* [LCV-FUNC-MAIN.1::TLA-LOOPCOND.1]
|
||||
VerifyToTargetDone ==
|
||||
/\ latestVerified.header.height >= TARGET_HEIGHT
|
||||
/\ state' = "finishedSuccess"
|
||||
/\ UNCHANGED <<nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, latestVerified>>
|
||||
/\ UNCHANGED <<prevVerified, prevCurrent, prevLocalClock, prevVerdict>>
|
||||
|
||||
(*
|
||||
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 ==
|
||||
\* the blockchain is initialized immediately to the ULTIMATE_HEIGHT
|
||||
/\ BC!InitToHeight(FAULTY_RATIO)
|
||||
\* the light client starts
|
||||
/\ LCInit
|
||||
|
||||
(*
|
||||
The system step is very simple.
|
||||
The light client is either executing VerifyToTarget, or it has terminated.
|
||||
(In the latter case, a model checker reports a deadlock.)
|
||||
Simultaneously, the global clock may advance.
|
||||
*)
|
||||
Next ==
|
||||
/\ state = "working"
|
||||
/\ VerifyToTargetLoop \/ VerifyToTargetDone
|
||||
/\ AdvanceClocks
|
||||
|
||||
(************************* Types ******************************************)
|
||||
TypeOK ==
|
||||
/\ state \in States
|
||||
/\ localClock \in Nat
|
||||
/\ refClock \in Nat
|
||||
/\ nextHeight \in HEIGHTS
|
||||
/\ latestVerified \in BC!LightBlocks
|
||||
/\ \E HS \in SUBSET HEIGHTS:
|
||||
/\ fetchedLightBlocks \in [HS -> BC!LightBlocks]
|
||||
/\ lightBlockStatus
|
||||
\in [HS -> {"StateVerified", "StateUnverified", "StateFailed"}]
|
||||
|
||||
(************************* Properties ******************************************)
|
||||
|
||||
(* The properties to check *)
|
||||
\* this invariant candidate is false
|
||||
NeverFinish ==
|
||||
state = "working"
|
||||
|
||||
\* this invariant candidate is false
|
||||
NeverFinishNegative ==
|
||||
state /= "finishedFailure"
|
||||
|
||||
\* This invariant holds true, when the primary is correct.
|
||||
\* This invariant candidate is false when the primary is faulty.
|
||||
NeverFinishNegativeWhenTrusted ==
|
||||
BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
=> state /= "finishedFailure"
|
||||
|
||||
\* this invariant candidate is false
|
||||
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.
|
||||
|
||||
It is always the case that every verified header in LightStore was generated by
|
||||
an instance of Tendermint consensus.
|
||||
|
||||
[LCV-DIST-SAFE.1::CORRECTNESS-INV.1]
|
||||
*)
|
||||
CorrectnessInv ==
|
||||
\A h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] = "StateVerified" =>
|
||||
fetchedLightBlocks[h].header = blockchain[h]
|
||||
|
||||
(**
|
||||
No faulty block was used to construct a proof. This invariant holds,
|
||||
only if FAULTY_RATIO < 1/3.
|
||||
*)
|
||||
NoTrustOnFaultyBlockInv ==
|
||||
(state = "finishedSuccess"
|
||||
/\ fetchedLightBlocks[TARGET_HEIGHT].header = blockchain[TARGET_HEIGHT])
|
||||
=> CorrectnessInv
|
||||
|
||||
(**
|
||||
Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "SUCCESS" pairwise
|
||||
This property is easily violated, whenever a header cannot be trusted anymore.
|
||||
*)
|
||||
StoredHeadersAreVerifiedInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers
|
||||
\/ lh >= rh
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "SUCCESS" = API!ValidAndVerified(fetchedLightBlocks[lh],
|
||||
fetchedLightBlocks[rh], FALSE)
|
||||
|
||||
\* 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"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers
|
||||
\/ lh >= rh
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "SUCCESS" = API!ValidAndVerified(fetchedLightBlocks[lh],
|
||||
fetchedLightBlocks[rh], FALSE)
|
||||
\* or the left header is outside the trusting period, so no guarantees
|
||||
\/ ~API!InTrustingPeriodLocal(fetchedLightBlocks[lh].header)
|
||||
|
||||
(**
|
||||
* An improved version of StoredHeadersAreSoundOrNotTrusted,
|
||||
* checking the property only for the verified headers.
|
||||
* This invariant holds true if CLOCK_DRIFT <= REAL_CLOCK_DRIFT.
|
||||
*)
|
||||
ProofOfChainOfTrustInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks:
|
||||
\* for every pair of stored headers that have been verified
|
||||
\/ lh >= rh
|
||||
\/ lightBlockStatus[lh] = "StateUnverified"
|
||||
\/ lightBlockStatus[rh] = "StateUnverified"
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh /\ lightBlockStatus[mh] = "StateVerified"
|
||||
\* or the left header is outside the trusting period, so no guarantees
|
||||
\/ ~(API!InTrustingPeriodLocal(fetchedLightBlocks[lh].header))
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "SUCCESS" = API!ValidAndVerified(fetchedLightBlocks[lh],
|
||||
fetchedLightBlocks[rh], FALSE)
|
||||
|
||||
(**
|
||||
* When the light client terminates, there are no failed blocks. (Otherwise, someone lied to us.)
|
||||
*)
|
||||
NoFailedBlocksOnSuccessInv ==
|
||||
state = "finishedSuccess" =>
|
||||
\A h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] /= "StateFailed"
|
||||
|
||||
\* This property states that whenever the light client finishes with a positive outcome,
|
||||
\* the trusted header is still within the trusting period.
|
||||
\* We expect this property to be violated. And Apalache shows us a counterexample.
|
||||
PositiveBeforeTrustedHeaderExpires ==
|
||||
(state = "finishedSuccess") =>
|
||||
BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
|
||||
\* If the primary is correct and the initial trusted block has not expired,
|
||||
\* then whenever the algorithm terminates, it reports "success".
|
||||
\* This property fails.
|
||||
CorrectPrimaryAndTimeliness ==
|
||||
(BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
/\ state /= "working" /\ IS_PRIMARY_CORRECT) =>
|
||||
state = "finishedSuccess"
|
||||
|
||||
(**
|
||||
If the primary is correct and there is a trusted block that has not expired,
|
||||
then whenever the algorithm terminates, it reports "success".
|
||||
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]
|
||||
*)
|
||||
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) =>
|
||||
state = "finishedSuccess"
|
||||
|
||||
\* Lite Client Completeness: If header h was correctly generated by an instance
|
||||
\* of Tendermint consensus (and its age is less than the trusting period),
|
||||
\* then the lite client should eventually set trust(h) to true.
|
||||
\*
|
||||
\* Note that Completeness assumes that the lite client communicates with a correct full node.
|
||||
\*
|
||||
\* We decompose completeness into Termination (liveness) and Precision (safety).
|
||||
\* Once again, Precision is an inverse version of the safety property in Completeness,
|
||||
\* as A => B is logically equivalent to ~B => ~A.
|
||||
\*
|
||||
\* 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
|
||||
\/ \E h \in DOMAIN fetchedLightBlocks:
|
||||
LET lightBlock == fetchedLightBlocks[h] IN
|
||||
\* the full node lied to the lite client about the block header
|
||||
\/ lightBlock.header /= blockchain[h]
|
||||
\* the full node lied to the lite client about the commits
|
||||
\/ lightBlock.Commits /= lightBlock.header.VS
|
||||
|
||||
\* the old invariant that was found to be buggy by TLC
|
||||
PrecisionBuggyInv ==
|
||||
(state = "finishedFailure")
|
||||
=> \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period
|
||||
\/ \E h \in DOMAIN fetchedLightBlocks:
|
||||
LET lightBlock == fetchedLightBlocks[h] IN
|
||||
\* the full node lied to the lite client about the block header
|
||||
lightBlock.header /= blockchain[h]
|
||||
|
||||
\* the worst complexity
|
||||
Complexity ==
|
||||
LET N == TARGET_HEIGHT - TRUSTED_HEIGHT + 1 IN
|
||||
state /= "working" =>
|
||||
(2 * nprobes <= N * (N - 1))
|
||||
|
||||
(**
|
||||
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.
|
||||
Of course, one has to analyze the deadlocked state and see that
|
||||
the algorithm has indeed terminated there.
|
||||
*)
|
||||
=============================================================================
|
||||
\* Modification History
|
||||
\* Last modified Fri Jun 26 12:08:28 CEST 2020 by igor
|
||||
\* Created Wed Oct 02 16:39:42 CEST 2019 by igor
|
||||
@@ -0,0 +1,440 @@
|
||||
-------------------------- MODULE Lightclient_A_1 ----------------------------
|
||||
(**
|
||||
* A state-machine specification of the lite client, following the English spec:
|
||||
*
|
||||
* ./verification_001_published.md
|
||||
*)
|
||||
|
||||
EXTENDS Integers, FiniteSets
|
||||
|
||||
\* the parameters of Light Client
|
||||
CONSTANTS
|
||||
TRUSTED_HEIGHT,
|
||||
(* an index of the block header that the light client trusts by social consensus *)
|
||||
TARGET_HEIGHT,
|
||||
(* an index of the block header that the light client tries to verify *)
|
||||
TRUSTING_PERIOD,
|
||||
(* the period within which the validators are trusted *)
|
||||
IS_PRIMARY_CORRECT
|
||||
(* is primary correct? *)
|
||||
|
||||
VARIABLES (* see TypeOK below for the variable types *)
|
||||
state, (* the current state of the light client *)
|
||||
nextHeight, (* the next height to explore by the light client *)
|
||||
nprobes (* the lite client iteration, or the number of block tests *)
|
||||
|
||||
(* the light store *)
|
||||
VARIABLES
|
||||
fetchedLightBlocks, (* a function from heights to LightBlocks *)
|
||||
lightBlockStatus, (* a function from heights to block statuses *)
|
||||
latestVerified (* the latest verified block *)
|
||||
|
||||
(* the variables of the lite client *)
|
||||
lcvars == <<state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified>>
|
||||
|
||||
(******************* Blockchain instance ***********************************)
|
||||
|
||||
\* the parameters that are propagated into Blockchain
|
||||
CONSTANTS
|
||||
AllNodes
|
||||
(* a set of all nodes that can act as validators (correct and faulty) *)
|
||||
|
||||
\* the state variables of Blockchain, see Blockchain.tla for the details
|
||||
VARIABLES now, blockchain, Faulty
|
||||
|
||||
\* All the variables of Blockchain. For some reason, BC!vars does not work
|
||||
bcvars == <<now, blockchain, Faulty>>
|
||||
|
||||
(* Create an instance of Blockchain.
|
||||
We could write EXTENDS Blockchain, but then all the constants and state variables
|
||||
would be hidden inside the Blockchain module.
|
||||
*)
|
||||
ULTIMATE_HEIGHT == TARGET_HEIGHT + 1
|
||||
|
||||
BC == INSTANCE Blockchain_A_1 WITH
|
||||
now <- now, blockchain <- blockchain, Faulty <- Faulty
|
||||
|
||||
(************************** Lite client ************************************)
|
||||
|
||||
(* the heights on which the light client is working *)
|
||||
HEIGHTS == TRUSTED_HEIGHT..TARGET_HEIGHT
|
||||
|
||||
(* the control states of the lite client *)
|
||||
States == { "working", "finishedSuccess", "finishedFailure" }
|
||||
|
||||
(**
|
||||
Check the precondition of ValidAndVerified.
|
||||
|
||||
[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
|
||||
/\ untrusted.Commits \subseteq uhdr.VS
|
||||
/\ LET TP == Cardinality(uhdr.VS)
|
||||
SP == Cardinality(untrusted.Commits)
|
||||
IN
|
||||
3 * SP > 2 * TP
|
||||
/\ thdr.height + 1 = uhdr.height => thdr.NextVS = uhdr.VS
|
||||
(* As we do not have explicit hashes we ignore these three checks of the English spec:
|
||||
|
||||
1. "trusted.Commit is a commit is for the header trusted.Header,
|
||||
i.e. it contains the correct hash of the header".
|
||||
2. untrusted.Validators = hash(untrusted.Header.Validators)
|
||||
3. untrusted.NextValidators = hash(untrusted.Header.NextValidators)
|
||||
*)
|
||||
|
||||
(**
|
||||
* Check that the commits in an untrusted block form 1/3 of the next validators
|
||||
* in a trusted header.
|
||||
*)
|
||||
SignedByOneThirdOfTrusted(trusted, untrusted) ==
|
||||
LET TP == Cardinality(trusted.header.NextVS)
|
||||
SP == Cardinality(untrusted.Commits \intersect trusted.header.NextVS)
|
||||
IN
|
||||
3 * SP > TP
|
||||
|
||||
(**
|
||||
Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header.
|
||||
|
||||
[LCV-FUNC-VALID.1::TLA.1]
|
||||
*)
|
||||
ValidAndVerified(trusted, untrusted) ==
|
||||
IF ~ValidAndVerifiedPre(trusted, untrusted)
|
||||
THEN "FAILED_VERIFICATION"
|
||||
ELSE IF ~BC!InTrustingPeriod(untrusted.header)
|
||||
(* We leave the following test for the documentation purposes.
|
||||
The implementation should do this test, as signature verification may be slow.
|
||||
In the TLA+ specification, ValidAndVerified happens in no time.
|
||||
*)
|
||||
THEN "FAILED_TRUSTING_PERIOD"
|
||||
ELSE IF untrusted.header.height = trusted.header.height + 1
|
||||
\/ SignedByOneThirdOfTrusted(trusted, untrusted)
|
||||
THEN "OK"
|
||||
ELSE "CANNOT_VERIFY"
|
||||
|
||||
(*
|
||||
Initial states of the light client.
|
||||
Initially, only the trusted light block is present.
|
||||
*)
|
||||
LCInit ==
|
||||
/\ state = "working"
|
||||
/\ nextHeight = TARGET_HEIGHT
|
||||
/\ nprobes = 0 \* no tests have been done so far
|
||||
/\ LET trustedBlock == blockchain[TRUSTED_HEIGHT]
|
||||
trustedLightBlock == [header |-> trustedBlock, Commits |-> AllNodes]
|
||||
IN
|
||||
\* initially, fetchedLightBlocks is a function of one element, i.e., TRUSTED_HEIGHT
|
||||
/\ fetchedLightBlocks = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock]
|
||||
\* initially, lightBlockStatus is a function of one element, i.e., TRUSTED_HEIGHT
|
||||
/\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"]
|
||||
\* the latest verified block the the trusted block
|
||||
/\ latestVerified = trustedLightBlock
|
||||
|
||||
\* block should contain a copy of the block from the reference chain, with a matching commit
|
||||
CopyLightBlockFromChain(block, height) ==
|
||||
LET ref == blockchain[height]
|
||||
lastCommit ==
|
||||
IF height < ULTIMATE_HEIGHT
|
||||
THEN blockchain[height + 1].lastCommit
|
||||
\* for the ultimate block, which we never use, as ULTIMATE_HEIGHT = TARGET_HEIGHT + 1
|
||||
ELSE blockchain[height].VS
|
||||
IN
|
||||
block = [header |-> ref, Commits |-> lastCommit]
|
||||
|
||||
\* Either the primary is correct and the block comes from the reference chain,
|
||||
\* or the block is produced by a faulty primary.
|
||||
\*
|
||||
\* [LCV-FUNC-FETCH.1::TLA.1]
|
||||
FetchLightBlockInto(block, height) ==
|
||||
IF IS_PRIMARY_CORRECT
|
||||
THEN CopyLightBlockFromChain(block, height)
|
||||
ELSE BC!IsLightBlockAllowedByDigitalSignatures(height, block)
|
||||
|
||||
\* add a block into the light store
|
||||
\*
|
||||
\* [LCV-FUNC-UPDATE.1::TLA.1]
|
||||
LightStoreUpdateBlocks(lightBlocks, block) ==
|
||||
LET ht == block.header.height IN
|
||||
[h \in DOMAIN lightBlocks \union {ht} |->
|
||||
IF h = ht THEN block ELSE lightBlocks[h]]
|
||||
|
||||
\* update the state of a light block
|
||||
\*
|
||||
\* [LCV-FUNC-UPDATE.1::TLA.1]
|
||||
LightStoreUpdateStates(statuses, ht, blockState) ==
|
||||
[h \in DOMAIN statuses \union {ht} |->
|
||||
IF h = ht THEN blockState ELSE statuses[h]]
|
||||
|
||||
\* Check, whether newHeight is a possible next height for the light client.
|
||||
\*
|
||||
\* [LCV-FUNC-SCHEDULE.1::TLA.1]
|
||||
CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) ==
|
||||
LET ht == pLatestVerified.header.height IN
|
||||
\/ /\ ht = pNextHeight
|
||||
/\ ht < pTargetHeight
|
||||
/\ pNextHeight < newHeight
|
||||
/\ newHeight <= pTargetHeight
|
||||
\/ /\ ht < pNextHeight
|
||||
/\ ht < pTargetHeight
|
||||
/\ ht < newHeight
|
||||
/\ newHeight < pNextHeight
|
||||
\/ /\ ht = pTargetHeight
|
||||
/\ newHeight = pTargetHeight
|
||||
|
||||
\* The loop of VerifyToTarget.
|
||||
\*
|
||||
\* [LCV-FUNC-MAIN.1::TLA-LOOP.1]
|
||||
VerifyToTargetLoop ==
|
||||
\* the loop condition is true
|
||||
/\ latestVerified.header.height < TARGET_HEIGHT
|
||||
\* pick a light block, which will be constrained later
|
||||
/\ \E current \in BC!LightBlocks:
|
||||
\* Get next LightBlock for verification
|
||||
/\ IF nextHeight \in DOMAIN fetchedLightBlocks
|
||||
THEN \* copy the block from the light store
|
||||
/\ current = fetchedLightBlocks[nextHeight]
|
||||
/\ UNCHANGED fetchedLightBlocks
|
||||
ELSE \* retrieve a light block and save it in the light store
|
||||
/\ FetchLightBlockInto(current, nextHeight)
|
||||
/\ fetchedLightBlocks' = LightStoreUpdateBlocks(fetchedLightBlocks, current)
|
||||
\* Record that one more probe has been done (for complexity and model checking)
|
||||
/\ nprobes' = nprobes + 1
|
||||
\* Verify the current block
|
||||
/\ LET verdict == ValidAndVerified(latestVerified, current) IN
|
||||
\* Decide whether/how to continue
|
||||
CASE verdict = "OK" ->
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified")
|
||||
/\ latestVerified' = current
|
||||
/\ state' =
|
||||
IF latestVerified'.header.height < TARGET_HEIGHT
|
||||
THEN "working"
|
||||
ELSE "finishedSuccess"
|
||||
/\ \E newHeight \in HEIGHTS:
|
||||
/\ CanScheduleTo(newHeight, current, nextHeight, TARGET_HEIGHT)
|
||||
/\ nextHeight' = newHeight
|
||||
|
||||
[] verdict = "CANNOT_VERIFY" ->
|
||||
(*
|
||||
do nothing: the light block current passed validation, but the validator
|
||||
set is too different to verify it. We keep the state of
|
||||
current at StateUnverified. For a later iteration, Schedule
|
||||
might decide to try verification of that light block again.
|
||||
*)
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateUnverified")
|
||||
/\ \E newHeight \in HEIGHTS:
|
||||
/\ CanScheduleTo(newHeight, latestVerified, nextHeight, TARGET_HEIGHT)
|
||||
/\ nextHeight' = newHeight
|
||||
/\ UNCHANGED <<latestVerified, state>>
|
||||
|
||||
[] OTHER ->
|
||||
\* verdict is some error code
|
||||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateFailed")
|
||||
/\ state' = "finishedFailure"
|
||||
/\ UNCHANGED <<latestVerified, nextHeight>>
|
||||
|
||||
\* The terminating condition of VerifyToTarget.
|
||||
\*
|
||||
\* [LCV-FUNC-MAIN.1::TLA-LOOPCOND.1]
|
||||
VerifyToTargetDone ==
|
||||
/\ latestVerified.header.height >= TARGET_HEIGHT
|
||||
/\ state' = "finishedSuccess"
|
||||
/\ UNCHANGED <<nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, latestVerified>>
|
||||
|
||||
(********************* Lite client + Blockchain *******************)
|
||||
Init ==
|
||||
\* the blockchain is initialized immediately to the ULTIMATE_HEIGHT
|
||||
/\ BC!InitToHeight
|
||||
\* the light client starts
|
||||
/\ LCInit
|
||||
|
||||
(*
|
||||
The system step is very simple.
|
||||
The light client is either executing VerifyToTarget, or it has terminated.
|
||||
(In the latter case, a model checker reports a deadlock.)
|
||||
Simultaneously, the global clock may advance.
|
||||
*)
|
||||
Next ==
|
||||
/\ state = "working"
|
||||
/\ VerifyToTargetLoop \/ VerifyToTargetDone
|
||||
/\ BC!AdvanceTime \* the global clock is advanced by zero or more time units
|
||||
|
||||
(************************* Types ******************************************)
|
||||
TypeOK ==
|
||||
/\ state \in States
|
||||
/\ nextHeight \in HEIGHTS
|
||||
/\ latestVerified \in BC!LightBlocks
|
||||
/\ \E HS \in SUBSET HEIGHTS:
|
||||
/\ fetchedLightBlocks \in [HS -> BC!LightBlocks]
|
||||
/\ lightBlockStatus
|
||||
\in [HS -> {"StateVerified", "StateUnverified", "StateFailed"}]
|
||||
|
||||
(************************* Properties ******************************************)
|
||||
|
||||
(* The properties to check *)
|
||||
\* this invariant candidate is false
|
||||
NeverFinish ==
|
||||
state = "working"
|
||||
|
||||
\* this invariant candidate is false
|
||||
NeverFinishNegative ==
|
||||
state /= "finishedFailure"
|
||||
|
||||
\* This invariant holds true, when the primary is correct.
|
||||
\* This invariant candidate is false when the primary is faulty.
|
||||
NeverFinishNegativeWhenTrusted ==
|
||||
(*(minTrustedHeight <= TRUSTED_HEIGHT)*)
|
||||
BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
=> state /= "finishedFailure"
|
||||
|
||||
\* this invariant candidate is false
|
||||
NeverFinishPositive ==
|
||||
state /= "finishedSuccess"
|
||||
|
||||
(**
|
||||
Correctness states that all the obtained headers are exactly like in the blockchain.
|
||||
|
||||
It is always the case that every verified header in LightStore was generated by
|
||||
an instance of Tendermint consensus.
|
||||
|
||||
[LCV-DIST-SAFE.1::CORRECTNESS-INV.1]
|
||||
*)
|
||||
CorrectnessInv ==
|
||||
\A h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] = "StateVerified" =>
|
||||
fetchedLightBlocks[h].header = blockchain[h]
|
||||
|
||||
(**
|
||||
Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "OK" pairwise
|
||||
This property is easily violated, whenever a header cannot be trusted anymore.
|
||||
*)
|
||||
StoredHeadersAreVerifiedInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers
|
||||
\/ lh >= rh
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
|
||||
|
||||
\* An improved version of StoredHeadersAreSound, assuming that a header may be not trusted.
|
||||
\* This invariant candidate is also violated,
|
||||
\* as there may be some unverified blocks left in the middle.
|
||||
StoredHeadersAreVerifiedOrNotTrustedInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers
|
||||
\/ lh >= rh
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
|
||||
\* or the left header is outside the trusting period, so no guarantees
|
||||
\/ ~BC!InTrustingPeriod(fetchedLightBlocks[lh].header)
|
||||
|
||||
(**
|
||||
* An improved version of StoredHeadersAreSoundOrNotTrusted,
|
||||
* checking the property only for the verified headers.
|
||||
* This invariant holds true.
|
||||
*)
|
||||
ProofOfChainOfTrustInv ==
|
||||
state = "finishedSuccess"
|
||||
=>
|
||||
\A lh, rh \in DOMAIN fetchedLightBlocks:
|
||||
\* for every pair of stored headers that have been verified
|
||||
\/ lh >= rh
|
||||
\/ lightBlockStatus[lh] = "StateUnverified"
|
||||
\/ lightBlockStatus[rh] = "StateUnverified"
|
||||
\* either there is a header between them
|
||||
\/ \E mh \in DOMAIN fetchedLightBlocks:
|
||||
lh < mh /\ mh < rh /\ lightBlockStatus[mh] = "StateVerified"
|
||||
\* or the left header is outside the trusting period, so no guarantees
|
||||
\/ ~(BC!InTrustingPeriod(fetchedLightBlocks[lh].header))
|
||||
\* or we can verify the right one using the left one
|
||||
\/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
|
||||
|
||||
(**
|
||||
* When the light client terminates, there are no failed blocks. (Otherwise, someone lied to us.)
|
||||
*)
|
||||
NoFailedBlocksOnSuccessInv ==
|
||||
state = "finishedSuccess" =>
|
||||
\A h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] /= "StateFailed"
|
||||
|
||||
\* This property states that whenever the light client finishes with a positive outcome,
|
||||
\* the trusted header is still within the trusting period.
|
||||
\* We expect this property to be violated. And Apalache shows us a counterexample.
|
||||
PositiveBeforeTrustedHeaderExpires ==
|
||||
(state = "finishedSuccess") => BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
|
||||
\* If the primary is correct and the initial trusted block has not expired,
|
||||
\* then whenever the algorithm terminates, it reports "success"
|
||||
CorrectPrimaryAndTimeliness ==
|
||||
(BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT])
|
||||
/\ state /= "working" /\ IS_PRIMARY_CORRECT) =>
|
||||
state = "finishedSuccess"
|
||||
|
||||
(**
|
||||
If the primary is correct and there is a trusted block that has not expired,
|
||||
then whenever the algorithm terminates, it reports "success".
|
||||
|
||||
[LCV-DIST-LIVE.1::SUCCESS-CORR-PRIMARY-CHAIN-OF-TRUST.1]
|
||||
*)
|
||||
SuccessOnCorrectPrimaryAndChainOfTrust ==
|
||||
(\E h \in DOMAIN fetchedLightBlocks:
|
||||
lightBlockStatus[h] = "StateVerified" /\ BC!InTrustingPeriod(blockchain[h])
|
||||
/\ state /= "working" /\ IS_PRIMARY_CORRECT) =>
|
||||
state = "finishedSuccess"
|
||||
|
||||
\* Lite Client Completeness: If header h was correctly generated by an instance
|
||||
\* of Tendermint consensus (and its age is less than the trusting period),
|
||||
\* then the lite client should eventually set trust(h) to true.
|
||||
\*
|
||||
\* Note that Completeness assumes that the lite client communicates with a correct full node.
|
||||
\*
|
||||
\* We decompose completeness into Termination (liveness) and Precision (safety).
|
||||
\* Once again, Precision is an inverse version of the safety property in Completeness,
|
||||
\* as A => B is logically equivalent to ~B => ~A.
|
||||
PrecisionInv ==
|
||||
(state = "finishedFailure")
|
||||
=> \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period
|
||||
\/ \E h \in DOMAIN fetchedLightBlocks:
|
||||
LET lightBlock == fetchedLightBlocks[h] IN
|
||||
\* the full node lied to the lite client about the block header
|
||||
\/ lightBlock.header /= blockchain[h]
|
||||
\* the full node lied to the lite client about the commits
|
||||
\/ lightBlock.Commits /= lightBlock.header.VS
|
||||
|
||||
\* the old invariant that was found to be buggy by TLC
|
||||
PrecisionBuggyInv ==
|
||||
(state = "finishedFailure")
|
||||
=> \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period
|
||||
\/ \E h \in DOMAIN fetchedLightBlocks:
|
||||
LET lightBlock == fetchedLightBlocks[h] IN
|
||||
\* the full node lied to the lite client about the block header
|
||||
lightBlock.header /= blockchain[h]
|
||||
|
||||
\* the worst complexity
|
||||
Complexity ==
|
||||
LET N == TARGET_HEIGHT - TRUSTED_HEIGHT + 1 IN
|
||||
state /= "working" =>
|
||||
(2 * nprobes <= N * (N - 1))
|
||||
|
||||
(*
|
||||
We omit termination, as the algorithm deadlocks in the end.
|
||||
So termination can be demonstrated by finding a deadlock.
|
||||
Of course, one has to analyze the deadlocked state and see that
|
||||
the algorithm has indeed terminated there.
|
||||
*)
|
||||
=============================================================================
|
||||
\* Modification History
|
||||
\* Last modified Fri Jun 26 12:08:28 CEST 2020 by igor
|
||||
\* Created Wed Oct 02 16:39:42 CEST 2019 by igor
|
||||
@@ -0,0 +1,26 @@
|
||||
---------------------------- MODULE MC4_3_correct ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 3
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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
|
||||
==============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
---------------------------- MODULE MC4_3_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 3
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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,
|
||||
localClock,
|
||||
refClock, blockchain, Faulty
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
INSTANCE Lightclient_003_draft
|
||||
==============================================================================
|
||||
@@ -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
|
||||
============================================================================
|
||||
@@ -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
|
||||
==============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
---------------------------- MODULE MC4_4_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 4
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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,
|
||||
localClock,
|
||||
refClock, blockchain, Faulty
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
INSTANCE Lightclient_003_draft
|
||||
==============================================================================
|
||||
@@ -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
|
||||
==============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC4_5_correct ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 5
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC4_5_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 5
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
IS_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, 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
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC4_6_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 6
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
IS_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,
|
||||
localClock,
|
||||
refClock, blockchain, Faulty
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
INSTANCE Lightclient_003_draft
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC4_7_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 7
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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,
|
||||
localClock,
|
||||
refClock, blockchain, Faulty
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
INSTANCE Lightclient_003_draft
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC5_5_correct ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4", "n5"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 5
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------- MODULE MC5_5_correct_peer_two_thirds_faulty ----------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4", "n5"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 5
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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, 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
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
----------------- 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, 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
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
----------------- MODULE MC5_5_faulty_peer_two_thirds_faulty ---------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4", "n5"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 5
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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, 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
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC5_7_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4", "n5"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 7
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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,
|
||||
localClock,
|
||||
refClock, blockchain, Faulty
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
INSTANCE Lightclient_003_draft
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC7_5_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4", "n5", "n6", "n7"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 5
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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,
|
||||
localClock,
|
||||
refClock, blockchain, Faulty
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
INSTANCE Lightclient_003_draft
|
||||
============================================================================
|
||||
@@ -0,0 +1,26 @@
|
||||
------------------------- MODULE MC7_7_faulty ---------------------------
|
||||
|
||||
AllNodes == {"n1", "n2", "n3", "n4", "n5", "n6", "n7"}
|
||||
TRUSTED_HEIGHT == 1
|
||||
TARGET_HEIGHT == 7
|
||||
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
|
||||
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,
|
||||
localClock,
|
||||
refClock, blockchain, Faulty
|
||||
|
||||
(* the light client previous state components, used for monitoring *)
|
||||
VARIABLES
|
||||
prevVerified,
|
||||
prevCurrent,
|
||||
prevLocalClock,
|
||||
prevVerdict
|
||||
|
||||
INSTANCE Lightclient_003_draft
|
||||
============================================================================
|
||||
@@ -0,0 +1,577 @@
|
||||
---
|
||||
order: 1
|
||||
parent:
|
||||
title: Verification
|
||||
order: 2
|
||||
---
|
||||
# Core Verification
|
||||
|
||||
## Problem statement
|
||||
|
||||
We assume that the light client knows a (base) header `inithead` it trusts (by social consensus or because
|
||||
the light client has decided to trust the header before). The goal is to check whether another header
|
||||
`newhead` can be trusted based on the data in `inithead`.
|
||||
|
||||
The correctness of the protocol is based on the assumption that `inithead` was generated by an instance of
|
||||
Tendermint consensus.
|
||||
|
||||
### Failure Model
|
||||
|
||||
For the purpose of the following definitions we assume that there exists a function
|
||||
`validators` that returns the corresponding validator set for the given hash.
|
||||
|
||||
The light client protocol is defined with respect to the following failure model:
|
||||
|
||||
Given a known bound `TRUSTED_PERIOD`, and a block `b` with header `h` generated at time `Time`
|
||||
(i.e. `h.Time = Time`), a set of validators that hold more than 2/3 of the voting power
|
||||
in `validators(b.Header.NextValidatorsHash)` is correct until time `b.Header.Time + TRUSTED_PERIOD`.
|
||||
|
||||
*Assumption*: "correct" is defined w.r.t. realtime (some Newtonian global notion of time, i.e., wall time),
|
||||
while `Header.Time` corresponds to the [BFT time](../consensus/bft-time.md). In this note, we assume that clocks of correct processes
|
||||
are synchronized (for example using NTP), and therefore there is bounded clock drift (`CLOCK_DRIFT`) between local clocks and
|
||||
BFT time. More precisely, for every correct light client process and every `header.Time` (i.e. BFT Time, for a header correctly
|
||||
generated by the Tendermint consensus), the following inequality holds: `Header.Time < now + CLOCK_DRIFT`,
|
||||
where `now` corresponds to the system clock at the light client process.
|
||||
|
||||
Furthermore, we assume that `TRUSTED_PERIOD` is (several) order of magnitude bigger than `CLOCK_DRIFT` (`TRUSTED_PERIOD >> CLOCK_DRIFT`),
|
||||
as `CLOCK_DRIFT` (using NTP) is in the order of milliseconds and `TRUSTED_PERIOD` is in the order of weeks.
|
||||
|
||||
We expect a light client process defined in this document to be used in the context in which there is some
|
||||
larger period during which misbehaving validators can be detected and punished (we normally refer to it as `UNBONDING_PERIOD`
|
||||
due to the "bonding" mechanism in modern proof of stake systems). Furthermore, we assume that
|
||||
`TRUSTED_PERIOD < UNBONDING_PERIOD` and that they are normally of the same order of magnitude, for example
|
||||
`TRUSTED_PERIOD = UNBONDING_PERIOD / 2`.
|
||||
|
||||
The specification in this document considers an implementation of the light client under the Failure Model defined above.
|
||||
Mechanisms like `fork accountability` and `evidence submission` are defined in the context of `UNBONDING_PERIOD` and
|
||||
they incentivize validators to follow the protocol specification defined in this document. If they don't,
|
||||
and we have 1/3 (or more) faulty validators, safety may be violated. Our approach then is
|
||||
to *detect* these cases (after the fact), and take suitable repair actions (automatic and social).
|
||||
This is discussed in document on [Fork accountability](./accountability.md).
|
||||
|
||||
The term "trusted" above indicates that the correctness of the protocol depends on
|
||||
this assumption. It is in the responsibility of the user that runs the light client to make sure that the risk
|
||||
of trusting a corrupted/forged `inithead` is negligible.
|
||||
|
||||
*Remark*: This failure model might change to a hybrid version that takes heights into account in the future.
|
||||
|
||||
### High Level Solution
|
||||
|
||||
Upon initialization, the light client is given a header `inithead` it trusts (by
|
||||
social consensus). When a light clients sees a new signed header `snh`, it has to decide whether to trust the new
|
||||
header. Trust can be obtained by (possibly) the combination of three methods.
|
||||
|
||||
1. **Uninterrupted sequence of headers.** Given a trusted header `h` and an untrusted header `h1`,
|
||||
the light client trusts a header `h1` if it trusts all headers in between `h` and `h1`.
|
||||
|
||||
2. **Trusted period.** Given a trusted header `h`, an untrusted header `h1 > h` and `TRUSTED_PERIOD` during which
|
||||
the failure model holds, we can check whether at least one validator, that has been continuously correct
|
||||
from `h.Time` until now, has signed `h1`. If this is the case, we can trust `h1`.
|
||||
|
||||
3. **Bisection.** If a check according to 2. (trusted period) fails, the light client can try to
|
||||
obtain a header `hp` whose height lies between `h` and `h1` in order to check whether `h` can be used to
|
||||
get trust for `hp`, and `hp` can be used to get trust for `snh`. If this is the case we can trust `h1`;
|
||||
if not, we continue recursively until either we found set of headers that can build (transitively) trust relation
|
||||
between `h` and `h1`, or we failed as two consecutive headers don't verify against each other.
|
||||
|
||||
## Definitions
|
||||
|
||||
### Data structures
|
||||
|
||||
In the following, only the details of the data structures needed for this specification are given.
|
||||
|
||||
```go
|
||||
type Header struct {
|
||||
Height int64
|
||||
Time Time // the chain time when the header (block) was generated
|
||||
|
||||
LastBlockID BlockID // prev block info
|
||||
ValidatorsHash []byte // hash of the validators for the current block
|
||||
NextValidatorsHash []byte // hash of the validators for the next block
|
||||
}
|
||||
|
||||
type SignedHeader struct {
|
||||
Header Header
|
||||
Commit Commit // commit for the given header
|
||||
}
|
||||
|
||||
type ValidatorSet struct {
|
||||
Validators []Validator
|
||||
TotalVotingPower int64
|
||||
}
|
||||
|
||||
type Validator struct {
|
||||
Address Address // validator address (we assume validator's addresses are unique)
|
||||
VotingPower int64 // validator's voting power
|
||||
}
|
||||
|
||||
type TrustedState {
|
||||
SignedHeader SignedHeader
|
||||
ValidatorSet ValidatorSet
|
||||
}
|
||||
```
|
||||
|
||||
### Functions
|
||||
|
||||
For the purpose of this light client specification, we assume that the Tendermint Full Node
|
||||
exposes the following functions over Tendermint RPC:
|
||||
|
||||
```go
|
||||
// returns signed header: Header with Commit, for the given height
|
||||
func Commit(height int64) (SignedHeader, error)
|
||||
|
||||
// returns validator set for the given height
|
||||
func Validators(height int64) (ValidatorSet, error)
|
||||
```
|
||||
|
||||
Furthermore, we assume the following auxiliary functions:
|
||||
|
||||
```go
|
||||
// returns true if the commit is for the header, ie. if it contains
|
||||
// the correct hash of the header; otherwise false
|
||||
func matchingCommit(header Header, commit Commit) bool
|
||||
|
||||
// returns the set of validators from the given validator set that
|
||||
// committed the block (that correctly signed the block)
|
||||
// it assumes signature verification so it can be computationally expensive
|
||||
func signers(commit Commit, validatorSet ValidatorSet) []Validator
|
||||
|
||||
// returns the voting power the validators in v1 have according to their voting power in set v2
|
||||
// it does not assume signature verification
|
||||
func votingPowerIn(v1 []Validator, v2 ValidatorSet) int64
|
||||
|
||||
// returns hash of the given validator set
|
||||
func hash(v2 ValidatorSet) []byte
|
||||
```
|
||||
|
||||
In the functions below we will be using `trustThreshold` as a parameter. For simplicity
|
||||
we assume that `trustThreshold` is a float between `1/3` and `2/3` and we will not be checking it
|
||||
in the pseudo-code.
|
||||
|
||||
**VerifySingle.** The function `VerifySingle` attempts to validate given untrusted header and the corresponding validator sets
|
||||
based on a given trusted state. It ensures that the trusted state is still within its trusted period,
|
||||
and that the untrusted header is within assumed `clockDrift` bound of the passed time `now`.
|
||||
Note that this function is not making external (RPC) calls to the full node; the whole logic is
|
||||
based on the local (given) state. This function is supposed to be used by the IBC handlers.
|
||||
|
||||
```go
|
||||
func VerifySingle(untrustedSh SignedHeader,
|
||||
untrustedVs ValidatorSet,
|
||||
untrustedNextVs ValidatorSet,
|
||||
trustedState TrustedState,
|
||||
trustThreshold float,
|
||||
trustingPeriod Duration,
|
||||
clockDrift Duration,
|
||||
now Time) (TrustedState, error) {
|
||||
|
||||
if untrustedSh.Header.Time > now + clockDrift {
|
||||
return (trustedState, ErrInvalidHeaderTime)
|
||||
}
|
||||
|
||||
trustedHeader = trustedState.SignedHeader.Header
|
||||
if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
|
||||
return (state, ErrHeaderNotWithinTrustedPeriod)
|
||||
}
|
||||
|
||||
// we assume that time it takes to execute verifySingle function
|
||||
// is several order of magnitudes smaller than trustingPeriod
|
||||
error = verifySingle(
|
||||
trustedState,
|
||||
untrustedSh,
|
||||
untrustedVs,
|
||||
untrustedNextVs,
|
||||
trustThreshold)
|
||||
|
||||
if error != nil return (state, error)
|
||||
|
||||
// the untrusted header is now trusted
|
||||
newTrustedState = TrustedState(untrustedSh, untrustedNextVs)
|
||||
return (newTrustedState, nil)
|
||||
}
|
||||
|
||||
// return true if header is within its light client trusted period; otherwise returns false
|
||||
func isWithinTrustedPeriod(header Header,
|
||||
trustingPeriod Duration,
|
||||
now Time) bool {
|
||||
|
||||
return header.Time + trustedPeriod > now
|
||||
}
|
||||
```
|
||||
|
||||
Note that in case `VerifySingle` returns without an error (untrusted header
|
||||
is successfully verified) then we have a guarantee that the transition of the trust
|
||||
from `trustedState` to `newTrustedState` happened during the trusted period of
|
||||
`trustedState.SignedHeader.Header`.
|
||||
|
||||
TODO: Explain what happens in case `VerifySingle` returns with an error.
|
||||
|
||||
**verifySingle.** The function `verifySingle` verifies a single untrusted header
|
||||
against a given trusted state. It includes all validations and signature verification.
|
||||
It is not publicly exposed since it does not check for header expiry (time constraints)
|
||||
and hence it's possible to use it incorrectly.
|
||||
|
||||
```go
|
||||
func verifySingle(trustedState TrustedState,
|
||||
untrustedSh SignedHeader,
|
||||
untrustedVs ValidatorSet,
|
||||
untrustedNextVs ValidatorSet,
|
||||
trustThreshold float) error {
|
||||
|
||||
untrustedHeader = untrustedSh.Header
|
||||
untrustedCommit = untrustedSh.Commit
|
||||
|
||||
trustedHeader = trustedState.SignedHeader.Header
|
||||
trustedVs = trustedState.ValidatorSet
|
||||
|
||||
if trustedHeader.Height >= untrustedHeader.Height return ErrNonIncreasingHeight
|
||||
if trustedHeader.Time >= untrustedHeader.Time return ErrNonIncreasingTime
|
||||
|
||||
// validate the untrusted header against its commit, vals, and next_vals
|
||||
error = validateSignedHeaderAndVals(untrustedSh, untrustedVs, untrustedNextVs)
|
||||
if error != nil return error
|
||||
|
||||
// check for adjacent headers
|
||||
if untrustedHeader.Height == trustedHeader.Height + 1 {
|
||||
if trustedHeader.NextValidatorsHash != untrustedHeader.ValidatorsHash {
|
||||
return ErrInvalidAdjacentHeaders
|
||||
}
|
||||
} else {
|
||||
error = verifyCommitTrusting(trustedVs, untrustedCommit, untrustedVs, trustThreshold)
|
||||
if error != nil return error
|
||||
}
|
||||
|
||||
// verify the untrusted commit
|
||||
return verifyCommitFull(untrustedVs, untrustedCommit)
|
||||
}
|
||||
|
||||
// returns nil if header and validator sets are consistent; otherwise returns error
|
||||
func validateSignedHeaderAndVals(signedHeader SignedHeader, vs ValidatorSet, nextVs ValidatorSet) error {
|
||||
header = signedHeader.Header
|
||||
if hash(vs) != header.ValidatorsHash return ErrInvalidValidatorSet
|
||||
if hash(nextVs) != header.NextValidatorsHash return ErrInvalidNextValidatorSet
|
||||
if !matchingCommit(header, signedHeader.Commit) return ErrInvalidCommitValue
|
||||
return nil
|
||||
}
|
||||
|
||||
// returns nil if at least single correst signer signed the commit; otherwise returns error
|
||||
func verifyCommitTrusting(trustedVs ValidatorSet,
|
||||
commit Commit,
|
||||
untrustedVs ValidatorSet,
|
||||
trustLevel float) error {
|
||||
|
||||
totalPower := trustedVs.TotalVotingPower
|
||||
signedPower := votingPowerIn(signers(commit, untrustedVs), trustedVs)
|
||||
|
||||
// check that the signers account for more than max(1/3, trustLevel) of the voting power
|
||||
// this ensures that there is at least single correct validator in the set of signers
|
||||
if signedPower < max(1/3, trustLevel) * totalPower return ErrInsufficientVotingPower
|
||||
return nil
|
||||
}
|
||||
|
||||
// returns nil if commit is signed by more than 2/3 of voting power of the given validator set
|
||||
// return error otherwise
|
||||
func verifyCommitFull(vs ValidatorSet, commit Commit) error {
|
||||
totalPower := vs.TotalVotingPower;
|
||||
signedPower := votingPowerIn(signers(commit, vs), vs)
|
||||
|
||||
// check the signers account for +2/3 of the voting power
|
||||
if signedPower * 3 <= totalPower * 2 return ErrInvalidCommit
|
||||
return nil
|
||||
}
|
||||
```
|
||||
|
||||
**VerifyHeaderAtHeight.** The function `VerifyHeaderAtHeight` captures high level
|
||||
logic, i.e., application call to the light client module to download and verify header
|
||||
for some height.
|
||||
|
||||
```go
|
||||
func VerifyHeaderAtHeight(untrustedHeight int64,
|
||||
trustedState TrustedState,
|
||||
trustThreshold float,
|
||||
trustingPeriod Duration,
|
||||
clockDrift Duration) (TrustedState, error)) {
|
||||
|
||||
trustedHeader := trustedState.SignedHeader.Header
|
||||
|
||||
now := System.Time()
|
||||
if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
|
||||
return (trustedState, ErrHeaderNotWithinTrustedPeriod)
|
||||
}
|
||||
|
||||
newTrustedState, err := VerifyBisection(untrustedHeight,
|
||||
trustedState,
|
||||
trustThreshold,
|
||||
trustingPeriod,
|
||||
clockDrift,
|
||||
now)
|
||||
|
||||
if err != nil return (trustedState, err)
|
||||
|
||||
now = System.Time()
|
||||
if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
|
||||
return (trustedState, ErrHeaderNotWithinTrustedPeriod)
|
||||
}
|
||||
|
||||
return (newTrustedState, err)
|
||||
}
|
||||
```
|
||||
|
||||
Note that in case `VerifyHeaderAtHeight` returns without an error (untrusted header
|
||||
is successfully verified) then we have a guarantee that the transition of the trust
|
||||
from `trustedState` to `newTrustedState` happened during the trusted period of
|
||||
`trustedState.SignedHeader.Header`.
|
||||
|
||||
In case `VerifyHeaderAtHeight` returns with an error, then either (i) the full node we are talking to is faulty
|
||||
or (ii) the trusted header has expired (it is outside its trusted period). In case (i) the full node is faulty so
|
||||
light client should disconnect and reinitialise with new peer. In the case (ii) as the trusted header has expired,
|
||||
we need to reinitialise light client with a new trusted header (that is within its trusted period),
|
||||
but we don't necessarily need to disconnect from the full node we are talking to (as we haven't observed full node misbehavior in this case).
|
||||
|
||||
**VerifyBisection.** The function `VerifyBisection` implements
|
||||
recursive logic for checking if it is possible building trust
|
||||
relationship between `trustedState` and untrusted header at the given height over
|
||||
finite set of (downloaded and verified) headers.
|
||||
|
||||
```go
|
||||
func VerifyBisection(untrustedHeight int64,
|
||||
trustedState TrustedState,
|
||||
trustThreshold float,
|
||||
trustingPeriod Duration,
|
||||
clockDrift Duration,
|
||||
now Time) (TrustedState, error) {
|
||||
|
||||
untrustedSh, error := Commit(untrustedHeight)
|
||||
if error != nil return (trustedState, ErrRequestFailed)
|
||||
|
||||
untrustedHeader = untrustedSh.Header
|
||||
|
||||
// note that we pass now during the recursive calls. This is fine as
|
||||
// all other untrusted headers we download during recursion will be
|
||||
// for a smaller heights, and therefore should happen before.
|
||||
if untrustedHeader.Time > now + clockDrift {
|
||||
return (trustedState, ErrInvalidHeaderTime)
|
||||
}
|
||||
|
||||
untrustedVs, error := Validators(untrustedHeight)
|
||||
if error != nil return (trustedState, ErrRequestFailed)
|
||||
|
||||
untrustedNextVs, error := Validators(untrustedHeight + 1)
|
||||
if error != nil return (trustedState, ErrRequestFailed)
|
||||
|
||||
error = verifySingle(
|
||||
trustedState,
|
||||
untrustedSh,
|
||||
untrustedVs,
|
||||
untrustedNextVs,
|
||||
trustThreshold)
|
||||
|
||||
if fatalError(error) return (trustedState, error)
|
||||
|
||||
if error == nil {
|
||||
// the untrusted header is now trusted.
|
||||
newTrustedState = TrustedState(untrustedSh, untrustedNextVs)
|
||||
return (newTrustedState, nil)
|
||||
}
|
||||
|
||||
// at this point in time we need to do bisection
|
||||
pivotHeight := ceil((trustedHeader.Height + untrustedHeight) / 2)
|
||||
|
||||
error, newTrustedState = VerifyBisection(pivotHeight,
|
||||
trustedState,
|
||||
trustThreshold,
|
||||
trustingPeriod,
|
||||
clockDrift,
|
||||
now)
|
||||
if error != nil return (newTrustedState, error)
|
||||
|
||||
return VerifyBisection(untrustedHeight,
|
||||
newTrustedState,
|
||||
trustThreshold,
|
||||
trustingPeriod,
|
||||
clockDrift,
|
||||
now)
|
||||
}
|
||||
|
||||
func fatalError(err) bool {
|
||||
return err == ErrHeaderNotWithinTrustedPeriod OR
|
||||
err == ErrInvalidAdjacentHeaders OR
|
||||
err == ErrNonIncreasingHeight OR
|
||||
err == ErrNonIncreasingTime OR
|
||||
err == ErrInvalidValidatorSet OR
|
||||
err == ErrInvalidNextValidatorSet OR
|
||||
err == ErrInvalidCommitValue OR
|
||||
err == ErrInvalidCommit
|
||||
}
|
||||
```
|
||||
|
||||
### The case `untrustedHeader.Height < trustedHeader.Height`
|
||||
|
||||
In the use case where someone tells the light client that application data that is relevant for it
|
||||
can be read in the block of height `k` and the light client trusts a more recent header, we can use the
|
||||
hashes to verify headers "down the chain." That is, we iterate down the heights and check the hashes in each step.
|
||||
|
||||
*Remark.* For the case were the light client trusts two headers `i` and `j` with `i < k < j`, we should
|
||||
discuss/experiment whether the forward or the backward method is more effective.
|
||||
|
||||
```go
|
||||
func VerifyHeaderBackwards(trustedHeader Header,
|
||||
untrustedHeader Header,
|
||||
trustingPeriod Duration,
|
||||
clockDrift Duration) error {
|
||||
|
||||
if untrustedHeader.Height >= trustedHeader.Height return ErrErrNonDecreasingHeight
|
||||
if untrustedHeader.Time >= trustedHeader.Time return ErrNonDecreasingTime
|
||||
|
||||
now := System.Time()
|
||||
if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
|
||||
return ErrHeaderNotWithinTrustedPeriod
|
||||
}
|
||||
|
||||
old := trustedHeader
|
||||
for i := trustedHeader.Height - 1; i > untrustedHeader.Height; i-- {
|
||||
untrustedSh, error := Commit(i)
|
||||
if error != nil return ErrRequestFailed
|
||||
|
||||
if (hash(untrustedSh.Header) != old.LastBlockID.Hash) {
|
||||
return ErrInvalidAdjacentHeaders
|
||||
}
|
||||
|
||||
old := untrustedSh.Header
|
||||
}
|
||||
|
||||
if hash(untrustedHeader) != old.LastBlockID.Hash {
|
||||
return ErrInvalidAdjacentHeaders
|
||||
}
|
||||
|
||||
now := System.Time()
|
||||
if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
|
||||
return ErrHeaderNotWithinTrustedPeriod
|
||||
}
|
||||
|
||||
return nil
|
||||
}
|
||||
```
|
||||
|
||||
*Assumption*: In the following, we assume that *untrusted_h.Header.height > trusted_h.Header.height*. We will quickly discuss the other case in the next section.
|
||||
|
||||
We consider the following set-up:
|
||||
|
||||
- the light client communicates with one full node
|
||||
- the light client locally stores all the headers that has passed basic verification and that are within light client trust period. In the pseudo code below we
|
||||
write *Store.Add(header)* for this. If a header failed to verify, then
|
||||
the full node we are talking to is faulty and we should disconnect from it and reinitialise with new peer.
|
||||
- If `CanTrust` returns *error*, then the light client has seen a forged header or the trusted header has expired (it is outside its trusted period).
|
||||
- In case of forged header, the full node is faulty so light client should disconnect and reinitialise with new peer. If the trusted header has expired,
|
||||
we need to reinitialise light client with new trusted header (that is within its trusted period), but we don't necessarily need to disconnect from the full node
|
||||
we are talking to (as we haven't observed full node misbehavior in this case).
|
||||
|
||||
## Correctness of the Light Client Protocols
|
||||
|
||||
### Definitions
|
||||
|
||||
- `TRUSTED_PERIOD`: trusted period
|
||||
- for realtime `t`, the predicate `correct(v,t)` is true if the validator `v`
|
||||
follows the protocol until time `t` (we will see about recovery later).
|
||||
- Validator fields. We will write a validator as a tuple `(v,p)` such that
|
||||
- `v` is the identifier (i.e., validator address; we assume identifiers are unique in each validator set)
|
||||
- `p` is its voting power
|
||||
- For each header `h`, we write `trust(h) = true` if the light client trusts `h`.
|
||||
|
||||
### Failure Model
|
||||
|
||||
If a block `b` with a header `h` is generated at time `Time` (i.e. `h.Time = Time`), then a set of validators that
|
||||
hold more than `2/3` of the voting power in `validators(h.NextValidatorsHash)` is correct until time
|
||||
`h.Time + TRUSTED_PERIOD`.
|
||||
|
||||
Formally,
|
||||
\[
|
||||
\sum_{(v,p) \in validators(h.NextValidatorsHash) \wedge correct(v,h.Time + TRUSTED_PERIOD)} p >
|
||||
2/3 \sum_{(v,p) \in validators(h.NextValidatorsHash)} p
|
||||
\]
|
||||
|
||||
The light client communicates with a full node and learns new headers. The goal is to locally decide whether to trust a header. Our implementation needs to ensure the following two properties:
|
||||
|
||||
- *Light Client Completeness*: If a header `h` was correctly generated by an instance of Tendermint consensus (and its age is less than the trusted period),
|
||||
then the light client should eventually set `trust(h)` to `true`.
|
||||
|
||||
- *Light Client Accuracy*: If a header `h` was *not generated* by an instance of Tendermint consensus, then the light client should never set `trust(h)` to true.
|
||||
|
||||
*Remark*: If in the course of the computation, the light client obtains certainty that some headers were forged by adversaries
|
||||
(that is were not generated by an instance of Tendermint consensus), it may submit (a subset of) the headers it has seen as evidence of misbehavior.
|
||||
|
||||
*Remark*: In Completeness we use "eventually", while in practice `trust(h)` should be set to true before `h.Time + TRUSTED_PERIOD`. If not, the header
|
||||
cannot be trusted because it is too old.
|
||||
|
||||
*Remark*: If a header `h` is marked with `trust(h)`, but it is too old at some point in time we denote with `now` (`h.Time + TRUSTED_PERIOD < now`),
|
||||
then the light client should set `trust(h)` to `false` again at time `now`.
|
||||
|
||||
*Assumption*: Initially, the light client has a header `inithead` that it trusts, that is, `inithead` was correctly generated by the Tendermint consensus.
|
||||
|
||||
To reason about the correctness, we may prove the following invariant.
|
||||
|
||||
*Verification Condition: light Client Invariant.*
|
||||
For each light client `l` and each header `h`:
|
||||
if `l` has set `trust(h) = true`,
|
||||
then validators that are correct until time `h.Time + TRUSTED_PERIOD` have more than two thirds of the voting power in `validators(h.NextValidatorsHash)`.
|
||||
|
||||
Formally,
|
||||
\[
|
||||
\sum_{(v,p) \in validators(h.NextValidatorsHash) \wedge correct(v,h.Time + TRUSTED_PERIOD)} p >
|
||||
2/3 \sum_{(v,p) \in validators(h.NextValidatorsHash)} p
|
||||
\]
|
||||
|
||||
*Remark.* To prove the invariant, we will have to prove that the light client only trusts headers that were correctly generated by Tendermint consensus.
|
||||
Then the formula above follows from the failure model.
|
||||
|
||||
## Details
|
||||
|
||||
**Observation 1.** If `h.Time + TRUSTED_PERIOD > now`, we trust the validator set `validators(h.NextValidatorsHash)`.
|
||||
|
||||
When we say we trust `validators(h.NextValidatorsHash)` we do `not` trust that each individual validator in `validators(h.NextValidatorsHash)`
|
||||
is correct, but we only trust the fact that less than `1/3` of them are faulty (more precisely, the faulty ones have less than `1/3` of the total voting power).
|
||||
|
||||
*`VerifySingle` correctness arguments*
|
||||
|
||||
Light Client Accuracy:
|
||||
|
||||
- Assume by contradiction that `untrustedHeader` was not generated correctly and the light client sets trust to true because `verifySingle` returns without error.
|
||||
- `trustedState` is trusted and sufficiently new
|
||||
- by the Failure Model, less than `1/3` of the voting power held by faulty validators => at least one correct validator `v` has signed `untrustedHeader`.
|
||||
- as `v` is correct up to now, it followed the Tendermint consensus protocol at least up to signing `untrustedHeader` => `untrustedHeader` was correctly generated.
|
||||
We arrive at the required contradiction.
|
||||
|
||||
Light Client Completeness:
|
||||
|
||||
- The check is successful if sufficiently many validators of `trustedState` are still validators in the height `untrustedHeader.Height` and signed `untrustedHeader`.
|
||||
- If `untrustedHeader.Height = trustedHeader.Height + 1`, and both headers were generated correctly, the test passes.
|
||||
|
||||
*Verification Condition:* We may need a Tendermint invariant stating that if `untrustedSignedHeader.Header.Height = trustedHeader.Height + 1` then
|
||||
`signers(untrustedSignedHeader.Commit) \subseteq validators(trustedHeader.NextValidatorsHash)`.
|
||||
|
||||
*Remark*: The variable `trustThreshold` can be used if the user believes that relying on one correct validator is not sufficient.
|
||||
However, in case of (frequent) changes in the validator set, the higher the `trustThreshold` is chosen, the more unlikely it becomes that
|
||||
`verifySingle` returns with an error for non-adjacent headers.
|
||||
|
||||
- `VerifyBisection` correctness arguments (sketch)*
|
||||
|
||||
Light Client Accuracy:
|
||||
|
||||
- Assume by contradiction that the header at `untrustedHeight` obtained from the full node was not generated correctly and
|
||||
the light client sets trust to true because `VerifyBisection` returns without an error.
|
||||
- `VerifyBisection` returns without error only if all calls to `verifySingle` in the recursion return without error (return `nil`).
|
||||
- Thus we have a sequence of headers that all satisfied the `verifySingle`
|
||||
- again a contradiction
|
||||
|
||||
light Client Completeness:
|
||||
|
||||
This is only ensured if upon `Commit(pivot)` the light client is always provided with a correctly generated header.
|
||||
|
||||
*Stalling*
|
||||
|
||||
With `VerifyBisection`, a faulty full node could stall a light client by creating a long sequence of headers that are queried one-by-one by the light client and look OK,
|
||||
before the light client eventually detects a problem. There are several ways to address this:
|
||||
|
||||
- Each call to `Commit` could be issued to a different full node
|
||||
- Instead of querying header by header, the light client tells a full node which header it trusts, and the height of the header it needs. The full node responds with
|
||||
the header along with a proof consisting of intermediate headers that the light client can use to verify. Roughly, `VerifyBisection` would then be executed at the full node.
|
||||
- We may set a timeout how long `VerifyBisection` may take.
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user