From 138dc0f036cf6ee4daa0f86bf29d5dc4c41d9a1d Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 9 Sep 2020 16:32:27 +0200 Subject: [PATCH 01/15] move from tendermint-rs but needs discussion --- .../lightclient/supervisor/supervisor.md | 646 ++++++++++++++++++ 1 file changed, 646 insertions(+) create mode 100644 rust-spec/lightclient/supervisor/supervisor.md diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md new file mode 100644 index 00000000..23c12718 --- /dev/null +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -0,0 +1,646 @@ +# Draft of Light Client Supervisor for discussion + +## TODOs: + +- move part I of verification here (or copy) + +- incorporate the structure of Stevan's Rust supervisor design + - new versions of `verifytotarget` and `backwards` that take as + input a single lightblock and return a fully verified lightstore + - update tags to ".2" + - lightstore.update: remove Unverified upon leaving verifyTotarget + +check that all is addressed: + +- https://github.com/informalsystems/tendermint-rs/issues/499 +- https://github.com/informalsystems/tendermint-rs/pull/509 +- https://github.com/tendermint/spec/issues/131 +- https://github.com/informalsystems/tendermint-rs/issues/461 + + +- links to verification and detection specs + + + +# Light Client Sequential Supervisor + +The light client implements a read operation of a +[header][TMBC-HEADER-link] from the [blockchain][TMBC-SEQ-link], by +communicating with full nodes, a so-called primary and several +so-called witnesses. As some full nodes may be faulty, this +functionality must be implemented in a fault-tolerant way. + +In the Tendermint blockchain, the validator set may change with every +new block. The staking and unbonding mechanism induces a [security +model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the +[header][TMBC-HEADER-link], +more than two-thirds of the next validators of a new block are correct +for the duration of *TrustedPeriod*. + +[Light Client Verification](TODO) implements the fault-tolerant read +operation designed for this security model. That is, it is safe if the +model assumptions are satisfied and makes progress if it communicates +to a correct primary. + +However, if the [security model][TMBC-FM-2THIRDS-link] is violated, +faulty peers (that have been validators at some point in the past) may +launch attacks on the Tendermint network, and on the light +client. These attacks as well as an axiomatization of blocks in +general are defined in [a document that contains the definitions that +are currently in detection.md](TODO). + +If there is a light client attack (but no +successful attack on the network), the safety of the verification step +may be violated (as we operate outside its basic assumption). +The light client also +contains a defense mechanism against light clients attacks, called detection. + +[Light Client Detection](TODO) implements a cross check of the result +of the verification step. If there is a light client attack, and the +light client is connected to a correct peer, the light client as a +whole is safe, that is, it will not operate on invalid +blocks. However, in this case it cannot successfully read, as +inconsistent blocks are in the system. However, in this case the +detection performs a distributed computation that results in so-called +evidence. Evidence can be used to prove +to a correct full node that there has been a +light client attack. + +[Light Client Evidence Accountability](TODO) is a protocol run on a +full node to check whether submitted evidence indeed proves the +existence of a light client attack. Further, from the evidence and its +own knowledge about the blockchain, the full node computes a set of +bonded full nodes (that at some point had more than one third of the +voting power) that participated in the attack that will be reported +via ABCI to the application. + +In this document we specify + +- Initialization of the Light Client +- The interaction of [verification](TODO) and [detection](TODO) + +The details of these two protocols are captured in their own +documents, as is the [accountability](TODO) protocol. + +> Another related line is IBC attack detection and submission at the +> relayer, as well as attack verification at the IBC handler. This +> will call for yet another spec. + + +# Status + +This document is work in progress. In order to develop the +specification step-by-step, +it assumes certain details of [verification](TODO) and +[detection](TODO) that are not specified in the respective current +versions yet. This inconsistencies will be addresses over several +upcoming PRs. + + +# Part I - Tendermint Blockchain + +TODO + +# Part II - Sequential Problem Definition + + +#### **[LC-SEQ-INIT-LIVE.1]**: +Upon initialization, the light client gets as input a header of the +blockchain, or the genesis file of the blockchain, and eventually +stores a header of the blockchain. + +> TODO: be more precise about heights in spec above + +#### **[LC-SEQ-LIVE.1]**: +The light client gets a sequence of heights as inputs. For each input +height *targetHeight*, it eventually stores the header of height +*targetHeight*. + +#### **[LC-SEQ-SAFE.1]**: + +The light client never stores a header which is not in the blockchain. + +# Part III - Light Client as Distributed System + +## Computational Model + +TODO: primary, witness (should be mainly discussed in detection +spec). + +TODO: always connected to a correct peer (should be mainly discussed +in detection spec). responds in time + +TODO: no main chain fork, that is, we assume all correct peers agree +on one blockchain. But TFM is violated, that is, there are bonded +validators that execute a light client attack +(details should be mainly discussed in +verification and detection specs). + +## Distributed Problem Statement + +### Two Kinds of Liveness + +In case of light client attacks, the sequential problem statement +cannot always be satisfied. The lightclient cannot decide which block +is from the chain and which is not. As a result, the light client just +creates evidence, submits it, and terminates. +For the liveness property, we thus add the +possibility that instead of adding a lightblock, we also might terminate +in case there is an attack. + + +#### **[LC-DIST-TERM.1]**: + +The light client either runs forever or it *terminates on attack*. + +### Design choices + +#### [LC-DIST-STORE.1]: +The light client has a local data structure called LightStore +that contains light blocks (that contain a header). + +TODO: put light store functions here (some are still in verification.md) + +#### **[LC-DIST-SAFE.1]**: +It is always the case that every header in *LightStore* was +generated by an instance of Tendermint consensus. + +#### **[LC-DIST-LIVE.1]**: + +Whenever the light client gets a new height *h* as input, +- and there is +no light client attack up to height *h*, then the lightclient +eventually puts the lightblock of height *h* in the lightstore and +wait for another input. +- otherwise, that is, if there +is a light client attack on height *h*, then the light client +must perform one of the following: + - it terminates on attack. + - it eventually puts the lightblock of height *h* in the lightstore and +wait for another input. + +### Solving the sequential specification + +TODO: as one of the peers is correct, the lightclient will always +download a correct lightblock (by the assumption that there is no fork +on the chain and all correct peers agree on the blokchain). -> safety + +For liveness there are three scenarios +1. no light client attack: all lightblocks match, and they are written + to the lightstore +2. there is an attack + a. one of the peers sends a lightblock involved in the attack to + the lightclient -> by assumption that there is a correct peer, it + will be detected, and we terminate on attack + b. the lightclient does not learn a faulty lightblock -> similar + to case 1. + +# Part IV - Light Client Supervisor Protocol + + +We provide a specification for a sequential Light Client Supervisor. +The local code for verification is presented by a sequential function +`Sequential-Supervisor` to highlight the control flow of this +functionality. Each lightblock is first verified with a primary, and then +cross-checked with secondaries, and if all goes well, the lightblock +is +added to the +lightstore. That is, no lightblock is ever removed from the +lightstore, and all lightblocks in the lightstore are trusted. + +> We note that if a different concurrency model is considered +> for an implementation, the semantics of the lightstore might change: +> In a concurrent implementation, we might do verification for some +> height *h*, add the +> lightblock to the lightstore, and start concurrent threads that +> - do verification for the next height *h' != h* +> - do cross-checking for height *h*. If we find an attack, we remove +> *h* from the lightstore. +> +> Thus, this concurrency model changes the semantics of the +> lightstore (not all lightblocks are trusted; they may be removed if +> we find a problem). Whether this is desirable, and whether the gain in +> performance is worth it, we keep for future versions/discussion of +> lightclient protocols. + + +## Definitions + +### Data Types + +The core data structure of the protocol is the LightBlock. + +#### **[LC-DATA-LIGHTBLOCK.1]**: +```go +type LightBlock struct { + Header Header + Commit Commit + Validators ValidatorSet + NextValidators ValidatorSet + Provider PeerID +} +``` + +#### **[LC-DATA-LIGHTSTORE.1]**: + +LightBlocks are stored in a structure which stores all LightBlock from +initialization or received from peers. + +```go +type LightStore struct { + ... +} + +``` + +The LightStore exposes the following functions to query stored LightBlocks. + +TODO: copy used new functions with tags. + + + +### Inputs + +The lightclient is initialized with LCInitData + +#### **[LC-DATA-INIT.1]**: +```go +type LCInitData struct { + lightBlock LightBlock + genesisDoc GenesisDoc +} +``` + +where only one of the components must be provided. `GenesisDoc` is +defined in the [Tendermint +Types](https://github.com/tendermint/tendermint/blob/master/types/genesis.go). + +#### **[LC-DATA-GENESIS.1]**: + +```go +type GenesisDoc struct { + GenesisTime time.Time `json:"genesis_time"` + ChainID string `json:"chain_id"` + InitialHeight int64 `json:"initial_height"` + ConsensusParams *tmproto.ConsensusParams `json:"consensus_params,omitempty"` + Validators []GenesisValidator `json:"validators,omitempty"` + AppHash tmbytes.HexBytes `json:"app_hash"` + AppState json.RawMessage `json:"app_state,omitempty"` +} +``` + +We use the following function +`makeblock` so that we create a lightblock from the genesis +file in order to do verification based on the data from the genesis +file using the same verification function we use in normal operation. + +#### **[LC-FUNC-MAKEBLOCK.1]**: +```go +func makeblock (genesisDoc GenesisDoc) (lightBlock LightBlock)) +``` +- Implementation remark + - none +- Expected precondition + - none +- Expected postcondition + - lightBlock.Header.Height = genesisDoc.InitialHeight + - lightBlock.Header.Time = genesisDoc.GenesisTime + - lightBlock.Header.LastBlockID = nil + - lightBlock.Header.LastCommit = nil + - lightBlock.Header.Validators = genesisDoc.Validators + - lightBlock.Header.NextValidators = genesisDoc.Validators + - lightBlock.Header.Data = nil + - lightBlock.Header.AppState = genesisDoc.AppState + - lightBlock.Header.LastResult = nil + - lightBlock.Commit = nil + - lightBlock.Validators = genesisDoc.Validators + - lightBlock.NextValidators = genesisDoc.Validators + - lightBlock.Provider = nil +- Error condition + - none +---- + + +### Configuration Parameters + +**TODO:** trusting period + +### Variables + +**TODO** + +- PeerList. + +It exposes the functions + +- primary() +- secondaries() +- replace_primary() +- replace secondary(peerID PeerID) + +### Assumptions + +init data is OK + +### Invariants + +#### **[LC-DATA-PEERLIST.1]:** +The peer list contains a primary and a secondary. + +> If the invariant is violated, the light client does not have enough +> peers to download headers from. As a result, the light client +> needs to terminate in case this invariant is violated. + + + +## Supervisor + +### Outline + +The supervisor implements the functionality of the lightclient. It is +initialized with a genesis file or with a lightblock the user +trusts. This initialization is subjective, that is, the security of +the lightclient is based on the validity of the input. If the genesis +file or the lightblock deviate from the actual ones on the blockchain, +the lightclient provides no guarantees. + +After initialization, the supervisor awaits an input, that is, the +height of the next lightblock that should be obtained. Then it +downloads, verifies, and cross-checks a lightblock, and if all tests +go through, the light block (and possibly other lightblocks) are added +to the lightstore, which is returned in an output event to the user. + +The following main loop does the interaction with the user (input, +output) and calls the following two functions: +- `InitLightClient`: it initializes the lightstore either with the + provided lightblock or with the lightblock that corresponds to the + first block generated by the blockchain (by the validators defined + by the genesis file) +- `VerifyAndDetect`: takes as input a lightstore and a height and + returns the updated lightstore. + +#### **[LC-FUNC-SUPERVISOR.1]:** + +```go +func Sequential-Supervisor (initdata LCInitData) (Error) { + + lightStore,result := InitLightClient(initData); + if result != OK { + return result; + } + + loop { + // get the next height + nextHeight := input(); + + lightStore,result := VerifyAndDetect(lightStore, nextHeight); + + if result == OK { + output(LightStore) + } + else { + return result + } + // QUESTION: is it OK to generate output event in normal case, + // and terminate with failure in the (light client) attack case? + } +} +``` +- Implementation remark + - infinite loop unless a light client attack is detected +- Expected precondition + - *LCInitData* contains a genesis file or a lightblock. +- Expected postcondition + - if a light client attack is detected: it stops and submits + evidence (in `InitLightClient` or `VerifyAndDetect`) + - otherwise: non. It runs forever. +- Invariant: *lightStore* contains trusted lightblocks only. +- Error condition + - if `InitLightClient` or `VerifyAndDetect` fails (if a attack is + detected, or if [LCV-INV-TP.1] is violated) +---- + + +### Details of the Functions + +#### Initialization + +The light client is based on subjective initialization. It has to +trust the initial data given to it by the user. It cannot do any +detection of attack. So either upon initialization we obtain a +lightblock and just initialize the lightstore with it. Or in case of a +genesis file, we download, verify, and cross-check the first block, to +initialize the lightstore with this first block. The reason is that +we want to maintain [LCV-INV-TP.1] from the beginning. + +> If the lightclient is initialized with a lightblock, one might think +> it may increase trust, when one cross-checks the initial light +> block. However, if a peer provides a conflicting +> lightblock, the question is to distinguish the case of a +> [bogus](TODO) block (upon which operation should proceed) from a +> [light client attack](TODO) (upon which operation should stop). In +> case of a bogus block, the lightclient might be forced to do +> backwards verification until the blocks are out of the trusting +> period, to make sure no previous validator set could have generated +> the bogus block, which effectively opens up a DoS attack on the lightclient +> without adding effective robustness. + +#### **[LC-FUNC-INIT.1]:** +```go +func InitLightClient (initData LCInitData) (LightStore, Error) { + + if LCInitData.LightBlock != nil { + // we trust the provided initial block. + newblock := LCInitData.LightBlock + } + else { + genesisBlock := makeblock(initData.genesisDoc); + + result := NoResult; + while result != ResultSuccess { + current = FetchLightBlock(PeerList.primary(), genesisBlock.Header.Height + 1) + // QUESTION: is the height with "+1" OK? + + if CANNOT_VERIFY = ValidAndVerify(genesisBlock, current) { + // TODO: remove "trusted.Commit is a commit for the header + // trusted.Header, i.e., it contains the correct hash of the + // header, and +2/3 of signatures" from validAndVerified precondition + peerList.replacePrimary(); + } + else { + result = ResultSuccess + } + } + + // cross-check + Evidences := AttackDetector(genesisBlock, current) + // TODO: wrap current in an auxiliary lightstore + if Evidences.Empty { + newBlock := current + } + else { + submitEvidence(Evidences); + return(nil, ErrorAttack); + } + } + + lightStore := new LightStore; + lightStore.Add(newBlock); //TODO: add Add to lightstore functions + return (lightStore, OK); +} + +``` +- Implementation remark + - none +- Expected precondition + - *LCInitData* contains either a genesis file of a lightblock + - if genesis it passes `ValidateAndComplete()` see [Tendermint](TODO) +- Expected postcondition + - *lightStore* initialized with trusted lightblock. It has either been + cross-checked (from genesis) or it has initial trust from the + user. +- Error condition + - if precondition is violated + - empty peerList +---- + + +#### Main verification and detection logic + + + +#### **[LC-FUNC-MAIN-VERIF-DETECT.1]:** + +```go +func VerifyAndDetect (lightStore LightStore, targetHeight Height) + (LightStore, Result) { + + b1, r1 = lightStore.Get(targetHeight) + if r1 = true { + // block already there + return (lightStore, ResultSuccess) + } + + // get the lightblock with maximum height smaller than targetHeight + // would typically be the heighest, if we always move forward + root_of_trust, r2 = lightStore.LatestPrevious(targetHeight); + if r2 = false { + // there is no lightblock from which we can do forward + // (skipping) verification. Thus we have to go backwards. + // No cross-check needed. We trust hashes. Therefore, we + // directly return the result + return Backwards(peerList.primary(), lightStore.lowest, targetHeight) + // TODO: in Backwards definition pointers need to be fixed to + // predecessor + // TODO: add tag pointer to Backwards + // TODO: define lightStore.lowest + } + else { + // Forward verification + detection + result := NoResult; + while result != ResultSuccess { + verifiedLS,result := VerifyToTarget(peerList.primary(), + root_of_trust, + nextHeight); + // TODO: in verifytotarget return only verification chain + // TODO: add tag pointer to verifytotarget + if result == ResultFailure { + // pick new primary (promote a secondary to primary) + peerList.Replace_Primary(); + } + } + + // Cross-check + // TODO: fix parameters and functions + Evidences := AttackDetector(root_of_trust, verifiedLS); + // TODO: add tag pointer to AttackDetector + if Evidences.Empty { + // no attack detected, we trust the new lightblock + lightStore.store_chain(verifidLS); + // TODO: add store_chain function + return (lightStore, OK); + } + else { + // there is an attack, we exit + return(lightStore, ErrorAttack); + } + } +} + +``` +- Implementation remark + - none +- Expected precondition + - none +- Expected postcondition + - lightblock of height *targetHeight* (and possibly additional blocks) added to *lightStore* +- Error condition + - an attack is detected + - [LC-DATA-PEERLIST-INV.1] is violated +---- + + + +TODO: submitEvidence(Evidences); in detector spec + + +### Solving the distributed specification + +TODO + + + +# Part V: Discussions on Changes Semantics of the LightStore + +In a previous version (TODO: versioning, link), +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 + + +---- + + + + From 77ed97eac7c13208105e937db44c8ecae1794d58 Mon Sep 17 00:00:00 2001 From: Marko Baricevic Date: Wed, 9 Sep 2020 18:03:21 +0200 Subject: [PATCH 02/15] markdown lint --- .markdownlint.yml | 1 + .../lightclient/supervisor/supervisor.md | 318 +++++++++--------- 2 files changed, 158 insertions(+), 161 deletions(-) diff --git a/.markdownlint.yml b/.markdownlint.yml index 9f8a8d68..6b4e78a3 100644 --- a/.markdownlint.yml +++ b/.markdownlint.yml @@ -1,4 +1,5 @@ default: true +MD001: false MD007: { indent: 4 } MD013: false MD024: { siblings_only: true } diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 23c12718..a20ac271 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -1,27 +1,24 @@ # Draft of Light Client Supervisor for discussion -## TODOs: +## TODOs - move part I of verification here (or copy) - incorporate the structure of Stevan's Rust supervisor design - - new versions of `verifytotarget` and `backwards` that take as + - new versions of `verifytotarget` and `backwards` that take as input a single lightblock and return a fully verified lightstore - - update tags to ".2" - - lightstore.update: remove Unverified upon leaving verifyTotarget - -check that all is addressed: + - update tags to ".2" + - lightstore.update: remove Unverified upon leaving verifyTotarget -- https://github.com/informalsystems/tendermint-rs/issues/499 -- https://github.com/informalsystems/tendermint-rs/pull/509 -- https://github.com/tendermint/spec/issues/131 -- https://github.com/informalsystems/tendermint-rs/issues/461 +check that all is addressed: +- +- +- +- - links to verification and detection specs - - # Light Client Sequential Supervisor The light client implements a read operation of a @@ -35,7 +32,7 @@ new block. The staking and unbonding mechanism induces a [security model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the [header][TMBC-HEADER-link], more than two-thirds of the next validators of a new block are correct -for the duration of *TrustedPeriod*. +for the duration of *TrustedPeriod*. [Light Client Verification](TODO) implements the fault-tolerant read operation designed for this security model. That is, it is safe if the @@ -47,7 +44,7 @@ faulty peers (that have been validators at some point in the past) may launch attacks on the Tendermint network, and on the light client. These attacks as well as an axiomatization of blocks in general are defined in [a document that contains the definitions that -are currently in detection.md](TODO). +are currently in detection.md](TODO). If there is a light client attack (but no successful attack on the network), the safety of the verification step @@ -86,7 +83,6 @@ documents, as is the [accountability](TODO) protocol. > relayer, as well as attack verification at the IBC handler. This > will call for yet another spec. - # Status This document is work in progress. In order to develop the @@ -96,27 +92,27 @@ it assumes certain details of [verification](TODO) and versions yet. This inconsistencies will be addresses over several upcoming PRs. - # Part I - Tendermint Blockchain TODO -# Part II - Sequential Problem Definition +# Part II - Sequential Problem Definition +#### **[LC-SEQ-INIT-LIVE.1]** -#### **[LC-SEQ-INIT-LIVE.1]**: Upon initialization, the light client gets as input a header of the blockchain, or the genesis file of the blockchain, and eventually stores a header of the blockchain. > TODO: be more precise about heights in spec above -#### **[LC-SEQ-LIVE.1]**: +#### **[LC-SEQ-LIVE.1]** + The light client gets a sequence of heights as inputs. For each input height *targetHeight*, it eventually stores the header of height *targetHeight*. -#### **[LC-SEQ-SAFE.1]**: +#### **[LC-SEQ-SAFE.1]** The light client never stores a header which is not in the blockchain. @@ -134,7 +130,7 @@ TODO: no main chain fork, that is, we assume all correct peers agree on one blockchain. But TFM is violated, that is, there are bonded validators that execute a light client attack (details should be mainly discussed in -verification and detection specs). +verification and detection specs). ## Distributed Problem Statement @@ -143,31 +139,33 @@ verification and detection specs). In case of light client attacks, the sequential problem statement cannot always be satisfied. The lightclient cannot decide which block is from the chain and which is not. As a result, the light client just -creates evidence, submits it, and terminates. +creates evidence, submits it, and terminates. For the liveness property, we thus add the possibility that instead of adding a lightblock, we also might terminate in case there is an attack. - -#### **[LC-DIST-TERM.1]**: +#### **[LC-DIST-TERM.1]** The light client either runs forever or it *terminates on attack*. ### Design choices -#### [LC-DIST-STORE.1]: -The light client has a local data structure called LightStore -that contains light blocks (that contain a header). +#### [LC-DIST-STORE.1] + +The light client has a local data structure called LightStore +that contains light blocks (that contain a header). TODO: put light store functions here (some are still in verification.md) -#### **[LC-DIST-SAFE.1]**: -It is always the case that every header in *LightStore* was +#### **[LC-DIST-SAFE.1]** + +It is always the case that every header in *LightStore* was generated by an instance of Tendermint consensus. -#### **[LC-DIST-LIVE.1]**: +#### **[LC-DIST-LIVE.1]** Whenever the light client gets a new height *h* as input, + - and there is no light client attack up to height *h*, then the lightclient eventually puts the lightblock of height *h* in the lightstore and @@ -186,18 +184,18 @@ download a correct lightblock (by the assumption that there is no fork on the chain and all correct peers agree on the blokchain). -> safety For liveness there are three scenarios + 1. no light client attack: all lightblocks match, and they are written to the lightstore 2. there is an attack a. one of the peers sends a lightblock involved in the attack to the lightclient -> by assumption that there is a correct peer, it will be detected, and we terminate on attack - b. the lightclient does not learn a faulty lightblock -> similar + b. the lightclient does not learn a faulty lightblock -> similar to case 1. # Part IV - Light Client Supervisor Protocol - We provide a specification for a sequential Light Client Supervisor. The local code for verification is presented by a sequential function `Sequential-Supervisor` to highlight the control flow of this @@ -206,13 +204,14 @@ cross-checked with secondaries, and if all goes well, the lightblock is added to the lightstore. That is, no lightblock is ever removed from the -lightstore, and all lightblocks in the lightstore are trusted. +lightstore, and all lightblocks in the lightstore are trusted. > We note that if a different concurrency model is considered > for an implementation, the semantics of the lightstore might change: > In a concurrent implementation, we might do verification for some > height *h*, add the > lightblock to the lightstore, and start concurrent threads that +> > - do verification for the next height *h' != h* > - do cross-checking for height *h*. If we find an attack, we remove > *h* from the lightstore. @@ -223,14 +222,14 @@ lightstore, and all lightblocks in the lightstore are trusted. > performance is worth it, we keep for future versions/discussion of > lightclient protocols. - ## Definitions ### Data Types The core data structure of the protocol is the LightBlock. -#### **[LC-DATA-LIGHTBLOCK.1]**: +#### **[LC-DATA-LIGHTBLOCK.1]** + ```go type LightBlock struct { Header Header @@ -239,9 +238,9 @@ type LightBlock struct { NextValidators ValidatorSet Provider PeerID } -``` +``` -#### **[LC-DATA-LIGHTSTORE.1]**: +#### **[LC-DATA-LIGHTSTORE.1]** LightBlocks are stored in a structure which stores all LightBlock from initialization or received from peers. @@ -257,35 +256,34 @@ The LightStore exposes the following functions to query stored LightBlocks. TODO: copy used new functions with tags. - - ### Inputs The lightclient is initialized with LCInitData -#### **[LC-DATA-INIT.1]**: +#### **[LC-DATA-INIT.1]** + ```go type LCInitData struct { - lightBlock LightBlock - genesisDoc GenesisDoc + lightBlock LightBlock + genesisDoc GenesisDoc } ``` where only one of the components must be provided. `GenesisDoc` is defined in the [Tendermint -Types](https://github.com/tendermint/tendermint/blob/master/types/genesis.go). +Types](https://github.com/tendermint/tendermint/blob/master/types/genesis.go). -#### **[LC-DATA-GENESIS.1]**: +#### **[LC-DATA-GENESIS.1]** ```go type GenesisDoc struct { - GenesisTime time.Time `json:"genesis_time"` - ChainID string `json:"chain_id"` - InitialHeight int64 `json:"initial_height"` - ConsensusParams *tmproto.ConsensusParams `json:"consensus_params,omitempty"` - Validators []GenesisValidator `json:"validators,omitempty"` - AppHash tmbytes.HexBytes `json:"app_hash"` - AppState json.RawMessage `json:"app_state,omitempty"` + GenesisTime time.Time `json:"genesis_time"` + ChainID string `json:"chain_id"` + InitialHeight int64 `json:"initial_height"` + ConsensusParams *tmproto.ConsensusParams `json:"consensus_params,omitempty"` + Validators []GenesisValidator `json:"validators,omitempty"` + AppHash tmbytes.HexBytes `json:"app_hash"` + AppState json.RawMessage `json:"app_state,omitempty"` } ``` @@ -294,10 +292,12 @@ We use the following function file in order to do verification based on the data from the genesis file using the same verification function we use in normal operation. -#### **[LC-FUNC-MAKEBLOCK.1]**: +#### **[LC-FUNC-MAKEBLOCK.1]** + ```go func makeblock (genesisDoc GenesisDoc) (lightBlock LightBlock)) ``` + - Implementation remark - none - Expected precondition @@ -309,17 +309,17 @@ func makeblock (genesisDoc GenesisDoc) (lightBlock LightBlock)) - lightBlock.Header.LastCommit = nil - lightBlock.Header.Validators = genesisDoc.Validators - lightBlock.Header.NextValidators = genesisDoc.Validators - - lightBlock.Header.Data = nil + - lightBlock.Header.Data = nil - lightBlock.Header.AppState = genesisDoc.AppState - lightBlock.Header.LastResult = nil - - lightBlock.Commit = nil - - lightBlock.Validators = genesisDoc.Validators - - lightBlock.NextValidators = genesisDoc.Validators - - lightBlock.Provider = nil + - lightBlock.Commit = nil + - lightBlock.Validators = genesisDoc.Validators + - lightBlock.NextValidators = genesisDoc.Validators + - lightBlock.Provider = nil - Error condition - none ----- +---- ### Configuration Parameters @@ -329,7 +329,7 @@ func makeblock (genesisDoc GenesisDoc) (lightBlock LightBlock)) **TODO** -- PeerList. +- PeerList. It exposes the functions @@ -345,13 +345,12 @@ init data is OK ### Invariants #### **[LC-DATA-PEERLIST.1]:** + The peer list contains a primary and a secondary. > If the invariant is violated, the light client does not have enough > peers to download headers from. As a result, the light client -> needs to terminate in case this invariant is violated. - - +> needs to terminate in case this invariant is violated. ## Supervisor @@ -372,44 +371,46 @@ to the lightstore, which is returned in an output event to the user. The following main loop does the interaction with the user (input, output) and calls the following two functions: + - `InitLightClient`: it initializes the lightstore either with the provided lightblock or with the lightblock that corresponds to the first block generated by the blockchain (by the validators defined by the genesis file) - `VerifyAndDetect`: takes as input a lightstore and a height and - returns the updated lightstore. + returns the updated lightstore. #### **[LC-FUNC-SUPERVISOR.1]:** ```go func Sequential-Supervisor (initdata LCInitData) (Error) { - - lightStore,result := InitLightClient(initData); - if result != OK { - return result; - } - + + lightStore,result := InitLightClient(initData); + if result != OK { + return result; + } + loop { - // get the next height + // get the next height nextHeight := input(); - - lightStore,result := VerifyAndDetect(lightStore, nextHeight); - - if result == OK { - output(LightStore) - } - else { - return result - } - // QUESTION: is it OK to generate output event in normal case, - // and terminate with failure in the (light client) attack case? - } + + lightStore,result := VerifyAndDetect(lightStore, nextHeight); + + if result == OK { + output(LightStore) + } + else { + return result + } + // QUESTION: is it OK to generate output event in normal case, + // and terminate with failure in the (light client) attack case? + } } ``` + - Implementation remark - infinite loop unless a light client attack is detected - Expected precondition - - *LCInitData* contains a genesis file or a lightblock. + - *LCInitData* contains a genesis file or a lightblock. - Expected postcondition - if a light client attack is detected: it stops and submits evidence (in `InitLightClient` or `VerifyAndDetect`) @@ -417,9 +418,9 @@ func Sequential-Supervisor (initdata LCInitData) (Error) { - Invariant: *lightStore* contains trusted lightblocks only. - Error condition - if `InitLightClient` or `VerifyAndDetect` fails (if a attack is - detected, or if [LCV-INV-TP.1] is violated) ----- + detected, or if [LCV-INV-TP.1] is violated) +---- ### Details of the Functions @@ -446,73 +447,73 @@ we want to maintain [LCV-INV-TP.1] from the beginning. > without adding effective robustness. #### **[LC-FUNC-INIT.1]:** + ```go func InitLightClient (initData LCInitData) (LightStore, Error) { if LCInitData.LightBlock != nil { - // we trust the provided initial block. + // we trust the provided initial block. newblock := LCInitData.LightBlock } else { - genesisBlock := makeblock(initData.genesisDoc); + genesisBlock := makeblock(initData.genesisDoc); result := NoResult; while result != ResultSuccess { current = FetchLightBlock(PeerList.primary(), genesisBlock.Header.Height + 1) // QUESTION: is the height with "+1" OK? - + if CANNOT_VERIFY = ValidAndVerify(genesisBlock, current) { - // TODO: remove "trusted.Commit is a commit for the header - // trusted.Header, i.e., it contains the correct hash of the - // header, and +2/3 of signatures" from validAndVerified precondition - peerList.replacePrimary(); - } - else { - result = ResultSuccess - } - } - + // TODO: remove "trusted.Commit is a commit for the header + // trusted.Header, i.e., it contains the correct hash of the + // header, and +2/3 of signatures" from validAndVerified precondition + peerList.replacePrimary(); + } + else { + result = ResultSuccess + } + } + // cross-check - Evidences := AttackDetector(genesisBlock, current) - // TODO: wrap current in an auxiliary lightstore + Evidences := AttackDetector(genesisBlock, current) + // TODO: wrap current in an auxiliary lightstore if Evidences.Empty { - newBlock := current - } - else { - submitEvidence(Evidences); + newBlock := current + } + else { + submitEvidence(Evidences); return(nil, ErrorAttack); - } + } } lightStore := new LightStore; lightStore.Add(newBlock); //TODO: add Add to lightstore functions return (lightStore, OK); } - + ``` + - Implementation remark - none - Expected precondition - - *LCInitData* contains either a genesis file of a lightblock - - if genesis it passes `ValidateAndComplete()` see [Tendermint](TODO) + - *LCInitData* contains either a genesis file of a lightblock + - if genesis it passes `ValidateAndComplete()` see [Tendermint](TODO) - Expected postcondition - *lightStore* initialized with trusted lightblock. It has either been cross-checked (from genesis) or it has initial trust from the user. - Error condition - if precondition is violated - - empty peerList ----- + - empty peerList +---- #### Main verification and detection logic - - #### **[LC-FUNC-MAIN-VERIF-DETECT.1]:** ```go -func VerifyAndDetect (lightStore LightStore, targetHeight Height) +func VerifyAndDetect (lightStore LightStore, targetHeight Height) (LightStore, Result) { b1, r1 = lightStore.Get(targetHeight) @@ -522,79 +523,77 @@ func VerifyAndDetect (lightStore LightStore, targetHeight Height) } // get the lightblock with maximum height smaller than targetHeight - // would typically be the heighest, if we always move forward + // would typically be the heighest, if we always move forward root_of_trust, r2 = lightStore.LatestPrevious(targetHeight); if r2 = false { - // there is no lightblock from which we can do forward - // (skipping) verification. Thus we have to go backwards. - // No cross-check needed. We trust hashes. Therefore, we - // directly return the result + // there is no lightblock from which we can do forward + // (skipping) verification. Thus we have to go backwards. + // No cross-check needed. We trust hashes. Therefore, we + // directly return the result return Backwards(peerList.primary(), lightStore.lowest, targetHeight) - // TODO: in Backwards definition pointers need to be fixed to - // predecessor - // TODO: add tag pointer to Backwards - // TODO: define lightStore.lowest - } - else { + // TODO: in Backwards definition pointers need to be fixed to + // predecessor + // TODO: add tag pointer to Backwards + // TODO: define lightStore.lowest + } + else { // Forward verification + detection result := NoResult; while result != ResultSuccess { verifiedLS,result := VerifyToTarget(peerList.primary(), - root_of_trust, - nextHeight); - // TODO: in verifytotarget return only verification chain - // TODO: add tag pointer to verifytotarget - if result == ResultFailure { - // pick new primary (promote a secondary to primary) - peerList.Replace_Primary(); - } + root_of_trust, + nextHeight); + // TODO: in verifytotarget return only verification chain + // TODO: add tag pointer to verifytotarget + if result == ResultFailure { + // pick new primary (promote a secondary to primary) + peerList.Replace_Primary(); + } } - - // Cross-check - // TODO: fix parameters and functions + + // Cross-check + // TODO: fix parameters and functions Evidences := AttackDetector(root_of_trust, verifiedLS); - // TODO: add tag pointer to AttackDetector - if Evidences.Empty { - // no attack detected, we trust the new lightblock + // TODO: add tag pointer to AttackDetector + if Evidences.Empty { + // no attack detected, we trust the new lightblock lightStore.store_chain(verifidLS); - // TODO: add store_chain function - return (lightStore, OK); - } + // TODO: add store_chain function + return (lightStore, OK); + } else { - // there is an attack, we exit + // there is an attack, we exit return(lightStore, ErrorAttack); } - } + } } ``` + - Implementation remark - none - Expected precondition - - none + - none - Expected postcondition - - lightblock of height *targetHeight* (and possibly additional blocks) added to *lightStore* + - lightblock of height *targetHeight* (and possibly additional blocks) added to *lightStore* - Error condition - an attack is detected - - [LC-DATA-PEERLIST-INV.1] is violated ----- - + - [LC-DATA-PEERLIST-INV.1] is violated +---- TODO: submitEvidence(Evidences); in detector spec - ### Solving the distributed specification TODO - - # Part V: Discussions on Changes Semantics of the LightStore In a previous version (TODO: versioning, link), a lightblock in the lightstore can be in one of the following states: + - StateUnverified - StateVerified - StateFailed @@ -623,24 +622,21 @@ 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 + +- 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 +- 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 +- 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 +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 - ---- - - - - From 3d6a023ffe9825a7637421e1a0e07fd9d7760758 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 9 Sep 2020 22:13:32 +0200 Subject: [PATCH 03/15] TODO links replaced --- .../lightclient/supervisor/supervisor.md | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index a20ac271..feb639bd 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -10,6 +10,8 @@ - update tags to ".2" - lightstore.update: remove Unverified upon leaving verifyTotarget +- replace links to "https://informal.systems/" with proper links + check that all is addressed: - @@ -34,7 +36,7 @@ model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the more than two-thirds of the next validators of a new block are correct for the duration of *TrustedPeriod*. -[Light Client Verification](TODO) implements the fault-tolerant read +[Light Client Verification](https://informal.systems/) implements the fault-tolerant read operation designed for this security model. That is, it is safe if the model assumptions are satisfied and makes progress if it communicates to a correct primary. @@ -44,7 +46,7 @@ faulty peers (that have been validators at some point in the past) may launch attacks on the Tendermint network, and on the light client. These attacks as well as an axiomatization of blocks in general are defined in [a document that contains the definitions that -are currently in detection.md](TODO). +are currently in detection.md](https://informal.systems/). If there is a light client attack (but no successful attack on the network), the safety of the verification step @@ -52,7 +54,7 @@ may be violated (as we operate outside its basic assumption). The light client also contains a defense mechanism against light clients attacks, called detection. -[Light Client Detection](TODO) implements a cross check of the result +[Light Client Detection](https://informal.systems/) implements a cross check of the result of the verification step. If there is a light client attack, and the light client is connected to a correct peer, the light client as a whole is safe, that is, it will not operate on invalid @@ -63,7 +65,7 @@ evidence. Evidence can be used to prove to a correct full node that there has been a light client attack. -[Light Client Evidence Accountability](TODO) is a protocol run on a +[Light Client Evidence Accountability](https://informal.systems/) is a protocol run on a full node to check whether submitted evidence indeed proves the existence of a light client attack. Further, from the evidence and its own knowledge about the blockchain, the full node computes a set of @@ -74,10 +76,10 @@ via ABCI to the application. In this document we specify - Initialization of the Light Client -- The interaction of [verification](TODO) and [detection](TODO) +- The interaction of [verification](https://informal.systems/) and [detection](https://informal.systems/) The details of these two protocols are captured in their own -documents, as is the [accountability](TODO) protocol. +documents, as is the [accountability](https://informal.systems/) protocol. > Another related line is IBC attack detection and submission at the > relayer, as well as attack verification at the IBC handler. This @@ -87,8 +89,8 @@ documents, as is the [accountability](TODO) protocol. This document is work in progress. In order to develop the specification step-by-step, -it assumes certain details of [verification](TODO) and -[detection](TODO) that are not specified in the respective current +it assumes certain details of [verification](https://informal.systems/) and +[detection](https://informal.systems/) that are not specified in the respective current versions yet. This inconsistencies will be addresses over several upcoming PRs. @@ -438,8 +440,8 @@ we want to maintain [LCV-INV-TP.1] from the beginning. > it may increase trust, when one cross-checks the initial light > block. However, if a peer provides a conflicting > lightblock, the question is to distinguish the case of a -> [bogus](TODO) block (upon which operation should proceed) from a -> [light client attack](TODO) (upon which operation should stop). In +> [bogus](https://informal.systems/) block (upon which operation should proceed) from a +> [light client attack](https://informal.systems/) (upon which operation should stop). In > case of a bogus block, the lightclient might be forced to do > backwards verification until the blocks are out of the trusting > period, to make sure no previous validator set could have generated @@ -497,7 +499,7 @@ func InitLightClient (initData LCInitData) (LightStore, Error) { - none - Expected precondition - *LCInitData* contains either a genesis file of a lightblock - - if genesis it passes `ValidateAndComplete()` see [Tendermint](TODO) + - if genesis it passes `ValidateAndComplete()` see [Tendermint](https://informal.systems/) - Expected postcondition - *lightStore* initialized with trusted lightblock. It has either been cross-checked (from genesis) or it has initial trust from the From d16a4a191dd9adfa01856a71657294a920078291 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 9 Sep 2020 22:23:33 +0200 Subject: [PATCH 04/15] links --- .../lightclient/supervisor/supervisor.md | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index feb639bd..3b497998 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -10,7 +10,7 @@ - update tags to ".2" - lightstore.update: remove Unverified upon leaving verifyTotarget -- replace links to "https://informal.systems/" with proper links +- replace links to "https://informal.systems" with proper links check that all is addressed: @@ -36,7 +36,7 @@ model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the more than two-thirds of the next validators of a new block are correct for the duration of *TrustedPeriod*. -[Light Client Verification](https://informal.systems/) implements the fault-tolerant read +[Light Client Verification](https://informal.systems) implements the fault-tolerant read operation designed for this security model. That is, it is safe if the model assumptions are satisfied and makes progress if it communicates to a correct primary. @@ -46,7 +46,7 @@ faulty peers (that have been validators at some point in the past) may launch attacks on the Tendermint network, and on the light client. These attacks as well as an axiomatization of blocks in general are defined in [a document that contains the definitions that -are currently in detection.md](https://informal.systems/). +are currently in detection.md](https://informal.systems). If there is a light client attack (but no successful attack on the network), the safety of the verification step @@ -54,7 +54,7 @@ may be violated (as we operate outside its basic assumption). The light client also contains a defense mechanism against light clients attacks, called detection. -[Light Client Detection](https://informal.systems/) implements a cross check of the result +[Light Client Detection](https://informal.systems) implements a cross check of the result of the verification step. If there is a light client attack, and the light client is connected to a correct peer, the light client as a whole is safe, that is, it will not operate on invalid @@ -65,7 +65,7 @@ evidence. Evidence can be used to prove to a correct full node that there has been a light client attack. -[Light Client Evidence Accountability](https://informal.systems/) is a protocol run on a +[Light Client Evidence Accountability](https://informal.systems) is a protocol run on a full node to check whether submitted evidence indeed proves the existence of a light client attack. Further, from the evidence and its own knowledge about the blockchain, the full node computes a set of @@ -76,10 +76,10 @@ via ABCI to the application. In this document we specify - Initialization of the Light Client -- The interaction of [verification](https://informal.systems/) and [detection](https://informal.systems/) +- The interaction of [verification](https://informal.systems) and [detection](https://informal.systems) The details of these two protocols are captured in their own -documents, as is the [accountability](https://informal.systems/) protocol. +documents, as is the [accountability](https://informal.systems) protocol. > Another related line is IBC attack detection and submission at the > relayer, as well as attack verification at the IBC handler. This @@ -89,8 +89,8 @@ documents, as is the [accountability](https://informal.systems/) protocol. This document is work in progress. In order to develop the specification step-by-step, -it assumes certain details of [verification](https://informal.systems/) and -[detection](https://informal.systems/) that are not specified in the respective current +it assumes certain details of [verification](https://informal.systems) and +[detection](https://informal.systems) that are not specified in the respective current versions yet. This inconsistencies will be addresses over several upcoming PRs. @@ -440,8 +440,8 @@ we want to maintain [LCV-INV-TP.1] from the beginning. > it may increase trust, when one cross-checks the initial light > block. However, if a peer provides a conflicting > lightblock, the question is to distinguish the case of a -> [bogus](https://informal.systems/) block (upon which operation should proceed) from a -> [light client attack](https://informal.systems/) (upon which operation should stop). In +> [bogus](https://informal.systems) block (upon which operation should proceed) from a +> [light client attack](https://informal.systems) (upon which operation should stop). In > case of a bogus block, the lightclient might be forced to do > backwards verification until the blocks are out of the trusting > period, to make sure no previous validator set could have generated @@ -499,7 +499,7 @@ func InitLightClient (initData LCInitData) (LightStore, Error) { - none - Expected precondition - *LCInitData* contains either a genesis file of a lightblock - - if genesis it passes `ValidateAndComplete()` see [Tendermint](https://informal.systems/) + - if genesis it passes `ValidateAndComplete()` see [Tendermint](https://informal.systems) - Expected postcondition - *lightStore* initialized with trusted lightblock. It has either been cross-checked (from genesis) or it has initial trust from the From e539705d7f01638924e99d9f3b7be3b73b9a9880 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 9 Sep 2020 22:26:38 +0200 Subject: [PATCH 05/15] links --- rust-spec/lightclient/supervisor/supervisor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 3b497998..5c583c94 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -10,7 +10,7 @@ - update tags to ".2" - lightstore.update: remove Unverified upon leaving verifyTotarget -- replace links to "https://informal.systems" with proper links +- replace links to https://informal.systems with proper links check that all is addressed: From 7365e46846d7da9027fc745e4c4d9ff32594ec47 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 9 Sep 2020 22:31:02 +0200 Subject: [PATCH 06/15] links lint --- rust-spec/lightclient/supervisor/supervisor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 5c583c94..81c287c5 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -10,7 +10,7 @@ - update tags to ".2" - lightstore.update: remove Unverified upon leaving verifyTotarget -- replace links to https://informal.systems with proper links +- replace links to [TODO](https://informal.systems) with proper links check that all is addressed: From cfcc61ebe78cb0dfcb234457883d067623789121 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 17 Sep 2020 13:14:37 +0200 Subject: [PATCH 07/15] Update rust-spec/lightclient/supervisor/supervisor.md --- rust-spec/lightclient/supervisor/supervisor.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 81c287c5..7dcc1e61 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -340,6 +340,11 @@ It exposes the functions - replace_primary() - replace secondary(peerID PeerID) +#### **[LC-INV-ROOT-AGREED.1]** + +In the Sequential-Supervisor, it is always the case that the primary +and all secondaries agree on lightStore.Latest(). + ### Assumptions init data is OK From 99b306183e31d13fb984ef21a71a031ec7914c79 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 17 Sep 2020 16:27:03 +0200 Subject: [PATCH 08/15] Update rust-spec/lightclient/supervisor/supervisor.md --- rust-spec/lightclient/supervisor/supervisor.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 7dcc1e61..596b869b 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -488,6 +488,8 @@ func InitLightClient (initData LCInitData) (LightStore, Error) { newBlock := current } else { + // [LC-SUMBIT-EVIDENCE.1] + // TODO: link to upcoming detector spec submitEvidence(Evidences); return(nil, ErrorAttack); } From 82607f3e43f6f651120d10123c99f5fe5f23b025 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 17 Sep 2020 16:29:28 +0200 Subject: [PATCH 09/15] Update rust-spec/lightclient/supervisor/supervisor.md --- rust-spec/lightclient/supervisor/supervisor.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 596b869b..2377f8d3 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -4,6 +4,8 @@ - move part I of verification here (or copy) +- move evidence submission into detector spec + - incorporate the structure of Stevan's Rust supervisor design - new versions of `verifytotarget` and `backwards` that take as input a single lightblock and return a fully verified lightstore From 3f968c6ceea46ce37bc40ce82fc079d34e495f08 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 17 Sep 2020 16:38:34 +0200 Subject: [PATCH 10/15] Update rust-spec/lightclient/supervisor/supervisor.md --- rust-spec/lightclient/supervisor/supervisor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 2377f8d3..36460001 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -4,7 +4,7 @@ - move part I of verification here (or copy) -- move evidence submission into detector spec +- move evidence submission into detector spec **QUESTION** Initially I wanted to have evidence submission here. Somewhat it feels at it should be visible at the supervisor. But the evidence is generated within the attack detector. Therefore all the definitions are there. Where should we put it? - incorporate the structure of Stevan's Rust supervisor design - new versions of `verifytotarget` and `backwards` that take as From 646ee318bc086f18d332f4b1462312aaedc77408 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 17 Sep 2020 17:03:15 +0200 Subject: [PATCH 11/15] moved peer handling definitions to supervisor --- .../lightclient/supervisor/supervisor.md | 133 ++++++++++++------ 1 file changed, 93 insertions(+), 40 deletions(-) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index 36460001..e434e65a 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -228,6 +228,70 @@ lightstore, and all lightblocks in the lightstore are trusted. ## Definitions +### Peers + +#### **[LC-DATA-PEERS.1]:** + +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 + +#### **[LC-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* + +#### **[LC-FUNC-REPLACE-PRIMARY.1]:** + +```go +Replace_Primary(root-of-trust LightBlock) +``` + +- Implementation remark + - the primary is replaced by a secondary + - to maintain a constant size of secondaries, need to + - pick a new secondary *nsec* while ensuring [LC-INV-ROOT-AGREED.1] + - that is, we need to ensure that root-of-trust = FetchLightBlock(nsec, root-of-trust.Header.Height) +- Expected precondition + - *FullNodes* is nonempty +- Expected postcondition + - *primary* is moved to *FaultyNodes* + - a secondary *s* is moved from *Secondaries* to primary +- Error condition + - if precondition is violated + +#### **[LC-FUNC-REPLACE-SECONDARY.1]:** + +```go +Replace_Secondary(addr Address, root-of-trust LightBlock) +``` + +- Implementation remark + - maintain [LCD-INV-ROOT-AGREED.1], that is, + ensure root-of-trust = FetchLightBlock(nsec, root-of-trust.Header.Height) +- Expected precondition + - *FullNodes* is nonempty +- Expected postcondition + - addr is moved from *Secondaries* to *FaultyNodes* + - an address *nsec* is moved from *FullNodes* to *Secondaries* +- Error condition + - if precondition is violated + + + ### Data Types The core data structure of the protocol is the LightBlock. @@ -329,18 +393,7 @@ func makeblock (genesisDoc GenesisDoc) (lightBlock LightBlock)) **TODO:** trusting period -### Variables -**TODO** - -- PeerList. - -It exposes the functions - -- primary() -- secondaries() -- replace_primary() -- replace secondary(peerID PeerID) #### **[LC-INV-ROOT-AGREED.1]** @@ -476,7 +529,7 @@ func InitLightClient (initData LCInitData) (LightStore, Error) { // TODO: remove "trusted.Commit is a commit for the header // trusted.Header, i.e., it contains the correct hash of the // header, and +2/3 of signatures" from validAndVerified precondition - peerList.replacePrimary(); + Replace_Primary(); } else { result = ResultSuccess @@ -534,49 +587,49 @@ func VerifyAndDetect (lightStore LightStore, targetHeight Height) } // get the lightblock with maximum height smaller than targetHeight - // would typically be the heighest, if we always move forward + // would typically be the heighest, if we always move forward root_of_trust, r2 = lightStore.LatestPrevious(targetHeight); if r2 = false { - // there is no lightblock from which we can do forward - // (skipping) verification. Thus we have to go backwards. - // No cross-check needed. We trust hashes. Therefore, we - // directly return the result - return Backwards(peerList.primary(), lightStore.lowest, targetHeight) - // TODO: in Backwards definition pointers need to be fixed to - // predecessor - // TODO: add tag pointer to Backwards - // TODO: define lightStore.lowest - } - else { + // there is no lightblock from which we can do forward + // (skipping) verification. Thus we have to go backwards. + // No cross-check needed. We trust hashes. Therefore, we + // directly return the result + return Backwards(peerList.primary(), lightStore.lowest, targetHeight) + // TODO: in Backwards definition pointers need to be fixed to + // predecessor + // TODO: add tag pointer to Backwards + // TODO: define lightStore.lowest + } + else { // Forward verification + detection result := NoResult; while result != ResultSuccess { verifiedLS,result := VerifyToTarget(peerList.primary(), - root_of_trust, - nextHeight); - // TODO: in verifytotarget return only verification chain - // TODO: add tag pointer to verifytotarget + root_of_trust, + nextHeight); + // TODO: in verifytotarget return only verification chain + // TODO: add tag pointer to verifytotarget if result == ResultFailure { - // pick new primary (promote a secondary to primary) - peerList.Replace_Primary(); - } + // pick new primary (promote a secondary to primary) + Replace_Primary(root_of_trust); + } } - // Cross-check - // TODO: fix parameters and functions + // Cross-check + // TODO: fix parameters and functions Evidences := AttackDetector(root_of_trust, verifiedLS); - // TODO: add tag pointer to AttackDetector - if Evidences.Empty { - // no attack detected, we trust the new lightblock + // TODO: add tag pointer to AttackDetector + if Evidences.Empty { + // no attack detected, we trust the new lightblock lightStore.store_chain(verifidLS); - // TODO: add store_chain function - return (lightStore, OK); + // TODO: add store_chain function + return (lightStore, OK); } else { - // there is an attack, we exit + // there is an attack, we exit return(lightStore, ErrorAttack); } - } + } } ``` From fe59c67835d9f30462208fdb0acf746a3c6241bf Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Tue, 29 Sep 2020 16:24:30 +0200 Subject: [PATCH 12/15] polishing --- .../lightclient/supervisor/supervisor.md | 164 +++++++----------- 1 file changed, 67 insertions(+), 97 deletions(-) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor.md index e434e65a..f8f6c092 100644 --- a/rust-spec/lightclient/supervisor/supervisor.md +++ b/rust-spec/lightclient/supervisor/supervisor.md @@ -6,11 +6,6 @@ - move evidence submission into detector spec **QUESTION** Initially I wanted to have evidence submission here. Somewhat it feels at it should be visible at the supervisor. But the evidence is generated within the attack detector. Therefore all the definitions are there. Where should we put it? -- incorporate the structure of Stevan's Rust supervisor design - - new versions of `verifytotarget` and `backwards` that take as - input a single lightblock and return a fully verified lightstore - - update tags to ".2" - - lightstore.update: remove Unverified upon leaving verifyTotarget - replace links to [TODO](https://informal.systems) with proper links @@ -26,15 +21,15 @@ check that all is addressed: # Light Client Sequential Supervisor The light client implements a read operation of a -[header][TMBC-HEADER-link] from the [blockchain][TMBC-SEQ-link], by +[header](TMBC-HEADER-link) from the [blockchain](TMBC-SEQ-link), by communicating with full nodes, a so-called primary and several so-called witnesses. As some full nodes may be faulty, this functionality must be implemented in a fault-tolerant way. In the Tendermint blockchain, the validator set may change with every new block. The staking and unbonding mechanism induces a [security -model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the -[header][TMBC-HEADER-link], +model](TMBC-FM-2THIRDS-link): starting at time *Time* of the +[header](TMBC-HEADER-link), more than two-thirds of the next validators of a new block are correct for the duration of *TrustedPeriod*. @@ -43,7 +38,7 @@ operation designed for this security model. That is, it is safe if the model assumptions are satisfied and makes progress if it communicates to a correct primary. -However, if the [security model][TMBC-FM-2THIRDS-link] is violated, +However, if the [security model](TMBC-FM-2THIRDS-link) is violated, faulty peers (that have been validators at some point in the past) may launch attacks on the Tendermint network, and on the light client. These attacks as well as an axiomatization of blocks in @@ -108,7 +103,6 @@ Upon initialization, the light client gets as input a header of the blockchain, or the genesis file of the blockchain, and eventually stores a header of the blockchain. -> TODO: be more precise about heights in spec above #### **[LC-SEQ-LIVE.1]** @@ -124,17 +118,9 @@ The light client never stores a header which is not in the blockchain. ## Computational Model -TODO: primary, witness (should be mainly discussed in detection -spec). - -TODO: always connected to a correct peer (should be mainly discussed -in detection spec). responds in time - -TODO: no main chain fork, that is, we assume all correct peers agree -on one blockchain. But TFM is violated, that is, there are bonded -validators that execute a light client attack -(details should be mainly discussed in -verification and detection specs). +The light client communicates with remote processes only via the +[verification](TODO) and the [detection](TODO) protocols. The +respective assumptions are given there. ## Distributed Problem Statement @@ -159,13 +145,19 @@ The light client either runs forever or it *terminates on attack*. The light client has a local data structure called LightStore that contains light blocks (that contain a header). -TODO: put light store functions here (some are still in verification.md) +> The light store exposes functions to query and update it. They are +> specified [here](TODO:onceVerificationIsMerged). + +**TODO:** reference light store invariant [LCV-INV-LS-ROOT.2] once +verification is merged + #### **[LC-DIST-SAFE.1]** It is always the case that every header in *LightStore* was generated by an instance of Tendermint consensus. + #### **[LC-DIST-LIVE.1]** Whenever the light client gets a new height *h* as input, @@ -183,20 +175,12 @@ wait for another input. ### Solving the sequential specification -TODO: as one of the peers is correct, the lightclient will always -download a correct lightblock (by the assumption that there is no fork -on the chain and all correct peers agree on the blokchain). -> safety +[LC-DIST-SAFE.1] is guaranteed by the detector; in particular it +follows from +[[LCD-DIST-INV-STORE.1]](TODO) +[[LCD-DIST-LIVE.1]](TODO) -For liveness there are three scenarios -1. no light client attack: all lightblocks match, and they are written - to the lightstore -2. there is an attack - a. one of the peers sends a lightblock involved in the attack to - the lightclient -> by assumption that there is a correct peer, it - will be detected, and we terminate on attack - b. the lightclient does not learn a faulty lightblock -> similar - to case 1. # Part IV - Light Client Supervisor Protocol @@ -225,6 +209,8 @@ lightstore, and all lightblocks in the lightstore are trusted. > we find a problem). Whether this is desirable, and whether the gain in > performance is worth it, we keep for future versions/discussion of > lightclient protocols. +> +> ## Definitions @@ -320,9 +306,9 @@ type LightStore struct { ``` -The LightStore exposes the following functions to query stored LightBlocks. +The LightStore exposes functions to query stored LightBlocks, which +are defined in the [verification specification](TODO). -TODO: copy used new functions with tags. ### Inputs @@ -332,8 +318,8 @@ The lightclient is initialized with LCInitData ```go type LCInitData struct { - lightBlock LightBlock - genesisDoc GenesisDoc + lightBlock LightBlock + genesisDoc GenesisDoc } ``` @@ -345,13 +331,13 @@ Types](https://github.com/tendermint/tendermint/blob/master/types/genesis.go). ```go type GenesisDoc struct { - GenesisTime time.Time `json:"genesis_time"` - ChainID string `json:"chain_id"` - InitialHeight int64 `json:"initial_height"` - ConsensusParams *tmproto.ConsensusParams `json:"consensus_params,omitempty"` - Validators []GenesisValidator `json:"validators,omitempty"` - AppHash tmbytes.HexBytes `json:"app_hash"` - AppState json.RawMessage `json:"app_state,omitempty"` + GenesisTime time.Time `json:"genesis_time"` + ChainID string `json:"chain_id"` + InitialHeight int64 `json:"initial_height"` + ConsensusParams *tmproto.ConsensusParams `json:"consensus_params,omitempty"` + Validators []GenesisValidator `json:"validators,omitempty"` + AppHash tmbytes.HexBytes `json:"app_hash"` + AppState json.RawMessage `json:"app_state,omitempty"` } ``` @@ -391,9 +377,6 @@ func makeblock (genesisDoc GenesisDoc) (lightBlock LightBlock)) ### Configuration Parameters -**TODO:** trusting period - - #### **[LC-INV-ROOT-AGREED.1]** @@ -402,11 +385,13 @@ and all secondaries agree on lightStore.Latest(). ### Assumptions -init data is OK +We have to assume that the initialization data (the lightblock or the +genesis file) are consistent with the blockchain. This is subjective +initialization and it cannot be checked locally. ### Invariants -#### **[LC-DATA-PEERLIST.1]:** +#### **[LC-INV-PEERLIST.1]:** The peer list contains a primary and a secondary. @@ -446,26 +431,26 @@ output) and calls the following two functions: ```go func Sequential-Supervisor (initdata LCInitData) (Error) { - lightStore,result := InitLightClient(initData); - if result != OK { - return result; - } + lightStore,result := InitLightClient(initData); + if result != OK { + return result; + } loop { - // get the next height + // get the next height nextHeight := input(); - lightStore,result := VerifyAndDetect(lightStore, nextHeight); + lightStore,result := VerifyAndDetect(lightStore, nextHeight); - if result == OK { - output(LightStore) - } - else { - return result - } - // QUESTION: is it OK to generate output event in normal case, - // and terminate with failure in the (light client) attack case? - } + if result == OK { + output(LightStore); + } + else { + return result + } + // QUESTION: is it OK to generate output event in normal case, + // and terminate with failure in the (light client) attack case? + } } ``` @@ -514,11 +499,11 @@ we want to maintain [LCV-INV-TP.1] from the beginning. func InitLightClient (initData LCInitData) (LightStore, Error) { if LCInitData.LightBlock != nil { - // we trust the provided initial block. + // we trust the provided initial block. newblock := LCInitData.LightBlock } else { - genesisBlock := makeblock(initData.genesisDoc); + genesisBlock := makeblock(initData.genesisDoc); result := NoResult; while result != ResultSuccess { @@ -526,28 +511,25 @@ func InitLightClient (initData LCInitData) (LightStore, Error) { // QUESTION: is the height with "+1" OK? if CANNOT_VERIFY = ValidAndVerify(genesisBlock, current) { - // TODO: remove "trusted.Commit is a commit for the header - // trusted.Header, i.e., it contains the correct hash of the - // header, and +2/3 of signatures" from validAndVerified precondition - Replace_Primary(); - } - else { - result = ResultSuccess - } - } + Replace_Primary(); + } + else { + result = ResultSuccess + } + } // cross-check - Evidences := AttackDetector(genesisBlock, current) - // TODO: wrap current in an auxiliary lightstore + auxLS := new LightStore + auxLS.Add(current) + Evidences := AttackDetector(genesisBlock, auxLS) if Evidences.Empty { - newBlock := current - } - else { - // [LC-SUMBIT-EVIDENCE.1] - // TODO: link to upcoming detector spec - submitEvidence(Evidences); + newBlock := current + } + else { + // [LC-SUMBIT-EVIDENCE.1] + submitEvidence(Evidences); return(nil, ErrorAttack); - } + } } lightStore := new LightStore; @@ -595,9 +577,6 @@ func VerifyAndDetect (lightStore LightStore, targetHeight Height) // No cross-check needed. We trust hashes. Therefore, we // directly return the result return Backwards(peerList.primary(), lightStore.lowest, targetHeight) - // TODO: in Backwards definition pointers need to be fixed to - // predecessor - // TODO: add tag pointer to Backwards // TODO: define lightStore.lowest } else { @@ -607,8 +586,6 @@ func VerifyAndDetect (lightStore LightStore, targetHeight Height) verifiedLS,result := VerifyToTarget(peerList.primary(), root_of_trust, nextHeight); - // TODO: in verifytotarget return only verification chain - // TODO: add tag pointer to verifytotarget if result == ResultFailure { // pick new primary (promote a secondary to primary) Replace_Primary(root_of_trust); @@ -616,13 +593,10 @@ func VerifyAndDetect (lightStore LightStore, targetHeight Height) } // Cross-check - // TODO: fix parameters and functions Evidences := AttackDetector(root_of_trust, verifiedLS); - // TODO: add tag pointer to AttackDetector if Evidences.Empty { // no attack detected, we trust the new lightblock lightStore.store_chain(verifidLS); - // TODO: add store_chain function return (lightStore, OK); } else { @@ -646,11 +620,7 @@ func VerifyAndDetect (lightStore LightStore, targetHeight Height) ---- -TODO: submitEvidence(Evidences); in detector spec -### Solving the distributed specification - -TODO # Part V: Discussions on Changes Semantics of the LightStore From fdcb4f80cda09fd7b28e84150de0267dcbf1e375 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Tue, 29 Sep 2020 16:25:05 +0200 Subject: [PATCH 13/15] rename --- .../supervisor/{supervisor.md => supervisor_001_draft.md} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename rust-spec/lightclient/supervisor/{supervisor.md => supervisor_001_draft.md} (100%) diff --git a/rust-spec/lightclient/supervisor/supervisor.md b/rust-spec/lightclient/supervisor/supervisor_001_draft.md similarity index 100% rename from rust-spec/lightclient/supervisor/supervisor.md rename to rust-spec/lightclient/supervisor/supervisor_001_draft.md From c71a84b72c505cf3442b67338be5b19d5bb62408 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Tue, 29 Sep 2020 16:29:35 +0200 Subject: [PATCH 14/15] Update rust-spec/lightclient/supervisor/supervisor_001_draft.md --- rust-spec/lightclient/supervisor/supervisor_001_draft.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-spec/lightclient/supervisor/supervisor_001_draft.md b/rust-spec/lightclient/supervisor/supervisor_001_draft.md index f8f6c092..cd8091b9 100644 --- a/rust-spec/lightclient/supervisor/supervisor_001_draft.md +++ b/rust-spec/lightclient/supervisor/supervisor_001_draft.md @@ -533,7 +533,7 @@ func InitLightClient (initData LCInitData) (LightStore, Error) { } lightStore := new LightStore; - lightStore.Add(newBlock); //TODO: add Add to lightstore functions + lightStore.Add(newBlock); return (lightStore, OK); } From 05bf5aa9e4947f3d15f82bf0a3bc2942de3355e0 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Tue, 29 Sep 2020 16:32:22 +0200 Subject: [PATCH 15/15] Update rust-spec/lightclient/supervisor/supervisor_001_draft.md --- rust-spec/lightclient/supervisor/supervisor_001_draft.md | 1 - 1 file changed, 1 deletion(-) diff --git a/rust-spec/lightclient/supervisor/supervisor_001_draft.md b/rust-spec/lightclient/supervisor/supervisor_001_draft.md index cd8091b9..cb545bce 100644 --- a/rust-spec/lightclient/supervisor/supervisor_001_draft.md +++ b/rust-spec/lightclient/supervisor/supervisor_001_draft.md @@ -577,7 +577,6 @@ func VerifyAndDetect (lightStore LightStore, targetHeight Height) // No cross-check needed. We trust hashes. Therefore, we // directly return the result return Backwards(peerList.primary(), lightStore.lowest, targetHeight) - // TODO: define lightStore.lowest } else { // Forward verification + detection