From f3033c551556b1c47fcc05e18c18ea80be3791bc Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 24 Sep 2020 09:53:50 +0200 Subject: [PATCH] spec: Light client attack detector (#164) * start with new detection and evidence spec * more definitions at top * sketch of functions * pre post draft * evidence proof * typo * evidence theory polished * some TODOs resolved * more TODOs * links * second to last revision before PR * links * I will read once more and then make a PR * removed peer handling definitions * secondary * ready to review * detector ready for review * Update rust-spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic * Update rust-spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic * Update rust-spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic * Update rust-spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic * Update rust-spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic * Update rust-spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic * Update rust-spec/lightclient/detection/detection.md * skip-trace * PossibleCommit explained * Update rust-spec/lightclient/detection/detection.md Co-authored-by: Zarko Milosevic * comments by Zarko * renamed and changed link in README Co-authored-by: Zarko Milosevic --- rust-spec/lightclient/README.md | 5 +- rust-spec/lightclient/detection/detection.md | 696 --------------- .../detection/detection_001_reviewed.md | 793 ++++++++++++++++++ 3 files changed, 796 insertions(+), 698 deletions(-) delete mode 100644 rust-spec/lightclient/detection/detection.md create mode 100644 rust-spec/lightclient/detection/detection_001_reviewed.md diff --git a/rust-spec/lightclient/README.md b/rust-spec/lightclient/README.md index a0e14e380..1958dc007 100644 --- a/rust-spec/lightclient/README.md +++ b/rust-spec/lightclient/README.md @@ -73,11 +73,12 @@ no bug is reported up to depth k. ![Experimental results](experiments.png) -## Fork Detection +## Attack Detection This is a work-in-progress draft. -The [English specification](detection/detection.md) defines blockchain forks and describes +The [English specification](detection/detection_001_reviewed.md) +defines blockchain forks and light client attacks, and describes the problem of a light client detecting them from communication with a network of full nodes, where at least one is correct. diff --git a/rust-spec/lightclient/detection/detection.md b/rust-spec/lightclient/detection/detection.md deleted file mode 100644 index 4faa0f4ca..000000000 --- a/rust-spec/lightclient/detection/detection.md +++ /dev/null @@ -1,696 +0,0 @@ -# Fork detector - -> ***This an unfinished draft. Comments are welcome!*** - -A detector (or detector for short) is a mechanism that expects as -input a header with some height *h*, connects to different Tendermint -full nodes, requests the header of height *h* from them, and then -cross-checks the headers and the input header. - -There are two foreseeable use cases: - -1) strengthen the light client: If a light client accepts a header -*hd* (after performing skipping or sequential verification), it can -use the detector to probe the system for conflicting headers and -increase the trust in *hd*. Instead of communicating with a single -full node, communicating with several full nodes shall increase the -likelihood to be aware of a fork (see [[accountability]] for -discussion about forks) in case there is one. - -2) to support fork accountability: In the case when more than 1/3 of -the voting power is held by faulty validators, faulty nodes may -generate two conflicting headers for the same height. The goal of the -detector is to learn about the conflicting headers by probing -different full nodes. Once a detector has two conflicting headers, -these headers are evidence of misbehavior. A natural extension is to -use the detector within a monitor process (on a full node) that calls -the detector on a sample (or all) headers (in parallel). (If the -sample is chosen at random, this adds a level of probabilistic -reasoning.) If conflicting headers are found, they are evidence that -can be used for punishing processes. - -In this document we will focus onn strengthening the light client, and -leave other uses of the detection mechanism (e.g., when run on a full -node) to the future. - -## Context of this document - -The light client verification specification [[verification]] is -designed for the Tendermint failure model (1/3 assumption) -[TMBC-FM-2THIRDS]. It is safe under this assumption, and live -if it can reliably (that is, no message loss, no duplication, and -eventually delivered) and timely communicate with a correct full node. If -this assumption is violated, the light client can be fooled to trust a -header that was not generated by Tendermint consensus. - -This specification, the fork detector, is a "second line of defense", -in case the 1/3 assumption is violated. Its goal is to detect fork (conflicting headers) and collect -evidence. However, it is impractical to probe all full nodes. At this -time we consider a simple scheme of maintaining an address book of -known full nodes from which a small subset (e.g., 4) are chosen -initially to communicate with. More involved book keeping with -probabilistic guarantees can be considered at later stages of the -project. - -The light client maintains a simple address book containing addresses -of full nodes that it can pick as primary and secondaries. To obtain -a new header, the light client first does [verification][verification] -with the primary, and then cross-checks the header with the -secondaries using this specification. - -### Tendermint Consensus and Forks - -#### **[TMBC-GENESIS.1]** - -Let *Genesis* be the agreed-upon initial block (file). - -#### **[TMBC-FUNC.1]** - -> **TODO** be more precise. +2/3 of b.NextV = c.Val signed c. For now -> the following will do: - -Let b and c be two light blocks -with *b.Header.Height + 1 = c.Header.Height*. We define **signs(b,c)** - iff `ValidAndVerified(b, c)` - -> **TODO** be more precise. +1/3 of b.NextV signed c. For now -> the following will do: - -Let *b* and *c* be two light blocks. We define **supports(b,c,t)** - iff `ValidAndVerified(b, c)` at time *t* - -> The following formalizes that *b* was properly generated by -> Tendermint; *b* can be traced back to genesis - -#### **[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. - -- *a(1) = Genesis* and -- *a(h) = b* and -- *signs( a(i) , a(i+1) )*. - -> The following formalizes that *c* is trusted based on *b* in -> skipping verification. Observe that we do not require here (yet) -> that *b* was properly generated. - -#### **[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 -- *a(h) = c* and -- *supports( a(i), a(i+1), t)*, for all i, *1 <= i < h*. - -> **TODO** In the above we might use a sequence of times t(i). Not sure. -> **TODO:** I believe the following definition -> corresponds to **Slashable fork** in -> [forks][tendermintfork]. Please confirm! -> Observe that sign-skip-match is even defined if there is a fork on -> the chain. - -#### **[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 - -- *b.Header.Height = c.Header.Height* and -- *skip-root(a,b,t)* -- *skip-root(a,c,t)* - -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*. -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 -> *c*. -> **TODO:** I think the following definition is -> the intuition behind **main chain forks** -> in the document on [forks][tendermintfork]. However, main chain -> forks were defined more operational "forks that are observed by -> full nodes as part of normal Tendermint consensus protocol". Please -> confirm! - -#### **[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 -- *sequ-rooted(b)* and -- *sequ-rooted(c)* - -implies *b = c*. - -If there exists two light blocks b and c, with *sign-unique(b,c) = -false* then we have a *fork on the chain*. - -> The following captures what I believe is called a light client fork -> in our discussions. There is no fork on the chain up to the height -> of block b. However, c is of that height, is different, and passes skipping -> verification -> Observe that a light client fork is a special case of a slashable -> 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 -- *sequ-rooted(b)* and -- *b* is "unique", that is, for all *d*, *sequ-rooted(d)* and - *d.Header.Height=b.Header.Height* implies *d = b* - -> Finally, let's also define bogus blocks that have no support. -> Observe that bogus is even defined if there is a fork on the chain. -> Also, for the definition it would be sufficient to restrict *a* to -> *a.height < b.height* (which is implied by the definitions which -> unfold until *supports()*. - -#### **[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* - -> Relation to [fork accountability][accountability]: F1, F2, and F3 -> (equivocation, amnesia, back to the past) can lead to a fork on the -> chain and to a light client fork. -> F4 and F5 (phantom validators, lunatic) cannot lead to a fork on the -> chain but to a light client -> fork if *t+1 < f < 2t+1*. -> F4 and F5 can also lead to bogus blocks - -### Informal Problem statement - -> We put tags to informal problem statements as there is no sequential -> specification. - -The following requirements are operational in that they describe how -things should be done, rather than what should be done. However, they -do not constitute temporal logic verification conditions. For those, -see [LCD-DIST-*] below. - -#### **[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.1]** - -Whenever the light client verifier performs `VerifyToTarget` with the -primary and returns with -`(lightStore, ResultSuccess)`, the - detector should query the secondaries by calling `FetchLightBlock` for height - *LightStore.LatestVerified().Height* remotely. -Then, -the detector returns the set of all headers *h'* downloaded from -secondaries that satisfy - -- *h'* is different from *LightStore.LatestVerified()* -- *h'* is a (light) fork. - -#### **[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 -node. (A full node that has not been primary or secondary -before). Detectable misbehavior can be - -- a timeout -- The case where *h'* is different -from *LightStore.LatestVerified()* but *h'* is not a fork, that is, if -*h'* is bogus. In other words, the -secondary cannot provide a sequence of light blocks that constitutes -proof of *h'*. - -## Assumptions/Incentives/Environment - -It is not in the interest of faulty full nodes to talk to the -detector as long as the detector is connected to at least one -correct full node. This would only increase the likelihood of -misbehavior being detected. Also we cannot punish them easily -(cheaply). The absence of a response need not be the fault of the full -node. - -Correct full nodes have the incentive to respond, because the -detector may help them to understand whether their header is a good -one. We can thus base liveness arguments of the detector on -the assumptions that correct full nodes reliably talk to the -detector. - -### Assumptions - -#### **[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.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.1]** - -Communication between the detector and a correct full node is -reliable and bounded in time. Reliable communication means that -messages are not lost, not duplicated, and eventually delivered. There -is a (known) end-to-end delay *Delta*, such that if a message is sent -at time *t* then it is received and processed by time *t + Delta*. -This implies that we need a timeout of at least *2 Delta* for remote -procedure calls to ensure that the response of a correct peer arrives -before the timeout expires. - -## (Distributed) Problem statement - -> As the fork detector from the beginning is there to reduce the -> impact of faulty nodes, and faulty nodes imply that there is a -> distributed system, there is no sequential specification. - -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 *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* ([TMBC-SIGN-FORK.1]), -then the detector should return the empty set. - -> 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-verified*, and -there are two correct full nodes *i* and *j* that are - -- on different branches, and -- *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. - -> 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*, -> 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'*, -> and if *h'* can be verified based on common root of trust, then -> evidence should be generated; -> By verifying we mean calling `VerifyToTarget` from the -> [[verification]] specification. - -## Definitions - -- A fixed set of full nodes is provided in the configuration upon - initialization. Initially this set is partitioned into - - one full node that is the *primary* (singleton set), - - a set *Secondaries* (of fixed size, e.g., 3), - - a set *FullNodes*. -- A set *FaultyNodes* of nodes that the light client suspects of being faulty; it is initially empty - -- *Lightstore* as defined in the [verification specification][verification]. - -#### **[LCD-INV-NODES.1]:** - -The detector shall maintain the following invariants: - -- *FullNodes \intersect Secondaries = {}* -- *FullNodes \intersect FaultyNodes = {}* -- *Secondaries \intersect FaultyNodes = {}* - -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]:** - -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 - -### Data Structures - -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 [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]** - -```go -type LightNodeProofOfFork struct { - TrustedBlock LightBlock - PrimaryTrace []LightBlock - SecondaryTrace []LightBlock -} -``` - - - - - - - - - -#### **[LCV-DATA-POFSTORE.1]** - -Proofs of Forks are stored in a structure which stores all proofs -generated during detection. - -```go -type PoFStore struct { - ... -} -``` - -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 -``` - -- Expected postcondition - - returns a lightstore that contains all lightblocks *b* from *ls* - that satisfy: *from < b.Header.Height <= to* - ----- - -### Inter Process Communication - -```go -func FetchLightBlock(peer PeerID, height Height) LightBlock -``` - -See the [verification specification][verification] for details. - -#### **[LCD-FUNC-SUBMIT.1]:** - -```go -func SubmitProofOfFork(pof LightNodeProofOfFork) Result -``` - -**TODO:** finalize what this should do, and what detail of - specification we need. - -- Implementation remark -- Expected precondition - - none -- Expected postcondition - - 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. 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 - -### 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 - - download block and compare to previously downloaded one. -- Expected precondition -- Expected postcondition -- Error condition - -#### **[LCD-FUNC-REPLACE-PRIMARY.1]:** - -```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* - - maintain [LCD-INV-TRUSTED-AGREED.1], that is, - - call `CrossCheck(nsec,lightStore.LatestTrusted()`. - If it matches we are OK, otherwise - - 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) - -- Expected precondition - - *FullNodes* is nonempty - -- Expected postcondition - - *primary* is moved to *FaultyNodes* - - 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 - -#### **[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 - - **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 -- Expected postcondition - - addr is moved from *Secondaries* to *FaultyNodes* - - an address *a* is moved from *FullNodes* to *Secondaries* -- Error condition - - if precondition is violated - -### From the verifier - -```go -func VerifyToTarget(primary PeerID, lightStore LightStore, - targetHeight Height) (LightStore, Result) -``` - -See the [verification specification][verification] for details. - -## Protocol - -### Shared data of the light client - -- a pool of full nodes *FullNodes* that have not been contacted before -- peer set called *Secondaries* -- primary -- lightStore - -### Outline - -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. - -- **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. - -### Fork Detector - -#### **[LCD-FUNC-DETECTOR.1]:** - -```go -func ForkDetector(ls LightStore, PoFs PoFStore) -{ - testedLB := LightStore.LatestVerified() - for i, secondary range Secondaries { - if OK = CrossCheck(secondary, testedLB) { - // header matches. we do nothing. - } - else { - // [LCD-REQ-REP] - // header does not match. there is a situation. - // we try to verify sh by querying s - // we set up an auxiliary lightstore with the highest - // trusted lightblock and the lightblock we want to verify - auxLS.Init - auxLS.Update(LightStore.LatestTrusted(), StateVerified); - auxLS.Update(sh,StateUnverified); - 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. - // If return code was EXPIRED it might be too late - // to punish, we still report it. - pof = new LightNodeProofOfFork; - 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 { - // secondary might be faulty or unreachable - // it might fail to provide a trace that supports sh - // or time out - Replace_Secondary(secondary) - } - } - } - 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** submit proof of fork -- Error condition - - fails if precondition is violated - - fails if [LCV-INV-TP] is violated (no trusted header within - trusting period - ----- - -## Correctness arguments - -#### Argument for [LCD-DIST-INV] - -**TODO** - -#### Argument for [LCD-DIST-LIFE-FORK] - -**TODO** - -# References - -> links to other specifications/ADRs this document refers to - -[[verification]] The specification of the light client verification. - -[[tendermintfork]] Tendermint fork detection and accountability - -[[accountability]] Fork accountability - -[TMBC-FM-2THIRDS-linkVDD]: https://github.com/informalsystems/VDD/tree/master/blockchain/blockchain.md#**[TMBC-FM-2THIRDS-link]**: - -[TMBC-FM-2THIRDS-link]: https://github.com/tendermint/spec/blob/master/spec/consensus/light-client/verification.md - -[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md - -[blockchain]: https://github.com/informalsystems/VDD/tree/master/blockchain/blockchain.md - -[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md - -[verificationVDD]: https://github.com/informalsystems/VDD/blob/master/lightclient/failuredetector.md - -[verification]: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md - -[accountability]: https://github.com/tendermint/spec/blob/master/spec/consensus/light-client/accountability.md - -[tendermintfork]: https://docs.google.com/document/d/1xjyp5JOPt7QfHem1AFEaowBH2Plk0IHACWtYFXFvO7E/edit#heading=h.th2369ptc2ve diff --git a/rust-spec/lightclient/detection/detection_001_reviewed.md b/rust-spec/lightclient/detection/detection_001_reviewed.md new file mode 100644 index 000000000..379a05313 --- /dev/null +++ b/rust-spec/lightclient/detection/detection_001_reviewed.md @@ -0,0 +1,793 @@ +# ***This an unfinished draft. Comments are welcome!*** + +**TODO:** We will need to do small adaptations to the verification +spec to reflect the semantics in the LightStore (verified, trusted, +untrusted, etc. not needed anymore). In more detail: + +- The state of the Lightstore needs to go. Functions like `LatestVerified` can +keep the name but will ignore state as it will not exist anymore. + +- verification spec should be adapted to the second parameter of +`VerifyToTarget` +being a lightblock; new version number of function tag; + +- 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. + +- We need to introduce a new version number for the new +specification. So we should decide how + to handle that. + +# Light Client Attack Detector + +In this specification, we strengthen the light client to be resistant +against so-called light client attacks. In a light client attack, all +the correct Tendermint full nodes agree on the sequence of generated +blocks (no fork), but a set of faulty full nodes attack a light client +by generating (signing) a block that deviates from the block of the +same height on the blockchain. In order to do so, some of these faulty +full nodes must have been validators before and violate +[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link), as otherwise, if +[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link) would hold, +[verification](verification) would satisfy +[[LCV-SEQ-SAFE.1]](LCV-SEQ-SAFE-link). + +An attack detector (or detector for short) is a mechanism that is used +by the light client [supervisor](supervisor) after +[verification](verification) of a new light block +with the primary, to cross-check the newly learned light block with +other peers (secondaries). It expects as input a light block with some +height *root* (that serves as a root of trust), and a verification +trace (a sequence of lightblocks) that the primary provided. + +In case the detector observes a light client attack, it computes +evidence data that can be used by Tendermint full nodes to isolate a +set of faulty full nodes that are still within the unbonding period +(more than 1/3 of the voting power of the validator set at some block of the chain), +and report them via ABCI to the application of a Tendermint blockchain +in order to punish faulty nodes. + +## Context of this document + +The light client [verification](verification) specification is +designed for the Tendermint failure model (1/3 assumption) +[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link). It is safe under this +assumption, and live if it can reliably (that is, no message loss, no +duplication, and eventually delivered) and timely communicate with a +correct full node. If [[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link) assumption is violated, the light client +can be fooled to trust a light block that was not generated by +Tendermint consensus. + +This specification, the attack detector, is a "second line of +defense", in case the 1/3 assumption is violated. Its goal is to +detect a light client attack (conflicting light blocks) and collect +evidence. However, it is impractical to probe all full nodes. At this +time we consider a simple scheme of maintaining an address book of +known full nodes from which a small subset (e.g., 4) are chosen +initially to communicate with. More involved book keeping with +probabilistic guarantees can be considered at later stages of the +project. + +The light client maintains a simple address book containing addresses +of full nodes that it can pick as primary and secondaries. To obtain +a new light block, the light client first does +[verification](verification) with the primary, and then cross-checks +the light block (and the trace of light blocks that led to it) with +the secondaries using this specification. + +## Tendermint Consensus and Light Client Attacks + +In this section we will give some mathematical definitions of what we +mean by light client attacks (that are considered in this +specification) and how they differ from main-chain forks. To this end +we start by defining some properties of the sequence of blocks that is +decided upon by Tendermint consensus in normal operation (if the +Tendermint failure model holds +[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link)), +and then define different +deviations that correspond to attack scenarios. + +#### **[TMBC-GENESIS.1]** + +Let *Genesis* be the agreed-upon initial block (file). + +#### **[TMBC-FUNC-SIGN.1]** + +Let *b* and *c* be two light blocks with *b.Header.Height + 1 = +c.Header.Height*. We define the predicate **signs(b,c)** to hold +iff *c.Header.LastCommit* is in *PossibleCommit(b)*. +[[TMBC-SOUND-DISTR-POSS-COMMIT.1]](TMBC-SOUND-DISTR-POSS-COMMIT-link). + +> The above encodes sequential verification, that is, intuitively, +> b.Header.NextValidators = c.Header.Validators and 2/3 of +> these Validators signed c? + +#### **[TMBC-FUNC-SUPPORT.1]** + +Let *b* and *c* be two light blocks. We define the predicate +**supports(b,c,t)** to hold iff + +- *t - trustingPeriod < b.Header.Time < t* +- the voting power in *b.NextValidators* of nodes in *c.Commit* + is more than 1/3 of *TotalVotingPower(b.Header.NextValidators)* + +> That is, if the [Tendermint failure model](TMBC-FM-2THIRDS-link) +> holds, then *c* has been signed by at least one correct full node, cf. +> [[TMBC-VAL-CONTAINS-CORR.1]](TMBC-VAL-CONTAINS-CORR-link). +> The following formalizes that *b* was properly generated by +> Tendermint; *b* can be traced back to genesis + +#### **[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. + +- *a(1) = Genesis* and +- *a(h) = b* and +- *signs( a(i) , a(i+1) )*. + +> The following formalizes that *c* is trusted based on *b* in +> skipping verification. Observe that we do not require here (yet) +> that *b* was properly generated. + +#### **[TMBC-SKIP-TRACE.1]** + +Let *b* and *c* be light blocks. We define *skip-trace(b,c,t)* if at +time t there exists an *h* and a sequence *a(1)*, ... *a(h)* s.t. + +- *a(1) = b* and +- *a(h) = c* and +- *supports( a(i), a(i+1), t)*, for all i, *1 <= i < h*. + +We call such a sequence *a(1)*, ... *a(h)* a **verification trace**. + +> The following formalizes that two light blocks of the same height +> should agree on the content of the header. Observe that *b* and *c* +> may disagree on the Commit. This is a special case if the canonical +> commit has not been decided on, that is, if b.Header.Height is the +> maximum height of all blocks decided upon by Tendermint at this +> moment. + +#### **[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 the following implication +evaluates to true: + +- *sequ-rooted(a)* and +- *b.Header.Height = c.Header.Height* and +- *skip-trace(a,b,t)* +- *skip-trace(a,c,t)* + +implies *b.Header = c.Header*. + +> Observe that *sign-skip-match* is defined via an implication. If it +> evaluates to false this means that the left-hand-side of the +> implication evaluates to true, and the right-hand-side evaluates to +> false. In particular, there are two **different** headers *b* and +> *c* that both can be verified from a common block *a* from the +> chain. Thus, the following describes an attack. + +#### **[TMBC-ATTACK.1]** + +If there exists three light blocks a, b, and c, with +*sign-skip-match(a,b,c,t) = false* then we have an *attack*. We say +we have **an attack at height** *b.Header.Height* and write +*attack(a,b,c,t)*. + +> The lightblock *a* need not be unique, that is, there may be +> several blocks that satisfy the above requirement for the same +> blocks *b* and *c*. + +[[TMBC-ATTACK.1]](#TMBC-ATTACK1) is a formalization of the violation +of the agreement property based on the result of consensus, that is, +the generated blocks. + +**Remark.** +Violation of agreement is only possible if more than 1/3 of the validators (or +next validators) of some previous block deviated from the protocol. The +upcoming "accountability" specification will describe how to compute +a set of at least 1/3 faulty nodes from two conflicting blocks. [] + +There are different ways to characterize forks +and attack scenarios. This specification uses the "node-based +characterization of attacks" which focuses on what kinds of nodes are +affected (light nodes vs. full nodes). For future reference and +discussion we also provide a +"block-based characterization of attacks" below. + +### Node-based characterization of attacks + +#### **[TMBC-MC-FORK.1]** + +We say there is a (main chain) fork at time *t* if + +- there are two correct full nodes *i* and *j* and +- *i* is different from *j* and +- *i* has decided on *b* and +- *j* has decided on *c* and +- there exist *a* such that *attack(a,b,c,t)*. + +#### **[TMBC-LC-ATTACK.1]** + +We say there is a light client attack at time *t*, if + +- there is **no** (main chain) fork [[TMBC-MC-FORK.1]](#TMBC-MC-FORK1), and +- there exist nodes that have computed light blocks *b* and *c* and +- there exist *a* such that *attack(a,b,c,t)*. + +We say the attack is at height *a.Header.Height*. + +> In this specification we consider detection of light client +> attacks. Intuitively, the case we consider is that +> light block *b* is the one from the +> blockchain, and some attacker has computed *c* and tries to wrongly +> convince +> the light client that *c* is the block from the chain. + +#### **[TMBC-LC-ATTACK-EVIDENCE.1]** + +We consider the following case of a light client attack +[[TMBC-LC-ATTACK.1]](#TMBC-LC-ATTACK1): + +- *attack(a,b,c,t)* +- there is a peer p1 that has a sequence *chain* of blocks from *a* to *b* +- *skip-trace(a,c,t)*: by [[TMBC-SKIP-TRACE.1]](#TMBC-SKIP-TRACE1) there is a + verification trace *v* of the form *a = v(1)*, ... *v(h) = c* + +Evidence for p1 (that proves an attack) consists for index i +of v(i) and v(i+1) such that + +- E1(i). v(i) is equal to the block of *chain* at height v(i).Height, and +- E2(i). v(i+1) that is different from the block of *chain* at + height v(i+1).height + +> Observe p1 can +> +> - check that v(i+1) differs from its block at that height, and +> - verify v(i+1) in one step from v(i) as v is a verification trace. + +**Proposition.** In the case of attack, evidence exists. +*Proof.* First observe that + +- (A). (NOT E2(i)) implies E1(i+1) + +Now by contradiction assume there is no evidence. Thus + +- for all i, we have NOT E1(i) or NOT E2(i) +- for i = 1 we have E1(1) and thus NOT E2(1) + thus by induction on i, by (A) we have for all i that **E1(i)** +- from attack we have E2(h-1), and as there is no evidence for + i = h - 1 we get **NOT E1(h-1)**. Contradiction. +QED. + +#### **[TMBC-LC-EVIDENCE-DATA.1]** + +To prove the attack to p1, because of Point E1, it is sufficient to +submit + +- v(i).Height (rather than v(i)). +- v(i+1) + +This information is *evidence for height v(i).Height*. + +### Block-based characterization of attacks + +In this section we provide a different characterization of attacks. It +is not defined on the nodes that are affected but purely on the +content of the blocks. In that sense these definitions are less +operational. + +> They might be relevant for a closer analysis of fork scenarios on the +> chain, which is out of the scope of this specification. + +#### **[TMBC-SIGN-UNIQUE.1]** + +Let *b* and *c* be light blocks, we define the predicate +*sign-unique(b,c)* to evaluate to true iff the following implication +evaluates to true: + +- *b.Header.Height = c.Header.Height* and +- *sequ-rooted(b)* and +- *sequ-rooted(c)* + +implies *b = c*. + +#### **[TMBC-BLOCKS-MCFORK.1]** + +If there exists two light blocks b and c, with *sign-unique(b,c) = +false* then we have a *fork*. + +> The difference of the above definition to +> [[TMBC-MC-FORK.1]](#TMBC-MC-FORK1) is subtle. The latter requires a +> full node being affected by a bad block while +> [[TMBC-BLOCKS-MCFORK.1]](#TMBC-BLOCKS-MCFORK1) just requires that a +> bad block exists, possibly in memory of an attacker. +> The following captures a light client fork. There is no fork up to +> the height of block b. However, c is of that height, is different, +> and passes skipping verification. It is a stricter property than +> [[TMBC-LC-ATTACK.1]](#TMBC-LC-ATTACK1), as +> [[TMBC-LC-ATTACK.1]](#TMBC-LC-ATTACK1) requires that no correct full +> node is affected. + +#### **[TMBC-BLOCKS-LCFORK.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 +- *sequ-rooted(b)* and +- *b* is "unique", that is, for all *d*, *sequ-rooted(d)* and + *d.Header.Height = b.Header.Height* implies *d = b* + +> Finally, let us also define bogus blocks that have no support. +> Observe that bogus is even defined if there is a fork. +> Also, for the definition it would be sufficient to restrict *a* to +> *a.height < b.height* (which is implied by the definitions which +> unfold until *supports()*). + +#### **[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-trace(a,b,t) = false* + +### Informal Problem statement + +There is no sequential specification: the detector only makes sense +in a distributed systems where some nodes misbehave. + +We work under the assumption that full nodes and validators are +responsible for detecting attacks on the main chain, and the evidence +reactor takes care of broadcasting evidence to communicate +misbehaving nodes via ABCI to the application, and halt the chain in +case of a fork. The point of this specification is to shield a light +clients against attacks that cannot be detected by full nodes, and +are fully addressed at light clients (and consequently IBC relayers, +which use the light client protocols to observe the state of a +blockchain). In order to provide full nodes the incentive to follow +the protocols when communicating with the light client, this +specification also considers the generation of evidence that will +also be processed by the Tendermint blockchain. + +#### **[LCD-IP-MODEL.1]** + +The detector is designed under the assumption that + +- [[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link) may be violated +- there is no fork on the main chain. + +> As a result some faulty full nodes may launch an attack on a light +> client. + +The following requirements are operational in that they describe how +things should be done, rather than what should be done. However, they +do not constitute temporal logic verification conditions. For those, +see [LCD-DIST-*] below. + +The detector is called in the [supervisor](supervisor) as follows + +```go +Evidences := AttackDetector(root_of_trust, verifiedLS);` +``` + +where + +- `root-of-trust` is a light block that is trusted (that is, +except upon initialization, the primary and the secondaries +agreed on in the past), and +- `verifiedLS` is a lightstore that contains a verification trace that + starts from a lightblock that can be verified with the + `root-of-trust` in one step and ends with a lightblock of the height + requested by the user +- `Evidences` is a list of evidences for misbehavior + +#### **[LCD-IP-STATEMENT.1]** + +Whenever AttackDetector is called, the detector should for each +secondary try to replay the verification trace `verifiedLS` with the +secondary + +- in case replaying leads to detection of a light client attack + (one of the lightblocks differ from the one in verifiedLS with + the same height), we should return evidence +- if the secondary cannot provide a verification trace, we have no + proof for an attack. Block *b* may be bogus. In this case the + secondary is faulty and it should be replaced. + +## Assumptions/Incentives/Environment + +It is not in the interest of faulty full nodes to talk to the +detector as long as the detector is connected to at least one +correct full node. This would only increase the likelihood of +misbehavior being detected. Also we cannot punish them easily +(cheaply). The absence of a response need not be the fault of the full +node. + +Correct full nodes have the incentive to respond, because the +detector may help them to understand whether their header is a good +one. We can thus base liveness arguments of the detector on +the assumptions that correct full nodes reliably talk to the +detector. + +### Assumptions + +#### **[LCD-A-CorrFull.1]** + +At all times there is at least one correct full +node among the primary and the secondaries. + +> For this version of the detection we take this assumption. It +> allows us to establish the invariant that the lightblock +> `root-of-trust` is always the one from the blockchain, and we can +> use it as starting point for the evidence computation. Moreover, it +> allows us to establish the invariant at the supervisor that any +> lightblock in the (top-level) lightstore is from the blockchain. +> In the future we might design a lightclient based on the assumption +> that at least in regular intervals the lightclient is connected to a +> correct full node. This will require the detector to reconsider +> `root-of-trust`, and remove lightblocks from the top-level +> lightstore. + +#### **[LCD-A-RelComm.1]** + +Communication between the detector and a correct full node is +reliable and bounded in time. Reliable communication means that +messages are not lost, not duplicated, and eventually delivered. There +is a (known) end-to-end delay *Delta*, such that if a message is sent +at time *t* then it is received and processed by time *t + Delta*. +This implies that we need a timeout of at least *2 Delta* for remote +procedure calls to ensure that the response of a correct peer arrives +before the timeout expires. + +## Definitions + +### Evidence + +Following the definition of +[[TMBC-LC-ATTACK-EVIDENCE.1]](#TMBC-LC-ATTACK-EVIDENCE1), by evidence +we refer to a variable of the following type + +#### **[LC-DATA-EVIDENCE.1]** + +```go +type LightClientAttackEvidence struct { + ConflictingBlock LightBlock + CommonHeight int64 +} +``` + +As the above data is computed for a specific peer, the following +data structure wraps the evidence and adds the peerID. + +#### **[LC-DATA-EVIDENCE-INT.1]** + +```go +type InternalEvidence struct { + Evidence LightClientAttackEvidence + Peer PeerID +} +``` + +#### **[LC-SUMBIT-EVIDENCE.1]** + +```go +func submitEvidence(Evidences []InternalEvidence) +``` + +- Expected postcondition + - for each `ev` in `Evidences`: submit `ev.Evidence` to `ev.Peer` + +--- + +### LightStore + +Lightblocks and LightStores are defined in the verification +specification [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See +the [verification specification][verification] for details. + +## (Distributed) Problem statement + +> As the attack detector is there to reduce the impact of faulty +> nodes, and faulty nodes imply that there is a distributed system, +> there is no sequential specification to which this distributed +> problem statement may refer to. + +The detector gets as input a trusted lightblock called *root* and an +auxiliary lightstore called *primary_trace* with lightblocks that have +been verified before, and that were provided by the primary. + +#### **[LCD-DIST-INV-ATTACK.1]** + +If the detector returns evidence for height *h* +[[TMBC-LC-EVIDENCE-DATA.1]](#TMBC-LC-EVIDENCE-DATA1), then there is an +attack at height *h*. [[TMBC-LC-ATTACK.1]](#TMBC-LC-ATTACK1) + +#### **[LCD-DIST-INV-STORE.1]** + +If the detector does not return evidence, then *primary_trace* +contains only blocks from the blockchain. + +#### **[LCD-DIST-LIVE.1]** + +The detector eventually terminates. + +#### **[LCD-DIST-TERM-NORMAL.1]** + +If + +- the *primary_trace* contains only blocks from the blockchain, and +- there is no attack, and +- *Secondaries* is always non-empty, and +- the age of *root* is always less than the trusting period, + +then the detector does not return evidence. + +#### **[LCD-DIST-TERM-ATTACK.1]** + +If + +- there is an attack, and +- a secondary reports a block that conflicts + with one of the blocks in *primary_trace*, and +- *Secondaries* is always non-empty, and +- the age of *root* is always less than the trusting period, + +then the detector returns evidence. + +> Observe that above we require that "a secondary reports a block that +> conflicts". If there is an attack, but no secondary tries to launch +> it against the detector (or the message from the secondary is lost +> by the network), then there is nothing to detect for us. + +#### **[LCD-DIST-SAFE-SECONDARY.1]** + +No correct secondary is ever replaced. + +#### **[LCD-DIST-SAFE-BOGUS.1]** + +If + +- a secondary reports a bogus lightblock, +- the age of *root* is always less than the trusting period, + +then the secondary is replaced before the detector terminates. + +> The above property is quite operational ("reports"), but it captures +> quite closely the requirement. As the +> detector only makes sense in a distributed setting, and does +> not have a sequential specification, less "pure" +> specification are acceptable. + +# Protocol + +## Functions and Data defined in other Specifications + +### From the supervisor + +```go +Replace_Secondary(addr Address, root-of-trust LightBlock) +``` + +### From the verifier + +```go +func VerifyToTarget(primary PeerID, root LightBlock, + targetHeight Height) (LightStore, Result) +``` + +> Note: the above differs from the current version in the second +> parameter. verification will be revised. + +Observe that `VerifyToTarget` does communication with the secondaries +via the function [FetchLightBlock](fetch). + +### Shared data of the light client + +- a pool of full nodes *FullNodes* that have not been contacted before +- peer set called *Secondaries* +- primary + +> Note that the lightStore is not needed to be shared. + +## Outline + +The problem laid out is solved by calling the function `AttackDetector` +with a lightstore that contains a light block that has just been +verified by the verifier. + +Then `AttackDetector` downloads headers from the secondaries. In case +a conflicting header is downloaded from a secondary, +`CreateEvidenceForPeer` which computes evidence in the case that +indeed an attack is confirmed. It could be that the secondary reports +a bogus block, which means that there need not be an attack, and the +secondary is replaced. + +## Details of the functions + +#### **[LCD-FUNC-DETECTOR.1]:** + +```go +func AttackDetector(root LightBlock, primary_trace []LightBlock) + ([]InternalEvidence) { + + Evidences := new []InternalEvidence; + + for each secondary in Secondaries { + // we replay the primary trace with the secondary, in + // order to generate evidence that we can submit to the + // secodary. We return the evidence + the trace the + // secondary told us that spans the evidence at its local store + + EvidenceForSecondary, newroot, secondary_trace, result := + CreateEvidenceForPeer(secondary, + root, + primary_trace); + if result == FaultyPeer { + Replace_Secondary(root); + } + else if result == FoundEvidence { + // the conflict is not bogus + Evidences.Add(EvidenceForSecondary); + // we replay the secondary trace with the primary, ... + EvidenceForPrimary, _, result := + CreateEvidenceForPeer(primary, + newroot, + secondary_trace); + if result == FoundEvidence { + Evidences.Add(EvidenceForPrimary); + } + // At this point we do not care about the other error + // codes. We already have generated evidence for an + // attack and need to stop the lightclient. It does not + // help to call replace_primary. Also we will use the + // same primary to check with other secondaries in + // later iterations of the loop + } + // In the case where the secondary reports NoEvidence + // we do nothing + } + return Evidences; +} +``` + +- Expected precondition + - root and primary trace are a verification trace +- Expected postcondition + - solves the problem statement (if attack found, then evidence is reported) +- Error condition + - `ErrorTrustExpired`: fails if root expires (outside trusting + period) [[LCV-INV-TP.1]](LCV-INV-TP1-link) + - `ErrorNoPeers`: if no peers are left to replace secondaries, and + no evidence was found before that happened + +--- + +```go +func CreateEvidenceForPeer(peer PeerID, root LightBlock, trace LightStore) + (Evidence, LightBlock, LightStore, result) { + + common := root; + + for i in 1 .. len(trace) { + auxLS, result := VerifyToTarget(peer, common, trace[i].Header.Height) + + if result != ResultSuccess { + // something went wrong; peer did not provide a verifyable block + return (nil, nil, nil, FaultyPeer) + } + else { + if auxLS.LatestVerified().Header != trace[i].Header { + // the header reported by the peer differs from the + // reference header in trace but both could be + // verified from common in one step. + // we can create evidence for submission to the secondary + ev := new InternalEvidence; + ev.Evidence.ConflictingBlock := trace[i]; + ev.Evidence.CommonHeight := common.Height; + ev.Peer := peer + return (ev, common, auxLS, FoundEvidence) + } + else { + // the peer agrees with the trace, we move common forward + // we could delete auxLS as it will be overwritten in +<<<<<<< HEAD:rust-spec/lightclient/detection/detection_001_reviewed.md + // the next iterationt + common := trace[i].Header +======= + // the next iteration + common := trace[i] +>>>>>>> bc3d1aff5ba358afb68f1698e5834995662ba74c:rust-spec/lightclient/detection/detection.md + } + } + } + return (nil, nil, nil, NoEvidence) +} +``` + +- Expected precondition + - root and trace are a verification trace +- Expected postcondition + - finds evidence where trace and peer diverge +- Error condition + - `ErrorTrustExpired`: fails if root expires (outside trusting + period) [[LCV-INV-TP.1]](LCV-INV-TP1-link) + - If `VerifyToTarget` returns error but root is not expired then return + `FaultyPeer` + +--- + +## Correctness arguments + +#### Argument for [[LCD-DIST-INV-ATTACK.1]](#LCD-DIST-INV-ATTACK1) + +Under the assumption that root and trace are a verification trace, +when in `CreateEvidenceForPeer` the detector the detector creates +evidence, then the lightclient has seen two different headers (one via +`trace` and one via `VerifyToTarget` for the same height that can both +be verified in one step. + +#### Argument for [[LCD-DIST-INV-STORE.1]](#LCD-DIST-INV-STORE1) + +We assume that there is at least one correct peer, and there is no +fork. As a result the correct peer has the correct sequence of +blocks. Since the primary_trace is checked block-by-block also against +each secondary, and at no point evidence was generated that means at +no point there were conflicting blocks. + +#### Argument for [[LCD-DIST-LIVE.1]](#LCD-DIST-LIVE1) + +At the latest when [[LCV-INV-TP.1]](LCV-INV-TP1-link) is violated, +`AttackDetector` terminates. + +#### Argument for [[LCD-DIST-TERM-NORMAL.1]](#LCD-DIST-TERM-NORMAL1) + +As there are finitely many peers, eventually the main loop +terminates. As there is no attack no evidence can be generated. + +#### Argument for [[LCD-DIST-TERM-ATTACK.1]](#LCD-DIST-TERM-ATTACK1) + +Argument similar to [[LCD-DIST-TERM-NORMAL.1]](#LCD-DIST-TERM-NORMAL1) + +#### Argument for [[LCD-DIST-SAFE-SECONDARY.1]](#LCD-DIST-SAFE-SECONDARY1) + +Secondaries are only replaced if they time-out or if they report bogus +blocks. The former is ruled out by the timing assumption, the latter +by correct peers only reporting blocks from the chain. + +#### Argument for [[LCD-DIST-SAFE-BOGUS.1]](#LCD-DIST-SAFE-BOGUS1) + +Once a bogus block is recognized as such the secondary is removed. + +# References + +> links to other specifications/ADRs this document refers to + +[[verification]] The specification of the light client verification. + +[[supervisor]] The specification of the light client supervisor. + +[verification]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md + +[supervisor]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/supervisor/supervisor.md + +[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md + +[TMBC-FM-2THIRDS-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#tmbc-fm-2thirds1 + +[TMBC-SOUND-DISTR-POSS-COMMIT-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#tmbc-sound-distr-poss-commit1 + +[LCV-SEQ-SAFE-link]:https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#lcv-seq-safe1 + +[TMBC-VAL-CONTAINS-CORR-link]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#tmbc-val-contains-corr1 + +[fetch]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#lcv-func-fetch1 + +[LCV-INV-TP1-link]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#lcv-inv-tp1