From 75c30a1b03bf18beabd92a2a562a326ccee5d374 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 22 Jul 2020 14:17:24 +0200 Subject: [PATCH 01/26] added todos --- docs/spec/lightclient/detection/detection.md | 110 ++++++++++++++++-- .../detection/req-ibc-detection.md | 23 ++++ .../lightclient/verification/verification.md | 5 +- 3 files changed, 129 insertions(+), 9 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 8c0664056..a54fb5549 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -1,5 +1,24 @@ ***This an unfinished draft. Comments are welcome!*** +## Decisions with Zarko + +- Generating a minimal proof of fork is too costly at the light client + - we do not know all lightblocks from the primary + - therefore there are many scenarios. we might even need to ask + the primary again for additional lightblocks to isolate the + branch. As the main goal is to catch misbehavior of the primary, + evidence generation and punishment must not depend on their + cooperation. + + +- proof of fork is a trace of lightblocks that verifies a block + different from the one the full node knows + +- For each secondary, we check the primary against one secondary +- We do not check secondary against secondary +- the reason is that the attack is via the primary. We only try to + catch if the primary installs a bad light block + ## TODOs - the main logic, i.e., describing what happens when the function of @@ -14,6 +33,12 @@ - clarify EXPIRED case. Can we always punish? Can we give sufficient conditions. + +- Discussion with end-user API in the case of + - user uses trusted blocks only + - user uses verified blocks (may need to roll back) + +- # Fork detector @@ -365,8 +390,39 @@ and the following transition invariant ## Solution +### Data Structures + +```go +type LightNodeProofOfFork struct { + TrustedBlock TrustedBlockInfo + ConflictingTrace LightStore +} + +// info about the LC's last trusted block +type TrustedBlockInfo struct { + Height int + BlockID BlockID +} +``` + +#### **[LCV-DATA-POFSTORE.1]**: + +Proofs of Forks are stored in a structure which stores all proofs +generated during detection + +```go +type PoFStore struct { + ... +} +``` +The following is defined at **[LCV-DATA-LIGHTBLOCK.1]**: +```go +// full light block (SignedHeader & ValidatorSet) +type LightBlock struct {} +``` + ### Inter Process Communication @@ -375,9 +431,24 @@ func FetchLightBlock(peer PeerID, height Height) LightBlock ``` See the [verification specification][verification] for details. + + +```go +func SubmitProofOfFork(peer PeerID, PoF LightNodeProofOfFork) Result +``` +- Implementation remark + * Sends to `peer` a `PoF` that contains a header that is not + on the branch, the full node `peer` is on +- Expected precondition +- Expected postcondition +- Error condition + + ### Auxiliary Functions (Local) + + ```go Replace_Secondary(addr Address) ``` @@ -415,10 +486,25 @@ The problem is solved by calling the function `ForkDetector` with a lightstore that contains a light block that has just been verified by the verifier. +```go +func Supervisor + +VerifyToTarget +result := Forkdetector +if result.Empty { + LightStore.Update(testedLB, StateTrusted) +} +else { + submit all PoFs to primary + + + generate PoFs to be sent to secondaries + +} +``` + ```go -func ForkDetector(ls LightStore) { - Forks.Init // initialize a container in which we collect forks +func ForkDetector(ls LightStore, PoFs PoFStore) { testedLB := LightStore.LatestVerified() for i, s range Secondaries { sh := FetchLightBlock(s,testedLB.Height) @@ -436,12 +522,18 @@ func ForkDetector(ls LightStore) { auxLS.Update(LightStore.LatestTrusted(), StateVerified); auxLS.Update(sh,StateUnverified); result := VerifyToTarget(s, auxLS, sh.Header.Height) - if result = (_,ResultSuccess) || (_,EXPIRED) { + if result = (LS,ResultSuccess) || (LS,EXPIRED) { // we verified header sh which is conflicting to hd // there is a fork on the main blockchain. // If return code was EXPIRED it might be too late // to punish, we still report it. - Forks.Add(sh) + + pof = new LightNodeProofOfFork + pof.ConflictingBlock := get smallest lightblock greater then latestTrusted + pof.TrustedBlock.Height = LightStore.LatestTrusted().Height + pof.TrustedBlock.BlockID = LightStore.LatestTrusted().Commit.LastBlockID + + PoFs.Add(pof) } else { // s might be faulty or unreachable Replace_Secondary(s) @@ -451,16 +543,20 @@ func ForkDetector(ls LightStore) { } } } - if Forks.isEmpty { - LightStore.Update(testedLB, StateTrusted) + if PoFs.isEmpty { + return PoFs + } + else { + return PoFs } - return (LightStore,Forks,OK) + } ``` - Expected precondition - Secondaries initialized and non-empty + - `PoFs` initialized and empty - Expected postcondition - satisfies [LCD-DIST-INV], [LCD-DIST-LIFE-FORK] - removes faulty secondary if it reports wrong header diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index f66e48978..66a0ddc6a 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -13,6 +13,12 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics > I assume you know what that is. +#### An IBC/Tendermint Dictionary + +| IBC Term | Tendermint-RS Spec Term | +|----------|-------------------------| +|Commitment root is app hash | AppState | + #### Handler A blockchain runs a **handler** that passively collects information about @@ -294,3 +300,20 @@ We will need to define what we expect from these components the interface, and what the handler does - we write specs for these components. + + +# ICS-007 + +> Below we will discuss in more detail the necessary steps to address +[Issue 461](https://github.com/informalsystems/tendermint-rs/issues/461) +in particular w.r.t. 1. "proof of fork" for on-chain clients - may +require breaking changes to +[ICS07](https://github.com/cosmos/ics/tree/master/spec/ics-007-tendermint-client). + +- "Tendermint client state tracks the current validator set": is this + the validator set or the nextvalidator set of the block with tha + maximum height verified thus far? What is `validatorSet` used for? + + + + diff --git a/docs/spec/lightclient/verification/verification.md b/docs/spec/lightclient/verification/verification.md index 4c1454cda..8a45ba752 100644 --- a/docs/spec/lightclient/verification/verification.md +++ b/docs/spec/lightclient/verification/verification.md @@ -477,6 +477,7 @@ independently: The core data structure of the protocol is the LightBlock. +#### **[LCV-DATA-LIGHTBLOCK.1]**: ```go type LightBlock struct { Header Header @@ -615,7 +616,7 @@ func Commit(height int64) (SignedHeader, error) } } ``` -- Expected precodnition +- Expected precondition - header of `height` exists on blockchain - Expected postcondition - if *n* is correct: Returns the signed header of height `height` @@ -644,7 +645,7 @@ func Validators(height int64) (ValidatorSet, error) } } ``` -- Expected precodnition +- Expected precondition - header of `height` exists on blockchain - Expected postcondition - if *n* is correct: Returns the validator set of height `height` From e7b01ef017bae240352cee04ed6ec891864d107f Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 22 Jul 2020 15:30:47 +0200 Subject: [PATCH 02/26] sketch of functions --- docs/spec/lightclient/detection/detection.md | 31 ++++++++++++-------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index a54fb5549..afaef8284 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -412,7 +412,8 @@ generated during detection ```go type PoFStore struct { - ... + PrimaryTrace LightStore + SecondaryTraces List of LightStore } ``` @@ -486,25 +487,32 @@ The problem is solved by calling the function `ForkDetector` with a lightstore that contains a light block that has just been verified by the verifier. + +**TODO::** polish functions below ```go func Supervisor - +{ +loop { VerifyToTarget result := Forkdetector if result.Empty { LightStore.Update(testedLB, StateTrusted) } else { - submit all PoFs to primary - - + generate PoFs to be sent to secondaries - + For all ls in PoFs.SecondaryTraces { + send ls to PoFs.PrimaryTrace[1].Provider + send PrimaryTrace to ls.Provider + **panic** + } +} +} } ``` ```go -func ForkDetector(ls LightStore, PoFs PoFStore) { +func ForkDetector(ls LightStore, PoFs PoFStore) +{ testedLB := LightStore.LatestVerified() for i, s range Secondaries { sh := FetchLightBlock(s,testedLB.Height) @@ -528,12 +536,9 @@ func ForkDetector(ls LightStore, PoFs PoFStore) { // If return code was EXPIRED it might be too late // to punish, we still report it. - pof = new LightNodeProofOfFork - pof.ConflictingBlock := get smallest lightblock greater then latestTrusted - pof.TrustedBlock.Height = LightStore.LatestTrusted().Height - pof.TrustedBlock.BlockID = LightStore.LatestTrusted().Commit.LastBlockID - - PoFs.Add(pof) + pof.ConflictingTrace := LS + PoFs.SecondariyTraces.Add(pof) + PoFs.PrimaryTrace = ls // ls can be truncated from ls.LatestTrusted() } else { // s might be faulty or unreachable Replace_Secondary(s) From 7d08cd9e9934efad896d48f67f8978e1c86aa737 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 23 Jul 2020 10:54:20 +0200 Subject: [PATCH 03/26] supervisor --- docs/spec/lightclient/detection/detection.md | 132 +++++++++++++------ 1 file changed, 90 insertions(+), 42 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index afaef8284..15c7cf154 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -392,37 +392,42 @@ and the following transition invariant ### Data Structures +Lightblocks and LightStores are +defined at [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See the [verification specification][verification] for details. + + +#### **[LCV-DATA-POF.1]**: ```go type LightNodeProofOfFork struct { - TrustedBlock TrustedBlockInfo - ConflictingTrace LightStore + TrustedBlock LightBlock + TraceA LightStore + TraceB LightStore } - -// info about the LC's last trusted block -type TrustedBlockInfo struct { - Height int - BlockID BlockID -} ``` + + + + + + + + #### **[LCV-DATA-POFSTORE.1]**: -Proofs of Forks are stored in a structure which stores all proofs -generated during detection +Proofs of Forks are stored in a structure which stores all proofs +generated during detection. ```go type PoFStore struct { - PrimaryTrace LightStore - SecondaryTraces List of LightStore + ... } ``` -The following is defined at **[LCV-DATA-LIGHTBLOCK.1]**: -```go -// full light block (SignedHeader & ValidatorSet) -type LightBlock struct {} -``` + + + ### Inter Process Communication @@ -433,7 +438,7 @@ func FetchLightBlock(peer PeerID, height Height) LightBlock See the [verification specification][verification] for details. - +####**[LCD-FUNC-SUBMIT.1]:** ```go func SubmitProofOfFork(peer PeerID, PoF LightNodeProofOfFork) Result ``` @@ -447,9 +452,20 @@ func SubmitProofOfFork(peer PeerID, PoF LightNodeProofOfFork) Result ### Auxiliary Functions (Local) +####**[LCD-FUNC-REPLACE-P.1]:** +```go +Replace_Primary() +``` +- Expected precondition + - *FullNodes* is nonempty +- Expected postcondition + - *primary* is moved to *FaultyNodes* + - an address *a* from *FullNodes* is assigned to *primary* +- Error condition + - if precondition is violated - +####**[LCD-FUNC-REPLACE-S.1]:** ```go Replace_Secondary(addr Address) ``` @@ -481,35 +497,67 @@ Shared data of the light client - LightStore +### Outline - -The problem is solved by calling the function `ForkDetector` with -a lightstore that contains a light block that has -just been verified by the verifier. +The problem laid out is solved by calling the function `ForkDetector` + with a lightstore that contains a light block that has just been + verified by the verifier. We start be describing the context on + which the fork detector is called by giving a sequential version + of the supervisor function: **TODO::** polish functions below + + + +####**[LCD-FUNC-SUPERVISOR.1]:** + ```go -func Supervisor -{ -loop { -VerifyToTarget -result := Forkdetector -if result.Empty { - LightStore.Update(testedLB, StateTrusted) -} -else { - For all ls in PoFs.SecondaryTraces { - send ls to PoFs.PrimaryTrace[1].Provider - send PrimaryTrace to ls.Provider - **panic** - } -} -} +func Sequential-Supervisor { + loop { + nextheight := input(); + result := NoResult; + while result != ResultSuccess { + lightStore,result := VerifyToTarget(primary, lightStore, nextheight); + if result == ResultFailure { + Replace_Primary(); + } + } + + PoFs := Forkdetector(lightStore, PoFs); + if PoFs.Empty { + LightStore.Update(testedLB, StateTrusted); + } + else { + For all ls in PoFs.SecondaryTraces { + send ls to PoFs.PrimaryTrace[1].Provider; + send PrimaryTrace to ls.Provider; + **panic**; + } + } + } } ``` +- Implementation remark + - sequential logic that fills the lightstore of the + supervisor. After verification (`VerifyToTarget`) it + cross-checks with secondaries (`Forkdetector`) +- Expected precondition + - *lightStore* initialized with trusted header + - *PoFs* empty +- Expected postcondition + - runs forever, or + - is terminated by user and satisfies LightStore invariant, or **TODO** + - has submitted proof of fork upon detecting a fork +- Error condition + - none +---- +**TODO** Discuss how lightstore can be used with different semantics +### Fork Detector + +####**[LCD-FUNC-DETECTOR.1]:** ```go func ForkDetector(ls LightStore, PoFs PoFStore) { @@ -529,8 +577,8 @@ func ForkDetector(ls LightStore, PoFs PoFStore) auxLS.Init auxLS.Update(LightStore.LatestTrusted(), StateVerified); auxLS.Update(sh,StateUnverified); - result := VerifyToTarget(s, auxLS, sh.Header.Height) - if result = (LS,ResultSuccess) || (LS,EXPIRED) { + LS,result := VerifyToTarget(s, auxLS, sh.Header.Height) + if result = ResultSuccess) || result = EXPIRED { // we verified header sh which is conflicting to hd // there is a fork on the main blockchain. // If return code was EXPIRED it might be too late @@ -569,7 +617,7 @@ func ForkDetector(ls LightStore, PoFs PoFStore) - fails if precondition is violated - fails if [LCV-INV-TP] is violated (no trusted header within trusting period - +---- From 7d9f6616f2dcdd7a24f484abdcd04278004b07e6 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 23 Jul 2020 13:39:18 +0200 Subject: [PATCH 04/26] first draft of functions --- docs/spec/lightclient/detection/detection.md | 68 +++++++++++--------- 1 file changed, 37 insertions(+), 31 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 15c7cf154..e8d52d50b 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -399,9 +399,9 @@ defined at [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See the [verific #### **[LCV-DATA-POF.1]**: ```go type LightNodeProofOfFork struct { - TrustedBlock LightBlock - TraceA LightStore - TraceB LightStore + TrustedBlock LightBlock + PrimaryTrace LightStore + SecondaryTrace LightStore } ``` @@ -425,9 +425,15 @@ type PoFStore struct { ``` +In additions to the functions defined in **TODO**, the LightStore exposes the following function - - +```go +func (ls LightStore) Subtrace(from int, to int) LightStore +``` +- Expected postcondition + - returns a lightstore that contains all lightblocks *b* from *ls* + that satisfy: *from < b.Header.Height <= to* +---- ### Inter Process Communication @@ -438,13 +444,12 @@ func FetchLightBlock(peer PeerID, height Height) LightBlock See the [verification specification][verification] for details. -####**[LCD-FUNC-SUBMIT.1]:** +#### **[LCD-FUNC-SUBMIT.1]:** ```go -func SubmitProofOfFork(peer PeerID, PoF LightNodeProofOfFork) Result +func SubmitProofOfFork(LightNodeProofOfFork) Result ``` - Implementation remark - * Sends to `peer` a `PoF` that contains a header that is not - on the branch, the full node `peer` is on + * submit PoF to primary and secondaries. **TODO** minimize data? - Expected precondition - Expected postcondition - Error condition @@ -510,10 +515,10 @@ The problem laid out is solved by calling the function `ForkDetector` -####**[LCD-FUNC-SUPERVISOR.1]:** +#### **[LCD-FUNC-SUPERVISOR.1]:** ```go -func Sequential-Supervisor { +func Sequential-Supervisor () (error) { loop { nextheight := input(); result := NoResult; @@ -526,14 +531,16 @@ func Sequential-Supervisor { PoFs := Forkdetector(lightStore, PoFs); if PoFs.Empty { + // no fork detected with secondaries, we trust the new + // lightblock LightStore.Update(testedLB, StateTrusted); } else { - For all ls in PoFs.SecondaryTraces { - send ls to PoFs.PrimaryTrace[1].Provider; - send PrimaryTrace to ls.Provider; - **panic**; + // there is a fork, we submit the proofs and exit + for i, p range PoFs { + SubmitProofOfFork(p); } + return(ErrorFork); } } } @@ -557,7 +564,7 @@ func Sequential-Supervisor { ### Fork Detector -####**[LCD-FUNC-DETECTOR.1]:** +#### **[LCD-FUNC-DETECTOR.1]:** ```go func ForkDetector(ls LightStore, PoFs PoFStore) { @@ -578,16 +585,22 @@ func ForkDetector(ls LightStore, PoFs PoFStore) auxLS.Update(LightStore.LatestTrusted(), StateVerified); auxLS.Update(sh,StateUnverified); LS,result := VerifyToTarget(s, auxLS, sh.Header.Height) - if result = ResultSuccess) || result = EXPIRED { + if (result = ResultSuccess || result = EXPIRED) { // we verified header sh which is conflicting to hd // there is a fork on the main blockchain. // If return code was EXPIRED it might be too late // to punish, we still report it. - - pof.ConflictingTrace := LS - PoFs.SecondariyTraces.Add(pof) - PoFs.PrimaryTrace = ls // ls can be truncated from ls.LatestTrusted() - } else { + new pof; + pof.TrustedBlock := LightStore.LatestTrusted() + pof.PrimaryTrace := + LightStore.Subtrace(LightStore.LatestTrusted().Height, + testedLB.Height); + pof.SecondaryTrace := + auxLS.Subtrace(LightStore.LatestTrusted().Height, + testedLB.Height); + PoFs.Add(pof); + } + else { // s might be faulty or unreachable Replace_Secondary(s) // If a new node is added to secondaries, this @@ -596,23 +609,16 @@ func ForkDetector(ls LightStore, PoFs PoFStore) } } } - if PoFs.isEmpty { - return PoFs - } - else { - return PoFs - } - + return PoFs } - ``` - - Expected precondition - Secondaries initialized and non-empty - `PoFs` initialized and empty - Expected postcondition - satisfies [LCD-DIST-INV], [LCD-DIST-LIFE-FORK] - removes faulty secondary if it reports wrong header + - **TODO** proof of fork - Error condition - fails if precondition is violated - fails if [LCV-INV-TP] is violated (no trusted header within From 0b78a78c01f9c5c4b00608ec31a9b84a46eeb9cb Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 23 Jul 2020 16:34:56 +0200 Subject: [PATCH 05/26] more fine grained detection --- docs/spec/lightclient/detection/detection.md | 53 ++++++++++++-------- 1 file changed, 32 insertions(+), 21 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index e8d52d50b..a26d1d020 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -446,18 +446,22 @@ See the [verification specification][verification] for details. #### **[LCD-FUNC-SUBMIT.1]:** ```go -func SubmitProofOfFork(LightNodeProofOfFork) Result +func SubmitProofOfFork(pof LightNodeProofOfFork) Result ``` - Implementation remark - * submit PoF to primary and secondaries. **TODO** minimize data? + - **QUESTION** minimize data? We could submit to the primary only + the trace of the secondary, and vice versa + - **QUESTION** Should we broadcast the complete evidence to everyone? - Expected precondition + - none - Expected postcondition + - submit evidence to primary and the secondary in *pof* - Error condition - + - none ### Auxiliary Functions (Local) -####**[LCD-FUNC-REPLACE-P.1]:** +#### **[LCD-FUNC-REPLACE-PRIMARY.1]:** ```go Replace_Primary() ``` @@ -466,11 +470,13 @@ Replace_Primary() - Expected postcondition - *primary* is moved to *FaultyNodes* - an address *a* from *FullNodes* is assigned to *primary* + - **QUESTION** OK: All lightblocks of heights greater than + *lightStore.LatestTrusted().Height* are removed from *lightStore* - Error condition - if precondition is violated -####**[LCD-FUNC-REPLACE-S.1]:** +#### **[LCD-FUNC-REPLACE-SECONDARY.1]:** ```go Replace_Secondary(addr Address) ``` @@ -495,11 +501,11 @@ See the [verification specification][verification] for details. ## Solution -Shared data of the light client +### Shared data of the light client - a pool of full nodes *FullNodes* that have not been contacted before - peer set called *Secondaries* - primary -- LightStore +- lightStore ### Outline @@ -511,24 +517,25 @@ The problem laid out is solved by calling the function `ForkDetector` of the supervisor function: -**TODO::** polish functions below - - #### **[LCD-FUNC-SUPERVISOR.1]:** ```go -func Sequential-Supervisor () (error) { +func Sequential-Supervisor () (Error) { loop { nextheight := input(); result := NoResult; while result != ResultSuccess { lightStore,result := VerifyToTarget(primary, lightStore, nextheight); if result == ResultFailure { + // pick new primary and delete all lightblocks above + // LastTrusted (they have not been cross-checked + // **QUESTION**: agreeotherwise we might get blocked Replace_Primary(); } } - + // at this point we have added a verified header of height nextheight + // now we cross-check PoFs := Forkdetector(lightStore, PoFs); if PoFs.Empty { // no fork detected with secondaries, we trust the new @@ -546,9 +553,6 @@ func Sequential-Supervisor () (error) { } ``` - Implementation remark - - sequential logic that fills the lightstore of the - supervisor. After verification (`VerifyToTarget`) it - cross-checks with secondaries (`Forkdetector`) - Expected precondition - *lightStore* initialized with trusted header - *PoFs* empty @@ -569,7 +573,7 @@ func Sequential-Supervisor () (error) { func ForkDetector(ls LightStore, PoFs PoFStore) { testedLB := LightStore.LatestVerified() - for i, s range Secondaries { + for i, secondary range Secondaries { sh := FetchLightBlock(s,testedLB.Height) // as the check below only needs the header, it is sufficient // to download the header rather than the LighBlock @@ -584,7 +588,7 @@ func ForkDetector(ls LightStore, PoFs PoFStore) auxLS.Init auxLS.Update(LightStore.LatestTrusted(), StateVerified); auxLS.Update(sh,StateUnverified); - LS,result := VerifyToTarget(s, auxLS, sh.Header.Height) + LS,result := VerifyToTarget(secondary, auxLS, sh.Header.Height) if (result = ResultSuccess || result = EXPIRED) { // we verified header sh which is conflicting to hd // there is a fork on the main blockchain. @@ -601,11 +605,16 @@ func ForkDetector(ls LightStore, PoFs PoFStore) PoFs.Add(pof); } else { - // s might be faulty or unreachable - Replace_Secondary(s) + // secondary might be faulty or unreachable + // it might fail to provide a trace that supports sh + // or time out + newSecondary := Replace_Secondary(secondary) // If a new node is added to secondaries, this - // should not imply an additional loop iteration. - // We assume one of the secondaries is correct. + // should imply an additional loop iteration. + // **QUESTION** additional iteration added. OK? + // **QUESTION** should check from oldest trusted lightblock + // I want the invariant that a trusted + // block has been checked with all secondaries } } } @@ -626,6 +635,8 @@ func ForkDetector(ls LightStore, PoFs PoFStore) ---- +#### **[LCD-INV-SECONDARIES.1]:** + ## Correctness arguments From b3039368d65b423148c2c2540bb38ab64181930d Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 23 Jul 2020 17:37:37 +0200 Subject: [PATCH 06/26] primary --- docs/spec/lightclient/detection/detection.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index a26d1d020..f19affdcd 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -400,8 +400,8 @@ defined at [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See the [verific ```go type LightNodeProofOfFork struct { TrustedBlock LightBlock - PrimaryTrace LightStore - SecondaryTrace LightStore + PrimaryTrace LightStore // list of lightblocks is sufficient + SecondaryTrace LightStore // list of lightblocks is sufficient } ``` @@ -425,8 +425,9 @@ type PoFStore struct { ``` -In additions to the functions defined in **TODO**, the LightStore exposes the following function +In additions to the functions defined in the [verification specification][verification], the LightStore exposes the following function +#### **[LCD-FUNC-SUBTRACE.1]:** ```go func (ls LightStore) Subtrace(from int, to int) LightStore ``` @@ -529,9 +530,13 @@ func Sequential-Supervisor () (Error) { lightStore,result := VerifyToTarget(primary, lightStore, nextheight); if result == ResultFailure { // pick new primary and delete all lightblocks above - // LastTrusted (they have not been cross-checked - // **QUESTION**: agreeotherwise we might get blocked + // LastTrusted (they have not been cross-checked) + // **QUESTION**: agreed? otherwise we might get blocked + // **QUESTION**: alternatively (preferred) we cross-check we new + // primary and might need to report a fork + Replace_Primary(); + } } // at this point we have added a verified header of height nextheight @@ -608,7 +613,7 @@ func ForkDetector(ls LightStore, PoFs PoFStore) // secondary might be faulty or unreachable // it might fail to provide a trace that supports sh // or time out - newSecondary := Replace_Secondary(secondary) + newSecondary := Replace_Secondary(secondary,LightStore) // If a new node is added to secondaries, this // should imply an additional loop iteration. // **QUESTION** additional iteration added. OK? From 26c4369e85368120730b455c07b0c9f26d99ccd0 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Fri, 24 Jul 2020 15:49:36 +0200 Subject: [PATCH 07/26] first updates after discussion with Zarko --- docs/spec/lightclient/detection/detection.md | 131 ++++++++++++++++--- 1 file changed, 112 insertions(+), 19 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index f19affdcd..82dbe890b 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -161,10 +161,16 @@ Let *a*, *b*, *c*, be light blocks and *t* a time, we define implies *b = c*. +---- + +#### **[TMBC-SIGN-FORK]** + If there exists three light blocks a, b, and c, with *sign-skip-match(a,b,c,t) = false* then we have a *slashable fork*. +We call *a* the bifurcation block of the fork. +---- > **TODO:** I think the following definition is @@ -379,7 +385,7 @@ prefer the above as it is slightly less operational. -#### **[LCD-INV-NODES]:** +#### **[LCD-INV-NODES.1]:** The detector shall maintain the following invariants: - *FullNodes \intersect Secondaries = {}* - *FullNodes \intersect FaultyNodes = {}* @@ -388,6 +394,11 @@ The detector shall maintain the following invariants: and the following transition invariant - *FullNodes' \union Secondaries' \union FaultyNodes' = FullNodes \union Secondaries \union FaultyNodes* + +#### **[LCD-INV-TRUSTED-AGREED.1]:** + +**TODO** The primary and the secondary agree on LatestTrusted. + ## Solution ### Data Structures @@ -395,16 +406,46 @@ and the following transition invariant Lightblocks and LightStores are defined at [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See the [verification specification][verification] for details. +The following data structure defines a **proof of fork**. Following +[TMBC-SIGN-FORK], we require two blocks *b* and *c* for the same +height that can both be verified from a common root block *a* (using +the skipping or the sequential method). + +**TODO:** move this discussion up to beginning of spec! + +> Observe that just two blocks for the same height are not +> sufficient. One of the blocks may be bogus [TMBC-BOGUS] which does +> not constitute slashable behavior. + +> Which leads to the question whether the light node should try to do +fork detection on its initial block (from subjective +initialization). This could be done by doing backwards verification +(with the hashes) until a bifurcation block is found. +While there are scenarios where a +fork could be found, there is also the scenario where a faulty full +node feeds the light node with bogus light blocks and forces the light +node to check hashes until a bogus chain is out of the trusting period. +As a result, the light client +should not try to establish a fork for its initial header. #### **[LCV-DATA-POF.1]**: ```go type LightNodeProofOfFork struct { TrustedBlock LightBlock - PrimaryTrace LightStore // list of lightblocks is sufficient - SecondaryTrace LightStore // list of lightblocks is sufficient + PrimaryTrace []LightBlock + SecondaryTrace []LightBlock } ``` +> [LCV-DATA-POF.1] mirrors the definition [TMBC-SIGN-FORK]: +> *TrustedBlock* corresponds to *a*, and *PrimaryTrace* and *SecondaryTrace* +> are traces to two blocks *b* and *c*. The traces establish that both +> *skip-root(a,b,t)* and *skip-root(a,c,t)* are satisfied. + + + + + @@ -425,7 +466,9 @@ type PoFStore struct { ``` -In additions to the functions defined in the [verification specification][verification], the LightStore exposes the following function +In additions to the functions defined in +the [verification specification][verification], the +LightStore exposes the following function #### **[LCD-FUNC-SUBTRACE.1]:** ```go @@ -436,6 +479,9 @@ func (ls LightStore) Subtrace(from int, to int) LightStore that satisfy: *from < b.Header.Height <= to* ---- + + + ### Inter Process Communication @@ -450,29 +496,71 @@ See the [verification specification][verification] for details. func SubmitProofOfFork(pof LightNodeProofOfFork) Result ``` - Implementation remark - - **QUESTION** minimize data? We could submit to the primary only - the trace of the secondary, and vice versa - - **QUESTION** Should we broadcast the complete evidence to everyone? - Expected precondition - none - Expected postcondition - - submit evidence to primary and the secondary in *pof* + - submit evidence to primary and the secondary in *pof*, that is, + to + - `pof.PrimaryTrace[1].Provider` + - `pof.SecondaryTrace[1].Provider` + - **QUESTION** minimize data? We could submit to the primary only + the trace of the secondary, and vice versa + - Error condition - none ### Auxiliary Functions (Local) +#### **[LCD-FUNC-CROSS-CHECK.1]:** + +```go +func CrossCheck(peer PeerID, testedLB LightBlock) (result) { + sh := FetchLightBlock(peer, testedLB.Height); + // as the check below only needs the header, it is sufficient + // to download the header rather than the LighBlock + if testedLB.Header == sh.Header { + return OK + } + else { + return DoesNotMatch + } +} +``` +- Implementation remark +- Expected precondition +- Expected postcondition +- Error condition + + #### **[LCD-FUNC-REPLACE-PRIMARY.1]:** ```go Replace_Primary() ``` +- Implementation remark + - the primary is replaced by a secondary, and lightblocks above + trusted blocks are removed + - to maintain a constant size of secondaries, at this point we + might need to + - pick a new secondary nsec + - maintain [LCD-INV-TRUSTED-AGREED.1], that is, + - call `CrossCheck(nsec,lightStore.LatestTrusted()`. + If it matches we are OK, otherwise + - we might just repeat with another full node as new secondary + - try to do fork detection from some possibly old + lightblock in store. (Might be the approach for the + light node that assumes to be connected to correct + full nodes only from time to time) + - Expected precondition - *FullNodes* is nonempty + - Expected postcondition - *primary* is moved to *FaultyNodes* - - an address *a* from *FullNodes* is assigned to *primary* - - **QUESTION** OK: All lightblocks of heights greater than - *lightStore.LatestTrusted().Height* are removed from *lightStore* + - all lightblocks with height greater than + lightStore.LatestTrusted().Height are removed from *lightStore*. + - a secondary *s* is moved from *Secondaries* to primary +> this ensures that *s* agrees on the Last Trusted State + - Error condition - if precondition is violated @@ -481,6 +569,16 @@ Replace_Primary() ```go Replace_Secondary(addr Address) ``` +- Implementation remark + - maintain [LCD-INV-TRUSTED-AGREED.1], that is, + - call `CrossCheck(nsec,lightStore.LatestTrusted()`. + If it matches we are OK, otherwise + - we might just repeat with another full node as new secondary + - try to do fork detection from some possibly old + lightblock in store. (Might be the approach for the + light node that assumes to be connected to correct + full nodes only from time to time) + - Expected precondition - *FullNodes* is nonempty - Expected postcondition @@ -573,16 +671,14 @@ func Sequential-Supervisor () (Error) { ### Fork Detector + #### **[LCD-FUNC-DETECTOR.1]:** ```go func ForkDetector(ls LightStore, PoFs PoFStore) { testedLB := LightStore.LatestVerified() for i, secondary range Secondaries { - sh := FetchLightBlock(s,testedLB.Height) - // as the check below only needs the header, it is sufficient - // to download the header rather than the LighBlock - if testedLB.Header == sh.Header { + if OK = CrossCheck(secondary, testedLB) { // header matches. we do nothing. } else { // [LCD-REQ-REP] @@ -599,7 +695,7 @@ func ForkDetector(ls LightStore, PoFs PoFStore) // there is a fork on the main blockchain. // If return code was EXPIRED it might be too late // to punish, we still report it. - new pof; + pof = new LightNodeProofOfFork; pof.TrustedBlock := LightStore.LatestTrusted() pof.PrimaryTrace := LightStore.Subtrace(LightStore.LatestTrusted().Height, @@ -640,9 +736,6 @@ func ForkDetector(ls LightStore, PoFs PoFStore) ---- -#### **[LCD-INV-SECONDARIES.1]:** - - ## Correctness arguments From f860837848db3469328bf4041031d76b1e241de3 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Fri, 24 Jul 2020 16:24:19 +0200 Subject: [PATCH 08/26] all discussion points with Zarko at least sketched --- docs/spec/lightclient/detection/detection.md | 36 +++++++++----------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 82dbe890b..3b9d829e9 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -501,11 +501,18 @@ func SubmitProofOfFork(pof LightNodeProofOfFork) Result - Expected postcondition - submit evidence to primary and the secondary in *pof*, that is, to - - `pof.PrimaryTrace[1].Provider` - - `pof.SecondaryTrace[1].Provider` + - `pof.PrimaryTrace[1].Provider` + - `pof.SecondaryTrace[1].Provider` - **QUESTION** minimize data? We could submit to the primary only - the trace of the secondary, and vice versa - + the trace of the secondary, and vice versa. Do we need to spell + that out here? (Also, by [LCD-INV-TRUSTED-AGREED.1], we do not + need to send `pof.TrustedBlock`) + - **FUTURE WORK:** we might send *pof* to primary or all + secondaries or broadcast to all full nodes. However, in evidence + detection this might need that a full node has to check a *pof* + where both traces are not theirs. This leads to more complicated + logic at the full node, which we do not need right now. + - Error condition - none @@ -564,6 +571,7 @@ Replace_Primary() - Error condition - if precondition is violated +**TODO:** pass in the lightstore to the replace functions #### **[LCD-FUNC-REPLACE-SECONDARY.1]:** ```go @@ -626,15 +634,10 @@ func Sequential-Supervisor () (Error) { result := NoResult; while result != ResultSuccess { lightStore,result := VerifyToTarget(primary, lightStore, nextheight); - if result == ResultFailure { - // pick new primary and delete all lightblocks above + if result == ResultFailure { + // pick new primary and delete all lightblocks above // LastTrusted (they have not been cross-checked) - // **QUESTION**: agreed? otherwise we might get blocked - // **QUESTION**: alternatively (preferred) we cross-check we new - // primary and might need to report a fork - Replace_Primary(); - } } // at this point we have added a verified header of height nextheight @@ -680,7 +683,8 @@ func ForkDetector(ls LightStore, PoFs PoFStore) for i, secondary range Secondaries { if OK = CrossCheck(secondary, testedLB) { // header matches. we do nothing. - } else { + } + else { // [LCD-REQ-REP] // header does not match. there is a situation. // we try to verify sh by querying s @@ -709,13 +713,7 @@ func ForkDetector(ls LightStore, PoFs PoFStore) // secondary might be faulty or unreachable // it might fail to provide a trace that supports sh // or time out - newSecondary := Replace_Secondary(secondary,LightStore) - // If a new node is added to secondaries, this - // should imply an additional loop iteration. - // **QUESTION** additional iteration added. OK? - // **QUESTION** should check from oldest trusted lightblock - // I want the invariant that a trusted - // block has been checked with all secondaries + Replace_Secondary(secondary) } } } From a5d8651ca15a066bb7b78c0a445f809165bfcef6 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Mon, 27 Jul 2020 09:53:46 +0200 Subject: [PATCH 09/26] prologue --- docs/spec/lightclient/detection/detection.md | 290 +++++++++++++------ 1 file changed, 196 insertions(+), 94 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 3b9d829e9..1dcc6b257 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -1,44 +1,182 @@ ***This an unfinished draft. Comments are welcome!*** -## Decisions with Zarko +This document contains: + +- the outcome of recent discussion +- a sketch of the light client supervisor to provide the context in + which fork detection happens +- a discussion about lightstore semantics +- a draft of the light node fork detection including "proof of fork" + definition, that is, the data structure to submit evidence to full + nodes. + + +## Results of Discussions and Decisions - Generating a minimal proof of fork is too costly at the light client - we do not know all lightblocks from the primary - therefore there are many scenarios. we might even need to ask the primary again for additional lightblocks to isolate the - branch. As the main goal is to catch misbehavior of the primary, + branch. +> For instance, the light node starts with block at height 1 and the +> primary provides a block of height 10 that the light node can +> verify immediately. In cross-checking, a secondary now provides a +> conflicting header b10 of height 10 that needs another header b5 +> of height 5 to +> verify. Now, in order for the light node to convince the primary: +> - The light node cannot just sent b5, as it is not clear whether +> the fork happened before or after 5 +> - The light node cannot just send b10, as the primary would also +> need b5 for verification +> - In order to minimize the evidence, the light node may try to +> figure out where the branch happens, e.g., by asking the primary +> for height 5 (it might be that more queries are required, also +> to the secondary. However, assuming that in this scenario the +> primary is faulty it may not respond. + + As the main goal is to catch misbehavior of the primary, evidence generation and punishment must not depend on their - cooperation. + cooperation. So the moment we have proof of fork (even if it + contains several light blocks) we should submit right away. -- proof of fork is a trace of lightblocks that verifies a block - different from the one the full node knows +- decision: "full" proof of fork consists of two traces that origin in the + same lightblock and lead to conflicting headers of the same height. + +- For submission of proof of fork, we may do some optimizations, for + instance, we might just submit a trace of lightblocks that verifies a block + different from the one the full node knows (we do not send the trace + the primary gave us back to the primary) -- For each secondary, we check the primary against one secondary -- We do not check secondary against secondary -- the reason is that the attack is via the primary. We only try to +- The light client attack is via the primary. Thus we try to catch if the primary installs a bad light block + - We do not check secondary against secondary + - For each secondary, we check the primary against one secondary -## TODOs -- the main logic, i.e., describing what happens when the function of - the current spec returns. If a fork is detected, we need to report - evidence (and shut down light client?). + pre and post conditions on - lightstore when `VerifyToTarget` or detector are called. - -- We should clarify what is the expectation of VerifyToTarget so if it - returns TimeoutError it can be assumed faulty. I guess that - VerifyToTarget with correct full node should never terminate with - TimeoutError. +# Light Client Sequential Supervisor + +**TODO:** decide where (into which specification) to put the +following: + + +We describe the context on which the fork detector is called by giving +a sequential version of the supervisor function. +Roughly, it alternates two phases namely: + - Light Client Verification. As a result, a header of the required + height has been downloaded from and verified with the primary + - Light Client Fork Detections. As a result the header has been + cross-checked with the secondaries. In case the is a fork we + submit "proof of fork" and exit. + + -- clarify EXPIRED case. Can we always punish? Can we give sufficient - conditions. - -- Discussion with end-user API in the case of - - user uses trusted blocks only - - user uses verified blocks (may need to roll back) -- + + +#### **[LC-FUNC-SUPERVISOR.1]:** + +```go +func Sequential-Supervisor () (Error) { + loop { + // get the next height + nextheight := input(); + + // Verify + result := NoResult; + while result != ResultSuccess { + lightStore,result := VerifyToTarget(primary, lightStore, nextheight); + if result == ResultFailure { + // pick new primary (promote a secondary to primary) + /// and delete all lightblocks above + // LastTrusted (they have not been cross-checked) + Replace_Primary(); + } + } + + // Cross-check + PoFs := Forkdetector(lightStore, PoFs); + if PoFs.Empty { + // no fork detected with secondaries, we trust the new + // lightblock + LightStore.Update(testedLB, StateTrusted); + } + else { + // there is a fork, we submit the proofs and exit + for i, p range PoFs { + SubmitProofOfFork(p); + } + return(ErrorFork); + } + } +} +``` +**TODO:** finish conditions +- Implementation remark +- Expected precondition + - *lightStore* initialized with trusted header + - *PoFs* empty +- Expected postcondition + - runs forever, or + - is terminated by user and satisfies LightStore invariant, or **TODO** + - has submitted proof of fork upon detecting a fork +- Error condition + - none +---- + +# Semantics of the LightStore + +Currently, a lightblock in the lightstore can be in one of the +following states: +- StateUnverified +- StateVerified +- StateFailed +- StateTrusted + +The intuition is that `StateVerified` captures that the lightblock has +been verified with the primary, and `StateTrusted` is the state after +successful cross-checking with the secondaries. + +Assuming there is **always one correct node among primary and +secondaries**, and there is no fork on the blockchain, lightblocks that +are in `StateTrusted` can be used by the user with the guarantee of +"finality". If a block in `StateVerified` is used, it might be that +detection later finds a fork, and a roll-back might be needed. + +**Remark:** The assumption of one correct node, does not render +verification useless. It is true that if the primary and the +secondaries return the same block we may trust it. However, if there +is a node that provides a different block, the light node still needs +verification to understand whether there is a fork, or whether the +different block is just bogus (without any support of some previous +validator set). + +**Remark:** A light node may choose the full nodes it communicates +with (the light node and the full node might even belong to the same +stakeholder) so the assumption might be justified in some cases. + +In the future, we will do the following changes + - we assume that only from time to time, the light node is + connected to a correct full node + - this means for some limited time, the light node might have no + means to defend against light client attacks + - as a result we do not have finality + - once the light node reconnects with a correct full node, it + should detect the light client attack and submit evidence. + +Under these assumptions, `StateTrusted` loses its meaning. As a +result, it should be removed from the API. We suggest that we replace +it with a flag "trusted" that can be used +- internally for efficiency reasons (to maintain + [LCD-INV-TRUSTED-AGREED.1] until a fork is detected) +- by light client based on the "one correct full node" assumption + + +---- + + + +> This is where the actual specification is going to start # Fork detector @@ -102,10 +240,10 @@ secondaries using this specification. ### Tendermint Consensus and Forks -#### **[TMBC-GENESIS]** +#### **[TMBC-GENESIS.1]** Let *Genesis* be the agreed-upon initial block (file). -#### **[TMBC-FUNC]** +#### **[TMBC-FUNC.1]** > **TODO** be more precise. +2/3 of b.NextV = c.Val signed c. For now > the following will do: @@ -123,7 +261,7 @@ Let *b* and *c* be two light blocks. We define **supports(b,c,t)** > The following formalizes that *b* was properly generated by > Tendermint; *b* can be traced back to genesis -#### **[TMBC-SEQ-ROOTED]** +#### **[TMBC-SEQ-ROOTED.1]** Let *b* be a light block. We define *sequ-rooted(b)* iff for all i, 1 <= i < h = b.Header.Height, there exist light blocks a(i) s.t. @@ -135,7 +273,7 @@ there exist light blocks a(i) s.t. > skipping verification. Observe that we do not require here (yet) > that *b* was properly generated. -#### **[TMBC-SKIP-ROOT]** +#### **[TMBC-SKIP-ROOT.1]** Let *b* and *c* be light blocks. We define *skip-root(b,c,t)* if at time t there exists an *h* and a sequence *a(1)*, ... *a(h)* s.t. - *a(1) = b* and @@ -150,7 +288,7 @@ time t there exists an *h* and a sequence *a(1)*, ... *a(h)* s.t. > Observe that sign-skip-match is even defined if there is a fork on > the chain. -#### **[TMBC-SIGN-SKIP-MATCH]** +#### **[TMBC-SIGN-SKIP-MATCH.1]** Let *a*, *b*, *c*, be light blocks and *t* a time, we define *sign-skip-match(a,b,c,t) = true* iff - *sequ-rooted(a)* and @@ -163,7 +301,7 @@ implies *b = c*. ---- -#### **[TMBC-SIGN-FORK]** +#### **[TMBC-SIGN-FORK.1]** If there exists three light blocks a, b, and c, with *sign-skip-match(a,b,c,t) = @@ -180,7 +318,7 @@ We call *a* the bifurcation block of the fork. > full nodes as part of normal Tendermint consensus protocol". Please > confirm! -#### **[TMBC-SIGN-UNIQUE]** +#### **[TMBC-SIGN-UNIQUE.1]** Let *b* and *c* be light blocks, we define *sign-unique(b,c) = true* iff - *b.Header.Height = c.Header.Height* and @@ -200,7 +338,7 @@ false* then we have a *fork on the chain*. > fork. -#### **[TMBC-LC-FORK]** +#### **[TMBC-LC-FORK.1]** Let *a*, *b*, *c*, be light blocks and *t* a time. We define *light-client-fork(a,b,c,t)* iff - *sign-skip-match(a,b,c,t) = false* and @@ -215,7 +353,7 @@ Let *a*, *b*, *c*, be light blocks and *t* a time. We define > *a.height < b.height* (which is implied by the definitions which > unfold until *supports()*. -#### **[TMBC-BOGUS]** +#### **[TMBC-BOGUS.1]** Let *b* be a light block and *t* a time. We define *bogus(b,t)* iff - *sequ-rooted(b) = false* and - for all *a*, *sequ-rooted(a)* implies *skip-root(a,b,t) = false* @@ -244,14 +382,14 @@ do not constitute temporal logic verification conditions. For those, see [LCD-DIST-*] below. -#### **[LCD-IP-STATE]** +#### **[LCD-IP-STATE.1]** The detector works on a LightStore that contains LightBlocks in one of the state `StateUnverified`, ` StateVerified`, `StateFailed`, or `StateTrusted`. -#### **[LCD-IP-Q]** +#### **[LCD-IP-Q.1]** Whenever the light client verifier performs `VerifyToTarget` with the primary and returns with @@ -265,7 +403,7 @@ secondaries that satisfy - *h'* is a (light) fork. -#### **[LCD-IP-PEERSET]** +#### **[LCD-IP-PEERSET.1]** Whenever the detector observes *detectable misbehavior* of a full node from the set of Secondaries it should be replaced by a fresh full @@ -300,16 +438,16 @@ detector. ### Assumptions -#### **[LCD-A-CorrFull]** +#### **[LCD-A-CorrFull.1]** At all times there is at least one correct full node among the primary and the secondaries. -**Remark:** Check whether [LCD-A-CorrFull] is not needed in the end because +**Remark:** Check whether [LCD-A-CorrFull.1] is not needed in the end because the verification conditions [LCD-DIST-*] have preconditions on specific cases where primary and/or secondaries are faulty. -#### **[LCD-A-RelComm]** +#### **[LCD-A-RelComm.1]** Communication between the detector and a correct full node is reliable and bounded in time. Reliable communication means that @@ -338,7 +476,7 @@ The detector returns a set *Forks*, and should satisfy the following temporal formulas: -#### **[LCD-DIST-INV]** +#### **[LCD-DIST-INV.1]** If there is no fork at height *h-verified*, then the detector should return the empty set. @@ -348,7 +486,7 @@ return the empty set. **TODO:** add requirements about stateTrusted -#### **[LCD-DIST-LIVE-FORK]** +#### **[LCD-DIST-LIVE-FORK.1]** If there is a fork at height *h*, with *h-trust < h <= h-verified*, and there are two correct full nodes *i* and *j* that are @@ -362,7 +500,7 @@ primary provided branch A, and a correct secondary is on branch B". I prefer the above as it is slightly less operational. -> #### **[LCD-REQ-REP]** +> #### **[LCD-REQ-REP.1]** > If the detector observes two conflicting headers for height *h*, > it should try to verify both. If both are verified it should report evidence. > If the primary reports header *h* and a secondary reports header *h'*, @@ -407,14 +545,14 @@ Lightblocks and LightStores are defined at [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See the [verification specification][verification] for details. The following data structure defines a **proof of fork**. Following -[TMBC-SIGN-FORK], we require two blocks *b* and *c* for the same +[TMBC-SIGN-FORK.1], we require two blocks *b* and *c* for the same height that can both be verified from a common root block *a* (using the skipping or the sequential method). **TODO:** move this discussion up to beginning of spec! > Observe that just two blocks for the same height are not -> sufficient. One of the blocks may be bogus [TMBC-BOGUS] which does +> sufficient. One of the blocks may be bogus [TMBC-BOGUS.1] which does > not constitute slashable behavior. > Which leads to the question whether the light node should try to do @@ -437,7 +575,7 @@ type LightNodeProofOfFork struct { } ``` -> [LCV-DATA-POF.1] mirrors the definition [TMBC-SIGN-FORK]: +> [LCV-DATA-POF.1] mirrors the definition [TMBC-SIGN-FORK.1]: > *TrustedBlock* corresponds to *a*, and *PrimaryTrace* and *SecondaryTrace* > are traces to two blocks *b* and *c*. The traces establish that both > *skip-root(a,b,t)* and *skip-root(a,c,t)* are satisfied. @@ -619,58 +757,22 @@ See the [verification specification][verification] for details. The problem laid out is solved by calling the function `ForkDetector` with a lightstore that contains a light block that has just been - verified by the verifier. We start be describing the context on - which the fork detector is called by giving a sequential version - of the supervisor function: + verified by the verifier. + -#### **[LCD-FUNC-SUPERVISOR.1]:** -```go -func Sequential-Supervisor () (Error) { - loop { - nextheight := input(); - result := NoResult; - while result != ResultSuccess { - lightStore,result := VerifyToTarget(primary, lightStore, nextheight); - if result == ResultFailure { - // pick new primary and delete all lightblocks above - // LastTrusted (they have not been cross-checked) - Replace_Primary(); - } - } - // at this point we have added a verified header of height nextheight - // now we cross-check - PoFs := Forkdetector(lightStore, PoFs); - if PoFs.Empty { - // no fork detected with secondaries, we trust the new - // lightblock - LightStore.Update(testedLB, StateTrusted); - } - else { - // there is a fork, we submit the proofs and exit - for i, p range PoFs { - SubmitProofOfFork(p); - } - return(ErrorFork); - } - } -} -``` -- Implementation remark -- Expected precondition - - *lightStore* initialized with trusted header - - *PoFs* empty -- Expected postcondition - - runs forever, or - - is terminated by user and satisfies LightStore invariant, or **TODO** - - has submitted proof of fork upon detecting a fork -- Error condition - - none ----- +- **TODO:** We should clarify what is the expectation of VerifyToTarget so if it + returns TimeoutError it can be assumed faulty. I guess that + VerifyToTarget with correct full node should never terminate with + TimeoutError. + +- **TODO:** clarify EXPIRED case. Can we always punish? Can we give sufficient + conditions. + + -**TODO** Discuss how lightstore can be used with different semantics ### Fork Detector @@ -724,7 +826,7 @@ func ForkDetector(ls LightStore, PoFs PoFStore) - Secondaries initialized and non-empty - `PoFs` initialized and empty - Expected postcondition - - satisfies [LCD-DIST-INV], [LCD-DIST-LIFE-FORK] + - satisfies [LCD-DIST-INV.1], [LCD-DIST-LIFE-FORK.1] - removes faulty secondary if it reports wrong header - **TODO** proof of fork - Error condition From 14331bdbef68e8cd089b2133822917cd1c93376d Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Mon, 27 Jul 2020 10:42:45 +0200 Subject: [PATCH 10/26] prologue --- docs/spec/lightclient/detection/detection.md | 43 +++++++++++--------- 1 file changed, 23 insertions(+), 20 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 1dcc6b257..87ba2b7fe 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -13,7 +13,7 @@ This document contains: ## Results of Discussions and Decisions -- Generating a minimal proof of fork is too costly at the light client +- Generating a minimal proof of fork (as suggested in [Issue #5083](https://github.com/tendermint/tendermint/issues/5083)) is too costly at the light client - we do not know all lightblocks from the primary - therefore there are many scenarios. we might even need to ask the primary again for additional lightblocks to isolate the @@ -54,6 +54,23 @@ This document contains: - For each secondary, we check the primary against one secondary +- Observe that just two blocks for the same height are not +sufficient proof of fork. +One of the blocks may be bogus [TMBC-BOGUS.1] which does +not constitute slashable behavior. +Which leads to the question whether the light node should try to do +fork detection on its initial block (from subjective +initialization). This could be done by doing backwards verification +(with the hashes) until a bifurcation block is found. +While there are scenarios where a +fork could be found, there is also the scenario where a faulty full +node feeds the light node with bogus light blocks and forces the light +node to check hashes until a bogus chain is out of the trusting period. +As a result, the light client +should not try to detect a fork for its initial header. **The initial +header must be trusted as is.** + + # Light Client Sequential Supervisor **TODO:** decide where (into which specification) to put the @@ -299,16 +316,17 @@ Let *a*, *b*, *c*, be light blocks and *t* a time, we define implies *b = c*. ----- #### **[TMBC-SIGN-FORK.1]** If there exists three light blocks a, b, and c, with *sign-skip-match(a,b,c,t) = -false* then we have a *slashable fork*. +false* then we have a *slashable fork*. +We call *a* a bifurcation block of the fork. -We call *a* the bifurcation block of the fork. ----- +> The lightblock *a* need not be unique, that is, a there may be +> several blocks that satisfy the above requirement for blocks *b* and +> *c*. > **TODO:** I think the following definition is @@ -549,22 +567,7 @@ The following data structure defines a **proof of fork**. Following height that can both be verified from a common root block *a* (using the skipping or the sequential method). -**TODO:** move this discussion up to beginning of spec! - -> Observe that just two blocks for the same height are not -> sufficient. One of the blocks may be bogus [TMBC-BOGUS.1] which does -> not constitute slashable behavior. -> Which leads to the question whether the light node should try to do -fork detection on its initial block (from subjective -initialization). This could be done by doing backwards verification -(with the hashes) until a bifurcation block is found. -While there are scenarios where a -fork could be found, there is also the scenario where a faulty full -node feeds the light node with bogus light blocks and forces the light -node to check hashes until a bogus chain is out of the trusting period. -As a result, the light client -should not try to establish a fork for its initial header. #### **[LCV-DATA-POF.1]**: ```go From df8069a53389fd60b359305e3dc6d71858e407c1 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Mon, 27 Jul 2020 15:17:43 +0200 Subject: [PATCH 11/26] ready for PR --- docs/spec/lightclient/detection/detection.md | 100 ++++++++++++------- 1 file changed, 66 insertions(+), 34 deletions(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 87ba2b7fe..950943786 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -322,7 +322,8 @@ implies *b = c*. If there exists three light blocks a, b, and c, with *sign-skip-match(a,b,c,t) = false* then we have a *slashable fork*. -We call *a* a bifurcation block of the fork. +We call *a* a bifurcation block of the fork. +We say we have **a fork at height** *b.Header.Height*. > The lightblock *a* need not be unique, that is, a there may be > several blocks that satisfy the above requirement for blocks *b* and @@ -489,34 +490,43 @@ The detector gets as input a lightstore *lightStore*. Let *h-verified = lightStore.LatestVerified().Height* and *h-trust=lightStore.LatestTrusted().Height* (see [LCV-DATA-LIGHTSTORE]). -It queries the secondaries for headers at height *h-verified*. -The detector returns a set *Forks*, and should satisfy the following +It queries the secondaries for headers at height *h-verified*. +The detector returns a set *PoF* of *Proof of Forks*, and should satisfy the following temporal formulas: #### **[LCD-DIST-INV.1]** -If there is no fork at height *h-verified*, then the detector should -return the empty set. +If there is no fork at height *h-verified* ([TMBC-SIGN-FORK.1]), +then the detector should return the empty set. - -**TODO:** be precise about what a fork is. - -**TODO:** add requirements about stateTrusted +> If the empty set is returned the supervisor will change the state of +> the header at height *h-verified* to *stateTrusted*. #### **[LCD-DIST-LIVE-FORK.1]** -If there is a fork at height *h*, with *h-trust < h <= h-verified*, and +If there is a fork at height *h-verified*, and there are two correct full nodes *i* and *j* that are - on different branches, and - - primary or secondary, + - *i* is primary and + - *j* is secondary, + +then the detector eventually outputs the fork. + +#### **[LCD-DIST-LIVE-FORK-FAULTY.1]** +If there is a fork at height *h-verified*, and +there is a correct secondary that is on a different branch than the +primary reported, then the detector eventually outputs the fork. -**TODO:** We can weaken the above to "the (not-necessarily correct) -primary provided branch A, and a correct secondary is on branch B". I -prefer the above as it is slightly less operational. +> The above property is quite operational ("Than the primary +> reported"), but it captures quite closely the requirement. As the +> fork detector only makes sense in a distributed setting, and does +> not have a sequential specification, less "pure" +> specification are acceptable. +> These properties capture the following operational requirement: > #### **[LCD-REQ-REP.1]** > If the detector observes two conflicting headers for height *h*, @@ -551,9 +561,23 @@ and the following transition invariant - *FullNodes' \union Secondaries' \union FaultyNodes' = FullNodes \union Secondaries \union FaultyNodes* +> The following invariant is very useful for reasoning, and underlies +> many intuition when we + #### **[LCD-INV-TRUSTED-AGREED.1]:** -**TODO** The primary and the secondary agree on LatestTrusted. +It is always the case the light client has downloaded a lightblock for height +*lightStore.LatestTrusted().Height* +from each of the current primary and the secondary, that all reported +the identical lightblock for that height. + +> In the above, I guess "the identical" might be replaced with "a +> matching" to cover commits that might be different. + +> The above requires us that before we pick a new secondary, we have to +> query the secondary for the header of height +> *lightStore.LatestTrusted().Height*. + ## Solution @@ -562,11 +586,16 @@ and the following transition invariant Lightblocks and LightStores are defined at [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See the [verification specification][verification] for details. -The following data structure defines a **proof of fork**. Following -[TMBC-SIGN-FORK.1], we require two blocks *b* and *c* for the same -height that can both be verified from a common root block *a* (using -the skipping or the sequential method). +> The following data structure [LCV-DATA-POF.1] +> defines a **proof of fork**. Following +> [TMBC-SIGN-FORK.1], we require two blocks *b* and *c* for the same +> height that can both be verified from a common root block *a* (using +> the skipping or the sequential method). +> [LCV-DATA-POF.1] mirrors the definition [TMBC-SIGN-FORK.1]: +> *TrustedBlock* corresponds to *a*, and *PrimaryTrace* and *SecondaryTrace* +> are traces to two blocks *b* and *c*. The traces establish that both +> *skip-root(a,b,t)* and *skip-root(a,c,t)* are satisfied. #### **[LCV-DATA-POF.1]**: @@ -578,10 +607,6 @@ type LightNodeProofOfFork struct { } ``` -> [LCV-DATA-POF.1] mirrors the definition [TMBC-SIGN-FORK.1]: -> *TrustedBlock* corresponds to *a*, and *PrimaryTrace* and *SecondaryTrace* -> are traces to two blocks *b* and *c*. The traces establish that both -> *skip-root(a,b,t)* and *skip-root(a,c,t)* are satisfied. @@ -636,6 +661,8 @@ See the [verification specification][verification] for details. ```go func SubmitProofOfFork(pof LightNodeProofOfFork) Result ``` +**TODO:** finalize what this should do, and what detail of + specification we need. - Implementation remark - Expected precondition - none @@ -675,6 +702,7 @@ func CrossCheck(peer PeerID, testedLB LightBlock) (result) { } ``` - Implementation remark + - download block and compare to previously downloaded one. - Expected precondition - Expected postcondition - Error condition @@ -684,17 +712,19 @@ func CrossCheck(peer PeerID, testedLB LightBlock) (result) { ```go Replace_Primary() ``` +**TODO:** formalize conditions - Implementation remark - the primary is replaced by a secondary, and lightblocks above trusted blocks are removed - to maintain a constant size of secondaries, at this point we might need to - - pick a new secondary nsec + - pick a new secondary *nsec* - maintain [LCD-INV-TRUSTED-AGREED.1], that is, - call `CrossCheck(nsec,lightStore.LatestTrusted()`. If it matches we are OK, otherwise - - we might just repeat with another full node as new secondary - - try to do fork detection from some possibly old + - we repeat with another full node as new + secondary candidate + - **FUTURE:** try to do fork detection from some possibly old lightblock in store. (Might be the approach for the light node that assumes to be connected to correct full nodes only from time to time) @@ -712,24 +742,24 @@ Replace_Primary() - Error condition - if precondition is violated -**TODO:** pass in the lightstore to the replace functions #### **[LCD-FUNC-REPLACE-SECONDARY.1]:** ```go Replace_Secondary(addr Address) ``` +**TODO:** formalize conditions - Implementation remark - maintain [LCD-INV-TRUSTED-AGREED.1], that is, - call `CrossCheck(nsec,lightStore.LatestTrusted()`. If it matches we are OK, otherwise - - we might just repeat with another full node as new secondary - - try to do fork detection from some possibly old - lightblock in store. (Might be the approach for the - light node that assumes to be connected to correct - full nodes only from time to time) + - we might just repeat with another full node as new secondary + - **FUTURE:** try to do fork detection from some possibly old + lightblock in store. (Might be the approach for the + light node that assumes to be connected to correct + full nodes only from time to time) - Expected precondition - - *FullNodes* is nonempty + - *FullNodes* is nonempty - Expected postcondition - addr is moved from *Secondaries* to *FaultyNodes* - an address *a* is moved from *FullNodes* to *Secondaries* @@ -825,13 +855,15 @@ func ForkDetector(ls LightStore, PoFs PoFStore) return PoFs } ``` +**TODO:** formalize conditions - Expected precondition - Secondaries initialized and non-empty - `PoFs` initialized and empty + - *lightStore.LatestTrusted().Height < lightStore.LatestVerified().Height* - Expected postcondition - satisfies [LCD-DIST-INV.1], [LCD-DIST-LIFE-FORK.1] - removes faulty secondary if it reports wrong header - - **TODO** proof of fork + - **TODO** submit proof of fork - Error condition - fails if precondition is violated - fails if [LCV-INV-TP] is violated (no trusted header within From 9e8d5feda4d281003c801fc3dbcadb81a2331951 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Tue, 28 Jul 2020 08:21:26 +0200 Subject: [PATCH 12/26] preliminary work for IBC fork dectection (until upgrades) --- .../detection/req-ibc-detection.md | 34 +++++++++++++++++-- 1 file changed, 31 insertions(+), 3 deletions(-) diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index 66a0ddc6a..270c2c2de 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -15,9 +15,37 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics #### An IBC/Tendermint Dictionary -| IBC Term | Tendermint-RS Spec Term | -|----------|-------------------------| -|Commitment root is app hash | AppState | +| IBC Term | Tendermint-RS Spec Term | Comment | +|----------|-------------------------| --------| +| `CommitmentRoot` | AppState | app hash | +| `ConsensusState` | Lightblock | not all fields are there. NextValidator is definitly needed | +| `ClientState` | latest light block + configuration parameters (e.g., trusting period + `frozenHeight` | NextValidators missing | +| `frozenHeight` | height of fork | set when a fork is detected | +| "would-have-been-fooled" | light node fork detection | light node may submit proof of fork to IBC component to halt it | +| `Height` | (no epochs) | (epoch,height) pair in lexicographical order (`compare`) | +| `Header` | ~signed header | validatorSet explicit (no hash); nextValidators missing | +| `Evidence` | t.b.d. | definition unclear "which the light client would have considered valid". Data structure will need to change | +| `verify` | `ValidAndVerified` | signature does not match perfectly (ClientState vs. LightBlock) | + + +#### Required Changes in ICS 007 + +- `assert(height > 0)` in definition of `initialise` doesn't match + definition of `Height` as *(epoch,height)* pair. + +- `initialise` needs to be updated to new data structures + +- `checkValidityAndUpdateState` + - `verify`: it needs to be clarified that checkValidityAndUpdateState + does not perform "bisection" (as currently hinted in the text) but + performs a single step of "skipping verification", called, + `ValidAndVerified` + - `assert (header.height > clientState.latestHeight)`: no old + headers can be installed. This might be OK, but we need to check + interplay with misbehavior + +- `checkMisbehaviourAndUpdateState`: as evidence will contain a trace + (or two), the assertion that uses verify will need to change. #### Handler From 9355baae41771b92436f9ef2da5697e1a71c07ba Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 29 Jul 2020 15:42:34 +0200 Subject: [PATCH 13/26] draft for new checkMisbehaviourAndUpdateState --- .../detection/req-ibc-detection.md | 61 +++++++++++++++++-- 1 file changed, 57 insertions(+), 4 deletions(-) diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index 270c2c2de..2e9992b40 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -13,21 +13,27 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics > I assume you know what that is. -#### An IBC/Tendermint Dictionary +#### An IBC/Tendermint correspondence | IBC Term | Tendermint-RS Spec Term | Comment | |----------|-------------------------| --------| | `CommitmentRoot` | AppState | app hash | | `ConsensusState` | Lightblock | not all fields are there. NextValidator is definitly needed | -| `ClientState` | latest light block + configuration parameters (e.g., trusting period + `frozenHeight` | NextValidators missing | +| `ClientState` | latest light block + configuration parameters (e.g., trusting period + `frozenHeight` | NextValidators missing; what is `proofSpecs`?| | `frozenHeight` | height of fork | set when a fork is detected | | "would-have-been-fooled" | light node fork detection | light node may submit proof of fork to IBC component to halt it | | `Height` | (no epochs) | (epoch,height) pair in lexicographical order (`compare`) | | `Header` | ~signed header | validatorSet explicit (no hash); nextValidators missing | | `Evidence` | t.b.d. | definition unclear "which the light client would have considered valid". Data structure will need to change | -| `verify` | `ValidAndVerified` | signature does not match perfectly (ClientState vs. LightBlock) | +| `verify` | `ValidAndVerified` | signature does not match perfectly (ClientState vs. LightBlock) + in `checkMisbehaviourAndUpdateState` it is unclear whether it uses traces or goes to h1 and h2 in one step | +#### Some IBC links +- [QueryConsensusState](https://github.com/cosmos/cosmos-sdk/blob/2651427ab4c6ea9f81d26afa0211757fc76cf747/x/ibc/02-client/client/utils/utils.go#L68) + + + + #### Required Changes in ICS 007 - `assert(height > 0)` in definition of `initialise` doesn't match @@ -35,6 +41,11 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics - `initialise` needs to be updated to new data structures +- `clientState.frozenHeight` semantics seem not totally consistent in + document. E.g., `min` needs to be defined over optional value in + `checkMisbehaviourAndUpdateState`. Also, if you are frozen, why do + you accept more evidence. + - `checkValidityAndUpdateState` - `verify`: it needs to be clarified that checkValidityAndUpdateState does not perform "bisection" (as currently hinted in the text) but @@ -43,10 +54,52 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics - `assert (header.height > clientState.latestHeight)`: no old headers can be installed. This might be OK, but we need to check interplay with misbehavior - + - clienstState needs to be updated according to complete data + structure + - `checkMisbehaviourAndUpdateState`: as evidence will contain a trace (or two), the assertion that uses verify will need to change. +- ICS 002 states w.r.t. `queryChainConsensusState` that "Note that + retrieval of past consensus states by height (as opposed to just the + current consensus state) is convenient but not required." For + Tendermint fork detection, this seems to be a necessity. + +- `Header` should become a lightblock + +- `Evidence` should become `LightNodeProofOfFork` [LCV-DATA-POF.1] + + +```go +func checkMisbehaviourAndUpdateState(cs: ClientState, PoF: LightNodeProofOfFork) +``` +**TODO:** finish conditions +- Implementation remark +- Expected precondition + - PoF.TrustedBlock.Header.Height = to the one I have stored + - both traces end with header of same height + - header are different + - both traces are supported (`supports` defined in [TMBC-FUNC]) + by PoF.TrustedBlock, that is, for `t = currentTimestamp()` (see + ICS 024) + - supports(PoF.TrustedBlock, PoF.PrimaryTrace[1], t) + - supports(PoF.PrimaryTrace[i], PoF.PrimaryTrace[i+1], t) for + *0 < i < length(PoF.PrimaryTrace)* + - supports(PoF.TrustedBlock, PoF.SecondaryTrace[1], t) + - supports(PoF.SecondaryTrace[i], PoF.SecondaryTrace[i+1], t) for + *0 < i < length(PoF.SecondaryTrace)* +- Expected postcondition + - set cs.FrozenHeight to min(cs.FrozenHeight, PoF.TrustedBlock.Header.Height) +- Error condition + - none +---- + + +#### Things that need clarification + +- `upgradeClientState` what is the semantics (in particular what is + `height` doing. + #### Handler A blockchain runs a **handler** that passively collects information about From a2c8357b9bb1c6f1f03de1efae3d4ff98e493b24 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 30 Jul 2020 12:58:01 +0200 Subject: [PATCH 14/26] first draft of SubmitIBCProofOfFork --- .../detection/req-ibc-detection.md | 144 +++++++++++++++++- 1 file changed, 140 insertions(+), 4 deletions(-) diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index 2e9992b40..cc02e4c96 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -69,6 +69,8 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics - `Evidence` should become `LightNodeProofOfFork` [LCV-DATA-POF.1] +- `upgradeClientState` what is the semantics (in particular what is + `height` doing. ```go func checkMisbehaviourAndUpdateState(cs: ClientState, PoF: LightNodeProofOfFork) @@ -76,7 +78,8 @@ func checkMisbehaviourAndUpdateState(cs: ClientState, PoF: LightNodeProofOfFork) **TODO:** finish conditions - Implementation remark - Expected precondition - - PoF.TrustedBlock.Header.Height = to the one I have stored + - PoF.TrustedBlock.Header is equal to lightBlock on store with + same height - both traces end with header of same height - header are different - both traces are supported (`supports` defined in [TMBC-FUNC]) @@ -94,11 +97,144 @@ func checkMisbehaviourAndUpdateState(cs: ClientState, PoF: LightNodeProofOfFork) - none ---- +### Relayer proof of fork preparation and submission algorithm -#### Things that need clarification +We get as input a proof of fork and submit a proof of fork the ibc +component can verify. + +#### Auxiliary Functions + +> For the lightStore + +#### [LCV-LS-FUNC-GET-PREV.1] +```go +func (ls LightStore) GetPreviousVerified(height Height) (LightBlock, bool) +``` +- Expected postcondition + - returns a verified LightBlock, whose height is maximal among all + verified lightblocks with height smaller than `height` +---- + + + + + + + + + + +#### [TAG-LS-FUNC-CONNECT.1] +```go +func Connector (lightStore LightStore, lb LightBlock, h Height) (LightBlock, bool) +``` +- Expected postcondition + - returns a verified LightBlock from lightStore with height less + than *h* that can be + verified by lb in one step. + +**TODO:** for the above to work we need an invariant that all verified +lightblocks form a chain of trust. Otherwise, we need a lightblock +that has a chain of trust to height. + + + + +> IBC component on-chain + +#### [TAG-IBC-HEIGHTS.1] +```go +func QueryHeightsRange(id, from, to) ([]Height) +``` +- Expected postcondition + - returns all heights *h*, with *from <= h <= to* for which the + IBC component has a consensus state. +---- + +#### [TAG-EXTEND-POF.1] +```go +func extendPoF (root LightBlock, connector LightBlock, lightStore LightStore, Pof LightNodeProofofFork) + (LightNodeProofofFork} +``` +- Implementation remark + - PoF is not sufficient to convince an IBC component, so we extend + the proof of fork farther in the past +- Expected postcondition + - returns a newPOF + - newPoF.TrustedBlock = root + - let prefix = + root + + lightStore.Subtrace(connector.Header.Height, PoF.TrustedBlock.Header.Height-1) + + PoF.TrustedBlock + - newPoF.PrimaryTrace = prefix + PoF.PrimaryTrace + - newPoF.SecondaryTrace = prefix + PoF.SecondaryTrace + + +#### [TAG-SUBMIT-POF-IBC.1] +```go +func SubmitIBCProofOfFork( + lightStore LightStore, + PoF: LightNodeProofOfFork, + ibc IBCComponent) (Error) { + if ibc.queryChainConsensusState(PoF.TrustedBlock.Height) = PoF.TrustedBlock { + // IBC component has root of PoF on store, we can just submit + ibc.submitMisbehaviourToClient(ibc.id,PoF) + return Success + // note sure about the id parameter + } + else { + // the ibc component does not have the TrustedBlock and might + // even be on yet a different branch. We have to compute a PoF + // that the ibc component can verifiy based on its current knowledge + + // first we ask for the heights the ibc component is aware of + ibcHeights = ibc.QueryHeightsRange( + ibc.id, + lightStore.LowestVerified().Height, + PoF.TrustedBlock.Height - 1); + // this function does not exist yet. Alternatively, we may + // request all transactions that installed headers via CosmosSDK + + + for { + h, result = max(ibcHeights) + if result = Empty { + return CouldNotGeneratePoF + } + ibcLightBlock = ibc.queryChainConsensusState(h) + lblock, result := Connector(lightStore, ibcLightBlock, PoF.TrustedBlock.Height) + if result = success { + newPoF = extendPoF(ibcLightBlock, lblock, lightStore, PoF) + ibc.submitMisbehaviourToClient(ibc.id, newPoF) + } + else{ + ibcHeights.remove(h) + } + } + } +} +``` +**TODO:** finish conditions +- Implementation remark +- Expected precondition + - the light + - both traces end with header of same height + - header are different + - both traces are supported (`supports` defined in [TMBC-FUNC]) + by PoF.TrustedBlock, that is, for `t = currentTimestamp()` (see + ICS 024) + - supports(PoF.TrustedBlock, PoF.PrimaryTrace[1], t) + - supports(PoF.PrimaryTrace[i], PoF.PrimaryTrace[i+1], t) for + *0 < i < length(PoF.PrimaryTrace)* + - supports(PoF.TrustedBlock, PoF.SecondaryTrace[1], t) + - supports(PoF.SecondaryTrace[i], PoF.SecondaryTrace[i+1], t) for + *0 < i < length(PoF.SecondaryTrace)* +- Expected postcondition + - set cs.FrozenHeight to min(cs.FrozenHeight, PoF.TrustedBlock.Header.Height) +- Error condition + - none +---- -- `upgradeClientState` what is the semantics (in particular what is - `height` doing. #### Handler From 6b8b3cba39d8fcd27061255f6a554a4bfd00d38b Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 30 Jul 2020 13:30:32 +0200 Subject: [PATCH 15/26] common root --- .../detection/req-ibc-detection.md | 70 +++++++++++++------ 1 file changed, 47 insertions(+), 23 deletions(-) diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index cc02e4c96..dae2940d1 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -151,6 +151,44 @@ func QueryHeightsRange(id, from, to) ([]Height) IBC component has a consensus state. ---- + +#### [TAG-COMMON-ROOT.1] +```go commonRoot(lightStore LightStore, ibc IBCComponent, lblock +LightBlock) (LightBlock, LightBlock, Result) { + + // first we ask for the heights the ibc component is aware of + ibcHeights = ibc.QueryHeightsRange( + ibc.id, + lightStore.LowestVerified().Height, + lblock.Height - 1); + // this function does not exist yet. Alternatively, we may + // request all transactions that installed headers via CosmosSDK + + + for { + h, result = max(ibcHeights) + if result = Empty { + return (_, _, NoRoot) + } + ibcLightBlock = ibc.queryChainConsensusState(h) + connector, result := Connector(lightStore, ibcLightBlock, lblock.Header.Height) + if result = success { + return (ibcLightBlock, connector, Success) + } + else{ + ibcHeights.remove(h) + } + } + } +} +``` +- Expected postcondition + - returns a lightBlock b1 from the IBC component, and a lightBlock b2 + from the lightStore with height less than lblock.Header.Hight, s.t. + b1 supports b2 +---- + + #### [TAG-EXTEND-POF.1] ```go func extendPoF (root LightBlock, connector LightBlock, lightStore LightStore, Pof LightNodeProofofFork) @@ -187,30 +225,16 @@ func SubmitIBCProofOfFork( // even be on yet a different branch. We have to compute a PoF // that the ibc component can verifiy based on its current knowledge - // first we ask for the heights the ibc component is aware of - ibcHeights = ibc.QueryHeightsRange( - ibc.id, - lightStore.LowestVerified().Height, - PoF.TrustedBlock.Height - 1); - // this function does not exist yet. Alternatively, we may - // request all transactions that installed headers via CosmosSDK - + ibcLightBlock, lblock, result := commonRoot(lightStore, ibc, PoF.TrustedBlock) - for { - h, result = max(ibcHeights) - if result = Empty { - return CouldNotGeneratePoF - } - ibcLightBlock = ibc.queryChainConsensusState(h) - lblock, result := Connector(lightStore, ibcLightBlock, PoF.TrustedBlock.Height) - if result = success { - newPoF = extendPoF(ibcLightBlock, lblock, lightStore, PoF) - ibc.submitMisbehaviourToClient(ibc.id, newPoF) - } - else{ - ibcHeights.remove(h) - } - } + if result = Success { + newPoF = extendPoF(ibcLightBlock, lblock, lightStore, PoF) + ibc.submitMisbehaviourToClient(ibc.id, newPoF) + return Success + } + else{ + return CouldNotGeneratePoF + } } } ``` From a9e131dfcf20314252f61faead54cdf7bf1f1c99 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 30 Jul 2020 17:38:14 +0200 Subject: [PATCH 16/26] ibc proof of fork submission first draft --- .../lightclient/detection/req-ibc-detection.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index dae2940d1..b2252c279 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -151,9 +151,12 @@ func QueryHeightsRange(id, from, to) ([]Height) IBC component has a consensus state. ---- +**TODO:** check and do fork on ibc component #### [TAG-COMMON-ROOT.1] -```go commonRoot(lightStore LightStore, ibc IBCComponent, lblock + +```go +func commonRoot(lightStore LightStore, ibc IBCComponent, lblock LightBlock) (LightBlock, LightBlock, Result) { // first we ask for the heights the ibc component is aware of @@ -179,9 +182,9 @@ LightBlock) (LightBlock, LightBlock, Result) { ibcHeights.remove(h) } } - } } ``` + - Expected postcondition - returns a lightBlock b1 from the IBC component, and a lightBlock b2 from the lightStore with height less than lblock.Header.Hight, s.t. @@ -191,17 +194,19 @@ LightBlock) (LightBlock, LightBlock, Result) { #### [TAG-EXTEND-POF.1] ```go -func extendPoF (root LightBlock, connector LightBlock, lightStore LightStore, Pof LightNodeProofofFork) - (LightNodeProofofFork} +func extendPoF (root LightBlock, + connector LightBlock, + lightStore LightStore, + Pof LightNodeProofofFork) (LightNodeProofofFork} ``` - Implementation remark - PoF is not sufficient to convince an IBC component, so we extend the proof of fork farther in the past - Expected postcondition - - returns a newPOF + - returns a newPOF: - newPoF.TrustedBlock = root - let prefix = - root + + connector + lightStore.Subtrace(connector.Header.Height, PoF.TrustedBlock.Header.Height-1) + PoF.TrustedBlock - newPoF.PrimaryTrace = prefix + PoF.PrimaryTrace From 53a0f93c6315f914d0abf89859468ca03bd01154 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Fri, 31 Jul 2020 09:00:11 +0200 Subject: [PATCH 17/26] ibc fork detection start --- .../detection/req-ibc-detection.md | 42 ++++++++++++++++--- 1 file changed, 36 insertions(+), 6 deletions(-) diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index b2252c279..8016f49ad 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -157,8 +157,10 @@ func QueryHeightsRange(id, from, to) ([]Height) ```go func commonRoot(lightStore LightStore, ibc IBCComponent, lblock -LightBlock) (LightBlock, LightBlock, Result) { - +LightBlock) (LightBlock, LightBlock, LightStore, Result) { + + auxLS.Init + // first we ask for the heights the ibc component is aware of ibcHeights = ibc.QueryHeightsRange( ibc.id, @@ -171,12 +173,13 @@ LightBlock) (LightBlock, LightBlock, Result) { for { h, result = max(ibcHeights) if result = Empty { - return (_, _, NoRoot) + return (_, _, _, NoRoot) } ibcLightBlock = ibc.queryChainConsensusState(h) + auxLS.Update(ibcLightBlock, StateVerified); connector, result := Connector(lightStore, ibcLightBlock, lblock.Header.Height) if result = success { - return (ibcLightBlock, connector, Success) + return (ibcLightBlock, connector, auxLS, Success) } else{ ibcHeights.remove(h) @@ -188,7 +191,8 @@ LightBlock) (LightBlock, LightBlock, Result) { - Expected postcondition - returns a lightBlock b1 from the IBC component, and a lightBlock b2 from the lightStore with height less than lblock.Header.Hight, s.t. - b1 supports b2 + b1 supports b2, and a lightstore with the blocks downloaded from + the ibc component ---- @@ -213,6 +217,32 @@ func extendPoF (root LightBlock, - newPoF.SecondaryTrace = prefix + PoF.SecondaryTrace +#### [TAG-HANDLER-DETECT-FORK.1] +```go +func DetectIBCFork(ibc IBCComponent, lightStore LightStore) (LightNodeProofOfFork, Error) { + cs = ibc.queryClientState(ibc); + lb, found := lightStore.Get(cs.Header.Height) + if !found { + **TODO:** need verify to target + lb = FetchLightBlock(primary, nextHeight) + // I guess here we have to get into the light client + lightStore.Update(current, StateUnverified) + } + if cs != lb { + // IBC component disagrees with my primary. + // I fetch the + ibcLightBlock, lblock, ibcStore, result := commonRoot(lightStore, ibc, lb) + pof = new LightNodeProofOfFork; + pof.TrustedBlock := ibcLightBlock + pof.PrimaryTrace := ibcStore + cs + pof.SecondaryTrace := lightStore.Subtrace(lblock.Header.Height, + lb.Header.Height); + return(pof, Fork) + } + return(nil , NoFork) +} +``` + #### [TAG-SUBMIT-POF-IBC.1] ```go func SubmitIBCProofOfFork( @@ -230,7 +260,7 @@ func SubmitIBCProofOfFork( // even be on yet a different branch. We have to compute a PoF // that the ibc component can verifiy based on its current knowledge - ibcLightBlock, lblock, result := commonRoot(lightStore, ibc, PoF.TrustedBlock) + ibcLightBlock, lblock, _, result := commonRoot(lightStore, ibc, PoF.TrustedBlock) if result = Success { newPoF = extendPoF(ibcLightBlock, lblock, lightStore, PoF) From 43578d78745feb3bb0e5f835b8a0ed61c53bc053 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Fri, 31 Jul 2020 15:01:37 +0200 Subject: [PATCH 18/26] sequence of proof --- .../lightclient/detection/req-ibc-detection.md | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index 8016f49ad..7f858ef5d 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -151,7 +151,7 @@ func QueryHeightsRange(id, from, to) ([]Height) IBC component has a consensus state. ---- -**TODO:** check and do fork on ibc component + #### [TAG-COMMON-ROOT.1] @@ -224,9 +224,12 @@ func DetectIBCFork(ibc IBCComponent, lightStore LightStore) (LightNodeProofOfFor lb, found := lightStore.Get(cs.Header.Height) if !found { **TODO:** need verify to target - lb = FetchLightBlock(primary, nextHeight) + lb, result = LightClient.Main(primary, lightStore, cs.Header.Height) + // [LCV-FUNC-IBCMAIN.1] + **TODO** decide what to do following the outcome of Issue #499 + // I guess here we have to get into the light client - lightStore.Update(current, StateUnverified) + } if cs != lb { // IBC component disagrees with my primary. @@ -242,6 +245,14 @@ func DetectIBCFork(ibc IBCComponent, lightStore LightStore) (LightNodeProofOfFor return(nil , NoFork) } ``` +**TODO:** finish conditions +- Implementation remark + - we ask the handle for the lastest check. Cross-check with the + chain. In case they deviate we generate PoF. + - we assume IBC component is correct. It has verified the + consensus state +- Expected precondition +- Expected postcondition #### [TAG-SUBMIT-POF-IBC.1] ```go From f62a8cbb5858653e13c36e34eb85df07ede75fb8 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Mon, 3 Aug 2020 09:04:04 +0200 Subject: [PATCH 19/26] Update docs/spec/lightclient/detection/detection.md Co-authored-by: Ethan Buchman --- docs/spec/lightclient/detection/detection.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 950943786..b411dad6a 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -40,7 +40,7 @@ This document contains: contains several light blocks) we should submit right away. -- decision: "full" proof of fork consists of two traces that origin in the +- decision: "full" proof of fork consists of two traces that originate in the same lightblock and lead to conflicting headers of the same height. - For submission of proof of fork, we may do some optimizations, for From 5e461d999b43cae1f2cc08d3c0ceb31823dacdc3 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Tue, 4 Aug 2020 15:06:56 +0200 Subject: [PATCH 20/26] Update docs/spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic --- docs/spec/lightclient/detection/detection.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index b411dad6a..aafac43d8 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -81,7 +81,7 @@ We describe the context on which the fork detector is called by giving a sequential version of the supervisor function. Roughly, it alternates two phases namely: - Light Client Verification. As a result, a header of the required - height has been downloaded from and verified with the primary + height has been downloaded from and verified with the primary. - Light Client Fork Detections. As a result the header has been cross-checked with the secondaries. In case the is a fork we submit "proof of fork" and exit. From 3e86d7069263157a0350f2b015c34588bcd6554c Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Tue, 4 Aug 2020 15:07:11 +0200 Subject: [PATCH 21/26] Update docs/spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic --- docs/spec/lightclient/detection/detection.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index aafac43d8..57cd99dba 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -83,7 +83,7 @@ Roughly, it alternates two phases namely: - Light Client Verification. As a result, a header of the required height has been downloaded from and verified with the primary. - Light Client Fork Detections. As a result the header has been - cross-checked with the secondaries. In case the is a fork we + cross-checked with the secondaries. In case there is a fork we submit "proof of fork" and exit. From 1f8f2c25fb125952b9c623713fd5eb4adbf17a5d Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Tue, 4 Aug 2020 15:07:21 +0200 Subject: [PATCH 22/26] Update docs/spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic --- docs/spec/lightclient/detection/detection.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 57cd99dba..90b39910e 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -102,7 +102,7 @@ func Sequential-Supervisor () (Error) { // Verify result := NoResult; while result != ResultSuccess { - lightStore,result := VerifyToTarget(primary, lightStore, nextheight); + lightStore,result := VerifyToTarget(primary, lightStore, nextHeight); if result == ResultFailure { // pick new primary (promote a secondary to primary) /// and delete all lightblocks above From d85a29ccf46133534f5268b09c771bc47eb36caf Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Tue, 4 Aug 2020 15:07:37 +0200 Subject: [PATCH 23/26] Update docs/spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic --- docs/spec/lightclient/detection/detection.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 90b39910e..5aed41d3f 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -97,7 +97,7 @@ Roughly, it alternates two phases namely: func Sequential-Supervisor () (Error) { loop { // get the next height - nextheight := input(); + nextHeight := input(); // Verify result := NoResult; From 7188c3f83d68af0dd30a657ff72ad73e7096c04a Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 5 Aug 2020 10:07:35 +0200 Subject: [PATCH 24/26] draft functions --- .../lightclient/detection/draft-functions.md | 283 ++++++++++++++++++ .../detection/req-ibc-detection.md | 235 +-------------- 2 files changed, 287 insertions(+), 231 deletions(-) create mode 100644 docs/spec/lightclient/detection/draft-functions.md diff --git a/docs/spec/lightclient/detection/draft-functions.md b/docs/spec/lightclient/detection/draft-functions.md new file mode 100644 index 000000000..e2d9588a8 --- /dev/null +++ b/docs/spec/lightclient/detection/draft-functions.md @@ -0,0 +1,283 @@ +# Draft of Functions for Fork detection and Proof of Fork Submisstion + +This document collects drafts of function for generating and +submitting proof of fork in the IBC context + +- [IBC](#on---chain-ibc-component) + +- [Relayer](#relayer) + + +## On-chain IBC Component + +> The following is a suggestions to change the function defined in ICS 007 + +#### [TAG-IBC-MISBEHAVIOR.1] +```go +func checkMisbehaviourAndUpdateState(cs: ClientState, PoF: LightNodeProofOfFork) +``` +**TODO:** finish conditions +- Implementation remark +- Expected precondition + - PoF.TrustedBlock.Header is equal to lightBlock on store with + same height + - both traces end with header of same height + - headers are different + - both traces are supported by PoF.TrustedBlock (`supports` + defined in [TMBC-FUNC]), that is, for `t = currentTimestamp()` (see + ICS 024) + - supports(PoF.TrustedBlock, PoF.PrimaryTrace[1], t) + - supports(PoF.PrimaryTrace[i], PoF.PrimaryTrace[i+1], t) for + *0 < i < length(PoF.PrimaryTrace)* + - supports(PoF.TrustedBlock, PoF.SecondaryTrace[1], t) + - supports(PoF.SecondaryTrace[i], PoF.SecondaryTrace[i+1], t) for + *0 < i < length(PoF.SecondaryTrace)* +- Expected postcondition + - set cs.FrozenHeight to min(cs.FrozenHeight, PoF.TrustedBlock.Header.Height) +- Error condition + - none +---- + +> The following is a suggestions to add functionality to ICS 002 and 007. +> I suppose the above is the most efficient way to get the required +> information. Another option is to subscribe to "header install" +> events via CosmosSDK + +#### [TAG-IBC-HEIGHTS.1] +```go +func QueryHeightsRange(id, from, to) ([]Height) +``` +- Expected postcondition + - returns all heights *h*, with *from <= h <= to* for which the + IBC component has a consensus state. +---- + +> This function can be used if the relayer has no information about +> the IBC component. This allows late-joining relayers to also +> participate in fork dection and the generation in proof of +> fork. Alternatively, we may also postulate that relayers are not +> responsible to detect forks for heights before they started (and +> subscribed to the transactions reporting fresh headers being +> installed at the IBC component). + +## Relayer + +### Auxiliary Functions to be implemented in the Light Client + +#### [LCV-LS-FUNC-GET-PREV.1] +```go +func (ls LightStore) GetPreviousVerified(height Height) (LightBlock, bool) +``` +- Expected postcondition + - returns a verified LightBlock, whose height is maximal among all + verified lightblocks with height smaller than `height` +---- + +### Relayer Submitting Proof of Fork to the IBC Component + +There are two ways the relayer can detect a fork +- by the fork detector of one of its lightclients +- be checking the consensus state of the IBC component + +The following function ignores how the proof of fork was generated. +It takes a proof of fork as input and computes a proof of fork that + will be accepted by the IBC component. +The problem addressed here is that both, the relayer's light client + and the IBC component have incomplete light stores, that might + not have all light blocks in common. +Hence the relayer has to figure out what the IBC component knows + (intuitively, a meeting point between the two lightstores + computed in `commonRoot`) and compute a proof of fork + (`extendPoF`) that the IBC component will accept based on its + knowledge. + +The auxiliary functions `commonRoot` and `extendPoF` are +defined below. + +#### [TAG-SUBMIT-POF-IBC.1] +```go +func SubmitIBCProofOfFork( + lightStore LightStore, + PoF: LightNodeProofOfFork, + ibc IBCComponent) (Error) { + if ibc.queryChainConsensusState(PoF.TrustedBlock.Height) = PoF.TrustedBlock { + // IBC component has root of PoF on store, we can just submit + ibc.submitMisbehaviourToClient(ibc.id,PoF) + return Success + // note sure about the id parameter + } + else { + // the ibc component does not have the TrustedBlock and might + // even be on yet a different branch. We have to compute a PoF + // that the ibc component can verifiy based on its current + // knowledge + + ibcLightBlock, lblock, _, result := commonRoot(lightStore, ibc, PoF.TrustedBlock) + + if result = Success { + newPoF = extendPoF(ibcLightBlock, lblock, lightStore, PoF) + ibc.submitMisbehaviourToClient(ibc.id, newPoF) + return Success + } + else{ + return CouldNotGeneratePoF + } + } +} +``` +**TODO:** finish conditions +- Implementation remark +- Expected precondition +- Expected postcondition +- Error condition + - none +---- + + +### Auxiliary Functions at the Relayer + + + + + + +> If the relayer detects a fork, it has to compute a proof of fork that +> will convince the IBC component. That is it has to compare the +> relayer's local lightstore against the lightstore of the IBC +> component, and find common ancestor lightblocks. + + + +#### [TAG-COMMON-ROOT.1] + +```go +func commonRoot(lightStore LightStore, ibc IBCComponent, lblock +LightBlock) (LightBlock, LightBlock, LightStore, Result) { + + auxLS.Init + + // first we ask for the heights the ibc component is aware of + ibcHeights = ibc.QueryHeightsRange( + ibc.id, + lightStore.LowestVerified().Height, + lblock.Height - 1); + // this function does not exist yet. Alternatively, we may + // request all transactions that installed headers via CosmosSDK + + + for { + h, result = max(ibcHeights) + if result = Empty { + return (_, _, _, NoRoot) + } + ibcLightBlock = ibc.queryChainConsensusState(h) + auxLS.Update(ibcLightBlock, StateVerified); + connector, result := Connector(lightStore, ibcLightBlock, lblock.Header.Height) + if result = success { + return (ibcLightBlock, connector, auxLS, Success) + } + else{ + ibcHeights.remove(h) + } + } +} +``` + +- Expected postcondition + - returns + - a lightBlock b1 from the IBC component, and + - a lightBlock b2 + from the local lightStore with height less than + lblock.Header.Hight, s.t. b1 supports b2, and + - a lightstore with the blocks downloaded from + the ibc component +---- + + + +#### [TAG-LS-FUNC-CONNECT.1] +```go +func Connector (lightStore LightStore, lb LightBlock, h Height) (LightBlock, bool) +``` +- Expected postcondition + - returns a verified LightBlock from lightStore with height less + than *h* that can be + verified by lb in one step. + +**TODO:** for the above to work we need an invariant that all verified +lightblocks form a chain of trust. Otherwise, we need a lightblock +that has a chain of trust to height. + + + +> Once the common root is found, a proof of fork that will be accepted +> by the IBC component needs to be generated. This is done in the +> following function. + + +#### [TAG-EXTEND-POF.1] +```go +func extendPoF (root LightBlock, + connector LightBlock, + lightStore LightStore, + Pof LightNodeProofofFork) (LightNodeProofofFork} +``` +- Implementation remark + - PoF is not sufficient to convince an IBC component, so we extend + the proof of fork farther in the past +- Expected postcondition + - returns a newPOF: + - newPoF.TrustedBlock = root + - let prefix = + connector + + lightStore.Subtrace(connector.Header.Height, PoF.TrustedBlock.Header.Height-1) + + PoF.TrustedBlock + - newPoF.PrimaryTrace = prefix + PoF.PrimaryTrace + - newPoF.SecondaryTrace = prefix + PoF.SecondaryTrace + + + +### Detection a fork at the IBC component + +The following functions is assumed to be called regularly to check +that latest consensus state of the IBC component. Alternatively, this +logic can be executed whenever the relayer is informed (via an event) +that a new header has been installed. + + +#### [TAG-HANDLER-DETECT-FORK.1] +```go +func DetectIBCFork(ibc IBCComponent, lightStore LightStore) (LightNodeProofOfFork, Error) { + cs = ibc.queryClientState(ibc); + lb, found := lightStore.Get(cs.Header.Height) + if !found { + **TODO:** need verify to target + lb, result = LightClient.Main(primary, lightStore, cs.Header.Height) + // [LCV-FUNC-IBCMAIN.1] + **TODO** decide what to do following the outcome of Issue #499 + + // I guess here we have to get into the light client + + } + if cs != lb { + // IBC component disagrees with my primary. + // I fetch the + ibcLightBlock, lblock, ibcStore, result := commonRoot(lightStore, ibc, lb) + pof = new LightNodeProofOfFork; + pof.TrustedBlock := ibcLightBlock + pof.PrimaryTrace := ibcStore + cs + pof.SecondaryTrace := lightStore.Subtrace(lblock.Header.Height, + lb.Header.Height); + return(pof, Fork) + } + return(nil , NoFork) +} +``` +**TODO:** finish conditions +- Implementation remark + - we ask the handler for the lastest check. Cross-check with the + chain. In case they deviate we generate PoF. + - we assume IBC component is correct. It has verified the + consensus state +- Expected precondition +- Expected postcondition diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index 7f858ef5d..f811bd5de 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -70,240 +70,13 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics - `Evidence` should become `LightNodeProofOfFork` [LCV-DATA-POF.1] - `upgradeClientState` what is the semantics (in particular what is - `height` doing. - -```go -func checkMisbehaviourAndUpdateState(cs: ClientState, PoF: LightNodeProofOfFork) -``` -**TODO:** finish conditions -- Implementation remark -- Expected precondition - - PoF.TrustedBlock.Header is equal to lightBlock on store with - same height - - both traces end with header of same height - - header are different - - both traces are supported (`supports` defined in [TMBC-FUNC]) - by PoF.TrustedBlock, that is, for `t = currentTimestamp()` (see - ICS 024) - - supports(PoF.TrustedBlock, PoF.PrimaryTrace[1], t) - - supports(PoF.PrimaryTrace[i], PoF.PrimaryTrace[i+1], t) for - *0 < i < length(PoF.PrimaryTrace)* - - supports(PoF.TrustedBlock, PoF.SecondaryTrace[1], t) - - supports(PoF.SecondaryTrace[i], PoF.SecondaryTrace[i+1], t) for - *0 < i < length(PoF.SecondaryTrace)* -- Expected postcondition - - set cs.FrozenHeight to min(cs.FrozenHeight, PoF.TrustedBlock.Header.Height) -- Error condition - - none ----- - -### Relayer proof of fork preparation and submission algorithm - -We get as input a proof of fork and submit a proof of fork the ibc -component can verify. - -#### Auxiliary Functions - -> For the lightStore - -#### [LCV-LS-FUNC-GET-PREV.1] -```go -func (ls LightStore) GetPreviousVerified(height Height) (LightBlock, bool) -``` -- Expected postcondition - - returns a verified LightBlock, whose height is maximal among all - verified lightblocks with height smaller than `height` ----- - - - - - - - - - - -#### [TAG-LS-FUNC-CONNECT.1] -```go -func Connector (lightStore LightStore, lb LightBlock, h Height) (LightBlock, bool) -``` -- Expected postcondition - - returns a verified LightBlock from lightStore with height less - than *h* that can be - verified by lb in one step. - -**TODO:** for the above to work we need an invariant that all verified -lightblocks form a chain of trust. Otherwise, we need a lightblock -that has a chain of trust to height. - - - - -> IBC component on-chain - -#### [TAG-IBC-HEIGHTS.1] -```go -func QueryHeightsRange(id, from, to) ([]Height) -``` -- Expected postcondition - - returns all heights *h*, with *from <= h <= to* for which the - IBC component has a consensus state. ----- - - - -#### [TAG-COMMON-ROOT.1] - -```go -func commonRoot(lightStore LightStore, ibc IBCComponent, lblock -LightBlock) (LightBlock, LightBlock, LightStore, Result) { - - auxLS.Init - - // first we ask for the heights the ibc component is aware of - ibcHeights = ibc.QueryHeightsRange( - ibc.id, - lightStore.LowestVerified().Height, - lblock.Height - 1); - // this function does not exist yet. Alternatively, we may - // request all transactions that installed headers via CosmosSDK - - - for { - h, result = max(ibcHeights) - if result = Empty { - return (_, _, _, NoRoot) - } - ibcLightBlock = ibc.queryChainConsensusState(h) - auxLS.Update(ibcLightBlock, StateVerified); - connector, result := Connector(lightStore, ibcLightBlock, lblock.Header.Height) - if result = success { - return (ibcLightBlock, connector, auxLS, Success) - } - else{ - ibcHeights.remove(h) - } - } -} -``` + `height` doing?). + +- `checkMisbehaviourAndUpdateState(cs: ClientState, PoF: + LightNodeProofOfFork)` needs to be adapted -- Expected postcondition - - returns a lightBlock b1 from the IBC component, and a lightBlock b2 - from the lightStore with height less than lblock.Header.Hight, s.t. - b1 supports b2, and a lightstore with the blocks downloaded from - the ibc component ----- -#### [TAG-EXTEND-POF.1] -```go -func extendPoF (root LightBlock, - connector LightBlock, - lightStore LightStore, - Pof LightNodeProofofFork) (LightNodeProofofFork} -``` -- Implementation remark - - PoF is not sufficient to convince an IBC component, so we extend - the proof of fork farther in the past -- Expected postcondition - - returns a newPOF: - - newPoF.TrustedBlock = root - - let prefix = - connector + - lightStore.Subtrace(connector.Header.Height, PoF.TrustedBlock.Header.Height-1) + - PoF.TrustedBlock - - newPoF.PrimaryTrace = prefix + PoF.PrimaryTrace - - newPoF.SecondaryTrace = prefix + PoF.SecondaryTrace - - -#### [TAG-HANDLER-DETECT-FORK.1] -```go -func DetectIBCFork(ibc IBCComponent, lightStore LightStore) (LightNodeProofOfFork, Error) { - cs = ibc.queryClientState(ibc); - lb, found := lightStore.Get(cs.Header.Height) - if !found { - **TODO:** need verify to target - lb, result = LightClient.Main(primary, lightStore, cs.Header.Height) - // [LCV-FUNC-IBCMAIN.1] - **TODO** decide what to do following the outcome of Issue #499 - - // I guess here we have to get into the light client - - } - if cs != lb { - // IBC component disagrees with my primary. - // I fetch the - ibcLightBlock, lblock, ibcStore, result := commonRoot(lightStore, ibc, lb) - pof = new LightNodeProofOfFork; - pof.TrustedBlock := ibcLightBlock - pof.PrimaryTrace := ibcStore + cs - pof.SecondaryTrace := lightStore.Subtrace(lblock.Header.Height, - lb.Header.Height); - return(pof, Fork) - } - return(nil , NoFork) -} -``` -**TODO:** finish conditions -- Implementation remark - - we ask the handle for the lastest check. Cross-check with the - chain. In case they deviate we generate PoF. - - we assume IBC component is correct. It has verified the - consensus state -- Expected precondition -- Expected postcondition - -#### [TAG-SUBMIT-POF-IBC.1] -```go -func SubmitIBCProofOfFork( - lightStore LightStore, - PoF: LightNodeProofOfFork, - ibc IBCComponent) (Error) { - if ibc.queryChainConsensusState(PoF.TrustedBlock.Height) = PoF.TrustedBlock { - // IBC component has root of PoF on store, we can just submit - ibc.submitMisbehaviourToClient(ibc.id,PoF) - return Success - // note sure about the id parameter - } - else { - // the ibc component does not have the TrustedBlock and might - // even be on yet a different branch. We have to compute a PoF - // that the ibc component can verifiy based on its current knowledge - - ibcLightBlock, lblock, _, result := commonRoot(lightStore, ibc, PoF.TrustedBlock) - - if result = Success { - newPoF = extendPoF(ibcLightBlock, lblock, lightStore, PoF) - ibc.submitMisbehaviourToClient(ibc.id, newPoF) - return Success - } - else{ - return CouldNotGeneratePoF - } - } -} -``` -**TODO:** finish conditions -- Implementation remark -- Expected precondition - - the light - - both traces end with header of same height - - header are different - - both traces are supported (`supports` defined in [TMBC-FUNC]) - by PoF.TrustedBlock, that is, for `t = currentTimestamp()` (see - ICS 024) - - supports(PoF.TrustedBlock, PoF.PrimaryTrace[1], t) - - supports(PoF.PrimaryTrace[i], PoF.PrimaryTrace[i+1], t) for - *0 < i < length(PoF.PrimaryTrace)* - - supports(PoF.TrustedBlock, PoF.SecondaryTrace[1], t) - - supports(PoF.SecondaryTrace[i], PoF.SecondaryTrace[i+1], t) for - *0 < i < length(PoF.SecondaryTrace)* -- Expected postcondition - - set cs.FrozenHeight to min(cs.FrozenHeight, PoF.TrustedBlock.Header.Height) -- Error condition - - none ----- #### Handler From 9e8cbd07a1cc020275ff24e797659276600b0c31 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Fri, 7 Aug 2020 12:14:02 +0200 Subject: [PATCH 25/26] added todo into verification.md --- .../lightclient/verification/verification.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/docs/spec/lightclient/verification/verification.md b/docs/spec/lightclient/verification/verification.md index 8a45ba752..d95d54a62 100644 --- a/docs/spec/lightclient/verification/verification.md +++ b/docs/spec/lightclient/verification/verification.md @@ -23,6 +23,22 @@ This specification tries to reduce the number of intermediate blocks that need to be checked, by exploiting the guarantees provided by the [security model][TMBC-FM-2THIRDS-link]. +# Status + +This document is thoroughly reviewed, and the protocol has been +formalized in TLA+ and model checked. + +## Issues that need to be addressed + +As it is part of the larger light node, its data structures and +functions interact with the fork dectection functionality of the light +client. As a result of the work on +[Pull Request 479](https://github.com/informalsystems/tendermint-rs/pull/479) we +established the need for an update in the data structures in [Issue 499](https://github.com/informalsystems/tendermint-rs/issues/499). This +will not change the verification logic, but it will record information +about verification that can be used in fork detection (in particular +in computing more efficiently the proof of fork). + # Outline - [Part I](#part-i---tendermint-blockchain): Introduction of From 5259bb61177a504df30b88f42bb16a33a7701eca Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Fri, 7 Aug 2020 15:44:40 +0200 Subject: [PATCH 26/26] clean up ready to merge --- docs/spec/lightclient/detection/README.md | 71 +++++++ docs/spec/lightclient/detection/detection.md | 193 ------------------ .../spec/lightclient/detection/discussions.md | 186 +++++++++++++++++ .../detection/req-ibc-detection.md | 14 -- 4 files changed, 257 insertions(+), 207 deletions(-) create mode 100644 docs/spec/lightclient/detection/README.md create mode 100644 docs/spec/lightclient/detection/discussions.md diff --git a/docs/spec/lightclient/detection/README.md b/docs/spec/lightclient/detection/README.md new file mode 100644 index 000000000..d4c372bd7 --- /dev/null +++ b/docs/spec/lightclient/detection/README.md @@ -0,0 +1,71 @@ +# Tendermint fork detection and IBC fork detection + +## Status + +This directory captures the ongoing work and discussion on fork +detection both in the context of a Tendermint light node and in the +context of IBC. It contains the following files + +### [detection.md](./detection.md) + +a draft of the light node fork detection including "proof of fork" + definition, that is, the data structure to submit evidence to full + nodes. + + +### [discussions.md](./discussions.md) + +A collection of ideas and intuitions from recent discussions + +- the outcome of recent discussion +- a sketch of the light client supervisor to provide the context in + which fork detection happens +- a discussion about lightstore semantics + + +### [req-ibc-detection.md](./req-ibc-detection.md) + +- a collection of requirements for fork detection in the IBC + context. In particular it contains a section "Required Changes in + ICS 007" with necessary updates to ICS 007 to support Tendermint + fork detection + + +### [draft-functions.md](./draft-functions.md) + +In order to address the collected requirements, we started to sketch +some functions that we will need in the future when we specify in more +detail the + +- fork detections +- proof of fork generation +- proof of fork verification + +on the following components. + +- IBC on-chain components +- Relayer + + +### TODOs + +We decided to merge the files while there are still open points to +address to record the current state an move forward. In particular, +the following points need to be addressed: + +- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466504876 + +- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466493900 + +- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466489045 + +- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466491471 + +Most likely we will write a specification on the light client +supervisor along the outcomes of + +- https://github.com/informalsystems/tendermint-rs/pull/509 + +that also addresses initialization + +- https://github.com/tendermint/spec/issues/131 diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md index 5aed41d3f..b743678a8 100644 --- a/docs/spec/lightclient/detection/detection.md +++ b/docs/spec/lightclient/detection/detection.md @@ -1,199 +1,6 @@ ***This an unfinished draft. Comments are welcome!*** -This document contains: - -- the outcome of recent discussion -- a sketch of the light client supervisor to provide the context in - which fork detection happens -- a discussion about lightstore semantics -- a draft of the light node fork detection including "proof of fork" - definition, that is, the data structure to submit evidence to full - nodes. - - -## Results of Discussions and Decisions - -- Generating a minimal proof of fork (as suggested in [Issue #5083](https://github.com/tendermint/tendermint/issues/5083)) is too costly at the light client - - we do not know all lightblocks from the primary - - therefore there are many scenarios. we might even need to ask - the primary again for additional lightblocks to isolate the - branch. -> For instance, the light node starts with block at height 1 and the -> primary provides a block of height 10 that the light node can -> verify immediately. In cross-checking, a secondary now provides a -> conflicting header b10 of height 10 that needs another header b5 -> of height 5 to -> verify. Now, in order for the light node to convince the primary: -> - The light node cannot just sent b5, as it is not clear whether -> the fork happened before or after 5 -> - The light node cannot just send b10, as the primary would also -> need b5 for verification -> - In order to minimize the evidence, the light node may try to -> figure out where the branch happens, e.g., by asking the primary -> for height 5 (it might be that more queries are required, also -> to the secondary. However, assuming that in this scenario the -> primary is faulty it may not respond. - - As the main goal is to catch misbehavior of the primary, - evidence generation and punishment must not depend on their - cooperation. So the moment we have proof of fork (even if it - contains several light blocks) we should submit right away. - - -- decision: "full" proof of fork consists of two traces that originate in the - same lightblock and lead to conflicting headers of the same height. - -- For submission of proof of fork, we may do some optimizations, for - instance, we might just submit a trace of lightblocks that verifies a block - different from the one the full node knows (we do not send the trace - the primary gave us back to the primary) - -- The light client attack is via the primary. Thus we try to - catch if the primary installs a bad light block - - We do not check secondary against secondary - - For each secondary, we check the primary against one secondary - - -- Observe that just two blocks for the same height are not -sufficient proof of fork. -One of the blocks may be bogus [TMBC-BOGUS.1] which does -not constitute slashable behavior. -Which leads to the question whether the light node should try to do -fork detection on its initial block (from subjective -initialization). This could be done by doing backwards verification -(with the hashes) until a bifurcation block is found. -While there are scenarios where a -fork could be found, there is also the scenario where a faulty full -node feeds the light node with bogus light blocks and forces the light -node to check hashes until a bogus chain is out of the trusting period. -As a result, the light client -should not try to detect a fork for its initial header. **The initial -header must be trusted as is.** - - -# Light Client Sequential Supervisor - -**TODO:** decide where (into which specification) to put the -following: - - -We describe the context on which the fork detector is called by giving -a sequential version of the supervisor function. -Roughly, it alternates two phases namely: - - Light Client Verification. As a result, a header of the required - height has been downloaded from and verified with the primary. - - Light Client Fork Detections. As a result the header has been - cross-checked with the secondaries. In case there is a fork we - submit "proof of fork" and exit. - - - - - - -#### **[LC-FUNC-SUPERVISOR.1]:** - -```go -func Sequential-Supervisor () (Error) { - loop { - // get the next height - nextHeight := input(); - - // Verify - result := NoResult; - while result != ResultSuccess { - lightStore,result := VerifyToTarget(primary, lightStore, nextHeight); - if result == ResultFailure { - // pick new primary (promote a secondary to primary) - /// and delete all lightblocks above - // LastTrusted (they have not been cross-checked) - Replace_Primary(); - } - } - - // Cross-check - PoFs := Forkdetector(lightStore, PoFs); - if PoFs.Empty { - // no fork detected with secondaries, we trust the new - // lightblock - LightStore.Update(testedLB, StateTrusted); - } - else { - // there is a fork, we submit the proofs and exit - for i, p range PoFs { - SubmitProofOfFork(p); - } - return(ErrorFork); - } - } -} -``` -**TODO:** finish conditions -- Implementation remark -- Expected precondition - - *lightStore* initialized with trusted header - - *PoFs* empty -- Expected postcondition - - runs forever, or - - is terminated by user and satisfies LightStore invariant, or **TODO** - - has submitted proof of fork upon detecting a fork -- Error condition - - none ----- - -# Semantics of the LightStore - -Currently, a lightblock in the lightstore can be in one of the -following states: -- StateUnverified -- StateVerified -- StateFailed -- StateTrusted - -The intuition is that `StateVerified` captures that the lightblock has -been verified with the primary, and `StateTrusted` is the state after -successful cross-checking with the secondaries. - -Assuming there is **always one correct node among primary and -secondaries**, and there is no fork on the blockchain, lightblocks that -are in `StateTrusted` can be used by the user with the guarantee of -"finality". If a block in `StateVerified` is used, it might be that -detection later finds a fork, and a roll-back might be needed. - -**Remark:** The assumption of one correct node, does not render -verification useless. It is true that if the primary and the -secondaries return the same block we may trust it. However, if there -is a node that provides a different block, the light node still needs -verification to understand whether there is a fork, or whether the -different block is just bogus (without any support of some previous -validator set). - -**Remark:** A light node may choose the full nodes it communicates -with (the light node and the full node might even belong to the same -stakeholder) so the assumption might be justified in some cases. - -In the future, we will do the following changes - - we assume that only from time to time, the light node is - connected to a correct full node - - this means for some limited time, the light node might have no - means to defend against light client attacks - - as a result we do not have finality - - once the light node reconnects with a correct full node, it - should detect the light client attack and submit evidence. - -Under these assumptions, `StateTrusted` loses its meaning. As a -result, it should be removed from the API. We suggest that we replace -it with a flag "trusted" that can be used -- internally for efficiency reasons (to maintain - [LCD-INV-TRUSTED-AGREED.1] until a fork is detected) -- by light client based on the "one correct full node" assumption - - ----- - - -> This is where the actual specification is going to start # Fork detector diff --git a/docs/spec/lightclient/detection/discussions.md b/docs/spec/lightclient/detection/discussions.md new file mode 100644 index 000000000..01d98d991 --- /dev/null +++ b/docs/spec/lightclient/detection/discussions.md @@ -0,0 +1,186 @@ + + + +## Results of Discussions and Decisions + +- Generating a minimal proof of fork (as suggested in [Issue #5083](https://github.com/tendermint/tendermint/issues/5083)) is too costly at the light client + - we do not know all lightblocks from the primary + - therefore there are many scenarios. we might even need to ask + the primary again for additional lightblocks to isolate the + branch. +> For instance, the light node starts with block at height 1 and the +> primary provides a block of height 10 that the light node can +> verify immediately. In cross-checking, a secondary now provides a +> conflicting header b10 of height 10 that needs another header b5 +> of height 5 to +> verify. Now, in order for the light node to convince the primary: +> - The light node cannot just sent b5, as it is not clear whether +> the fork happened before or after 5 +> - The light node cannot just send b10, as the primary would also +> need b5 for verification +> - In order to minimize the evidence, the light node may try to +> figure out where the branch happens, e.g., by asking the primary +> for height 5 (it might be that more queries are required, also +> to the secondary. However, assuming that in this scenario the +> primary is faulty it may not respond. + + As the main goal is to catch misbehavior of the primary, + evidence generation and punishment must not depend on their + cooperation. So the moment we have proof of fork (even if it + contains several light blocks) we should submit right away. + + +- decision: "full" proof of fork consists of two traces that originate in the + same lightblock and lead to conflicting headers of the same height. + +- For submission of proof of fork, we may do some optimizations, for + instance, we might just submit a trace of lightblocks that verifies a block + different from the one the full node knows (we do not send the trace + the primary gave us back to the primary) + +- The light client attack is via the primary. Thus we try to + catch if the primary installs a bad light block + - We do not check secondary against secondary + - For each secondary, we check the primary against one secondary + + +- Observe that just two blocks for the same height are not +sufficient proof of fork. +One of the blocks may be bogus [TMBC-BOGUS.1] which does +not constitute slashable behavior. +Which leads to the question whether the light node should try to do +fork detection on its initial block (from subjective +initialization). This could be done by doing backwards verification +(with the hashes) until a bifurcation block is found. +While there are scenarios where a +fork could be found, there is also the scenario where a faulty full +node feeds the light node with bogus light blocks and forces the light +node to check hashes until a bogus chain is out of the trusting period. +As a result, the light client +should not try to detect a fork for its initial header. **The initial +header must be trusted as is.** + + +# Light Client Sequential Supervisor + +**TODO:** decide where (into which specification) to put the +following: + + +We describe the context on which the fork detector is called by giving +a sequential version of the supervisor function. +Roughly, it alternates two phases namely: + - Light Client Verification. As a result, a header of the required + height has been downloaded from and verified with the primary. + - Light Client Fork Detections. As a result the header has been + cross-checked with the secondaries. In case there is a fork we + submit "proof of fork" and exit. + + + + + + +#### **[LC-FUNC-SUPERVISOR.1]:** + +```go +func Sequential-Supervisor () (Error) { + loop { + // get the next height + nextHeight := input(); + + // Verify + result := NoResult; + while result != ResultSuccess { + lightStore,result := VerifyToTarget(primary, lightStore, nextHeight); + if result == ResultFailure { + // pick new primary (promote a secondary to primary) + /// and delete all lightblocks above + // LastTrusted (they have not been cross-checked) + Replace_Primary(); + } + } + + // Cross-check + PoFs := Forkdetector(lightStore, PoFs); + if PoFs.Empty { + // no fork detected with secondaries, we trust the new + // lightblock + LightStore.Update(testedLB, StateTrusted); + } + else { + // there is a fork, we submit the proofs and exit + for i, p range PoFs { + SubmitProofOfFork(p); + } + return(ErrorFork); + } + } +} +``` +**TODO:** finish conditions +- Implementation remark +- Expected precondition + - *lightStore* initialized with trusted header + - *PoFs* empty +- Expected postcondition + - runs forever, or + - is terminated by user and satisfies LightStore invariant, or **TODO** + - has submitted proof of fork upon detecting a fork +- Error condition + - none +---- + +# Semantics of the LightStore + +Currently, a lightblock in the lightstore can be in one of the +following states: +- StateUnverified +- StateVerified +- StateFailed +- StateTrusted + +The intuition is that `StateVerified` captures that the lightblock has +been verified with the primary, and `StateTrusted` is the state after +successful cross-checking with the secondaries. + +Assuming there is **always one correct node among primary and +secondaries**, and there is no fork on the blockchain, lightblocks that +are in `StateTrusted` can be used by the user with the guarantee of +"finality". If a block in `StateVerified` is used, it might be that +detection later finds a fork, and a roll-back might be needed. + +**Remark:** The assumption of one correct node, does not render +verification useless. It is true that if the primary and the +secondaries return the same block we may trust it. However, if there +is a node that provides a different block, the light node still needs +verification to understand whether there is a fork, or whether the +different block is just bogus (without any support of some previous +validator set). + +**Remark:** A light node may choose the full nodes it communicates +with (the light node and the full node might even belong to the same +stakeholder) so the assumption might be justified in some cases. + +In the future, we will do the following changes + - we assume that only from time to time, the light node is + connected to a correct full node + - this means for some limited time, the light node might have no + means to defend against light client attacks + - as a result we do not have finality + - once the light node reconnects with a correct full node, it + should detect the light client attack and submit evidence. + +Under these assumptions, `StateTrusted` loses its meaning. As a +result, it should be removed from the API. We suggest that we replace +it with a flag "trusted" that can be used +- internally for efficiency reasons (to maintain + [LCD-INV-TRUSTED-AGREED.1] until a fork is detected) +- by light client based on the "one correct full node" assumption + + +---- + + + + diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md index f811bd5de..7001a39c9 100644 --- a/docs/spec/lightclient/detection/req-ibc-detection.md +++ b/docs/spec/lightclient/detection/req-ibc-detection.md @@ -362,18 +362,4 @@ We will need to define what we expect from these components - we write specs for these components. -# ICS-007 - -> Below we will discuss in more detail the necessary steps to address -[Issue 461](https://github.com/informalsystems/tendermint-rs/issues/461) -in particular w.r.t. 1. "proof of fork" for on-chain clients - may -require breaking changes to -[ICS07](https://github.com/cosmos/ics/tree/master/spec/ics-007-tendermint-client). - -- "Tendermint client state tracks the current validator set": is this - the validator set or the nextvalidator set of the block with tha - maximum height verified thus far? What is `validatorSet` used for? - - -