From ec8af314cce85fc0f4bad16086187314b859c61a Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 22 Oct 2020 14:26:56 +0200 Subject: [PATCH] spec: update light client verification to match supervisor (#171) * VDD renaming of verification spec + links fixed * latest() * backwards * added TODOs * link in old file to new name * better text * revision done. needs one more round of reading * renamed constants in 001 according to TLA+ and impl * ready for PR * forgot linting * Update rust-spec/lightclient/verification/verification_002_draft.md * Update rust-spec/lightclient/verification/verification_002_draft.md * added lightstore function needed for supervisor * added lightstore functions for supervisor * ident * Update rust-spec/lightclient/verification/verification_002_draft.md --- rust-spec/lightclient/README.md | 6 +- .../verification/Lightclient_A_1.tla | 2 +- .../lightclient/verification/verification.md | 1166 +--------------- .../verification_001_published.md | 1181 +++++++++++++++++ .../verification/verification_002_draft.md | 1061 +++++++++++++++ 5 files changed, 2250 insertions(+), 1166 deletions(-) create mode 100644 rust-spec/lightclient/verification/verification_001_published.md create mode 100644 rust-spec/lightclient/verification/verification_002_draft.md diff --git a/rust-spec/lightclient/README.md b/rust-spec/lightclient/README.md index 1958dc007..4f30ed5db 100644 --- a/rust-spec/lightclient/README.md +++ b/rust-spec/lightclient/README.md @@ -18,10 +18,10 @@ The light client is decomposed into three components: ## Commit Verification -The [English specification](verification/verification.md) describes the light client +The [English specification](verification/verification_001_published.md) describes the light client commit verification problem in terms of the temporal properties -[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md#lcv-dist-safe1) and -[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md#lcv-dist-live1). +[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification_001_published.md#lcv-dist-safe1) and +[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification_001_published.md#lcv-dist-live1). Commit verification is assumed to operate within the Tendermint Failure Model, where +2/3 of validators are correct for some time period and validator sets can change arbitrarily at each height. diff --git a/rust-spec/lightclient/verification/Lightclient_A_1.tla b/rust-spec/lightclient/verification/Lightclient_A_1.tla index 2be9b8788..70e6caf00 100644 --- a/rust-spec/lightclient/verification/Lightclient_A_1.tla +++ b/rust-spec/lightclient/verification/Lightclient_A_1.tla @@ -2,7 +2,7 @@ (** * A state-machine specification of the lite client, following the English spec: * - * https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md + * ./verification_001_published.md *) EXTENDS Integers, FiniteSets diff --git a/rust-spec/lightclient/verification/verification.md b/rust-spec/lightclient/verification/verification.md index f9ccc2160..09226ab64 100644 --- a/rust-spec/lightclient/verification/verification.md +++ b/rust-spec/lightclient/verification/verification.md @@ -1,1162 +1,4 @@ -# Light Client Verification - -The light client implements a read operation of a -[header][TMBC-HEADER-link] from the [blockchain][TMBC-SEQ-link], by -communicating with full nodes. 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*. The fault-tolerant read -operation is designed for this security model. - -The challenge addressed here is that the light client might have a -block of height *h1* and needs to read the block of height *h2* -greater than *h1*. Checking all headers of heights from *h1* to *h2* -might be too costly (e.g., in terms of energy for mobile devices). -This specification tries to reduce the number of intermediate blocks -that need to be checked, by exploiting the guarantees provided by the -[security model][TMBC-FM-2THIRDS-link]. - -# Status - -This document is thoroughly reviewed, and the protocol has been -formalized in TLA+ and model checked. - -## Issues that need to be addressed - -As it is part of the larger light node, its data structures and -functions interact with the fork dectection functionality of the light -client. As a result of the work on -[Pull Request 479](https://github.com/informalsystems/tendermint-rs/pull/479) we -established the need for an update in the data structures in [Issue 499](https://github.com/informalsystems/tendermint-rs/issues/499). This -will not change the verification logic, but it will record information -about verification that can be used in fork detection (in particular -in computing more efficiently the proof of fork). - -# Outline - -- [Part I](#part-i---tendermint-blockchain): Introduction of - relevant terms of the Tendermint -blockchain. - -- [Part II](#part-ii---sequential-definition-of-the-verification-problem): Introduction -of the problem addressed by the Lightclient Verification protocol. - - [Verification Informal Problem - statement](#Verification-Informal-Problem-statement): For the general - audience, that is, engineers who want to get an overview over what - the component is doing from a bird's eye view. - - [Sequential Problem statement](#Sequential-Problem-statement): - Provides a mathematical definition of the problem statement in - its sequential form, that is, ignoring the distributed aspect of - the implementation of the blockchain. - -- [Part III](#part-iii---light-client-as-distributed-system): Distributed - aspects of the light client, system assumptions and temporal - logic specifications. - - - [Incentives](#incentives): how faulty full nodes may benefit from - misbehaving and how correct full nodes benefit from cooperating. - - - [Computational Model](#Computational-Model): - timing and correctness assumptions. - - - [Distributed Problem Statement](#Distributed-Problem-Statement): - temporal properties that formalize safety and liveness - properties in the distributed setting. - -- [Part IV](#part-iv---light-client-verification-protocol): - Specification of the protocols. - - - [Definitions](#Definitions): Describes inputs, outputs, - variables used by the protocol, auxiliary functions - - - [Core Verification](#core-verification): gives an outline of the solution, - and details of the functions used (with preconditions, - postconditions, error conditions). - - - [Liveness Scenarios](#liveness-scenarios): when the light - client makes progress depends heavily on the changes in the - validator sets of the blockchain. We discuss some typical scenarios. - -- [Part V](#part-v---supporting-the-ibc-relayer): The above parts - focus on a common case where the last verified block has height *h1* - and the - requested height *h2* satisfies *h2 > h1*. For IBC, there are - scenarios where this might not be the case. In this part, we provide - some preliminaries for supporting this. As not all details of the - IBC requirements are clear by now, we do not provide a complete - specification at this point. We mark with "Open Question" points - that need to be addressed in order to finalize this specification. - It should be noted that the technically - most challenging case is the one specified in Part IV. - -In this document we quite extensively use tags in order to be able to -reference assumptions, invariants, etc. in future communication. In -these tags we frequently use the following short forms: - -- TMBC: Tendermint blockchain -- SEQ: for sequential specifications -- LCV: Lightclient Verification -- LIVE: liveness -- SAFE: safety -- FUNC: function -- INV: invariant -- A: assumption - -# Part I - Tendermint Blockchain - -## Header Fields necessary for the Light Client - -#### **[TMBC-HEADER.1]** - -A set of blockchain transactions is stored in a data structure called -*block*, which contains a field called *header*. (The data structure -*block* is defined [here][block]). As the header contains hashes to -the relevant fields of the block, for the purpose of this -specification, we will assume that the blockchain is a list of -headers, rather than a list of blocks. - -#### **[TMBC-HASH-UNIQUENESS.1]** - -We assume that every hash in the header identifies the data it hashes. -Therefore, in this specification, we do not distinguish between hashes and the -data they represent. - -#### **[TMBC-HEADER-FIELDS.1]** - -A header contains the following fields: - -- `Height`: non-negative integer -- `Time`: time (integer) -- `LastBlockID`: Hashvalue -- `LastCommit` DomainCommit -- `Validators`: DomainVal -- `NextValidators`: DomainVal -- `Data`: DomainTX -- `AppState`: DomainApp -- `LastResults`: DomainRes - -#### **[TMBC-SEQ.1]** - -The Tendermint blockchain is a list *chain* of headers. - -#### **[TMBC-VALIDATOR-PAIR.1]** - -Given a full node, a -*validator pair* is a pair *(peerID, voting_power)*, where - -- *peerID* is the PeerID (public key) of a full node, -- *voting_power* is an integer (representing the full node's - voting power in a certain consensus instance). - -> In the Golang implementation the data type for *validator -pair* is called `Validator` - -#### **[TMBC-VALIDATOR-SET.1]** - -A *validator set* is a set of validator pairs. For a validator set -*vs*, we write *TotalVotingPower(vs)* for the sum of the voting powers -of its validator pairs. - -#### **[TMBC-VOTE.1]** - -A *vote* contains a `prevote` or `precommit` message sent and signed by -a validator node during the execution of [consensus][arXiv]. Each -message contains the following fields - -- `Type`: prevote or precommit -- `Height`: positive integer -- `Round` a positive integer -- `BlockID` a Hashvalue of a block (not necessarily a block of the chain) - -#### **[TMBC-COMMIT.1]** - -A commit is a set of `precommit` message. - -## Tendermint Failure Model - -#### **[TMBC-AUTH-BYZ.1]** - -We assume the authenticated Byzantine fault model in which no node (faulty or -correct) may break digital signatures, but otherwise, no additional -assumption is made about the internal behavior of faulty -nodes. That is, faulty nodes are only limited in that they cannot forge -messages. - -#### **[TMBC-TIME-PARAMS.1]** - -A Tendermint blockchain has the following configuration parameters: - -- *unbondingPeriod*: a time duration. -- *trustingPeriod*: a time duration smaller than *unbondingPeriod*. - -#### **[TMBC-CORRECT.1]** - -We define a predicate *correctUntil(n, t)*, where *n* is a node and *t* is a -time point. -The predicate *correctUntil(n, t)* is true if and only if the node *n* -follows all the protocols (at least) until time *t*. - -#### **[TMBC-FM-2THIRDS.1]** - -If a block *h* is in the chain, -then there exists a subset *CorrV* -of *h.NextValidators*, such that: - -- *TotalVotingPower(CorrV) > 2/3 - TotalVotingPower(h.NextValidators)*; cf. [TMBC-VALIDATOR-SET.1] -- For every validator pair *(n,p)* in *CorrV*, it holds *correctUntil(n, - h.Time + trustingPeriod)*; cf. [TMBC-CORRECT.1] - -> The definition of correct -> [**[TMBC-CORRECT.1]**][TMBC-CORRECT-link] refers to realtime, while it -> is used here with *Time* and *trustingPeriod*, which are "hardware -> times". We do not make a distinction here. - -#### **[TMBC-CORR-FULL.1]** - -Every correct full node locally stores a prefix of the -current list of headers from [**[TMBC-SEQ.1]**][TMBC-SEQ-link]. - -## What the Light Client Checks - -> From [TMBC-FM-2THIRDS.1] we directly derive the following observation: - -#### **[TMBC-VAL-CONTAINS-CORR.1]** - -Given a (trusted) block *tb* of the blockchain, a given set of full nodes -*N* contains a correct node at a real-time *t*, if - -- *t - trustingPeriod < tb.Time < t* -- the voting power in tb.NextValidators of nodes in *N* is more - than 1/3 of *TotalVotingPower(tb.NextValidators)* - -> The following describes how a commit for a given block *b* must look -> like. - -#### **[TMBC-SOUND-DISTR-POSS-COMMIT.1]** - -For a block *b*, each element *pc* of *PossibleCommit(b)* satisfies: - -- *pc* contains only votes (cf. [TMBC-VOTE.1]) - by validators from *b.Validators* -- the sum of the voting powers in *pc* is greater than 2/3 - *TotalVotingPower(b.Validators)* -- and there is an *r* such that each vote *v* in *pc* satisfies - - v.Type = precommit - - v.Height = b.Height - - v.Round = r - - v.blockID = hash(b) - -> The following property comes from the validity of the [consensus][arXiv]: A -> correct validator node only sends `prevote` or `precommit`, if -> `BlockID` of the new (to-be-decided) block is equal to the hash of -> the last block. - -#### **[TMBC-VAL-COMMIT.1]** - -If for a block *b*, a commit *c* - -- contains at least one validator pair *(v,p)* such that *v* is a - **correct** validator node, and -- is contained in *PossibleCommit(b)* - -then the block *b* is on the blockchain. - -## Context of this document - -In this document we specify the light client verification component, -called *Core Verification*. The *Core Verification* communicates with -a full node. As full nodes may be faulty, it cannot trust the -received information, but the light client has to check whether the -header it receives coincides with the one generated by Tendermint -consensus. - -The two - properties [[TMBC-VAL-CONTAINS-CORR.1]][TMBC-VAL-CONTAINS-CORR-link] and -[[TMBC-VAL-COMMIT]][TMBC-VAL-COMMIT-link] formalize the checks done - by this specification: -Given a trusted block *tb* and an untrusted block *ub* with a commit *cub*, -one has to check that *cub* is in *PossibleCommit(ub)*, and that *cub* -contains a correct node using *tb*. - -# Part II - Sequential Definition of the Verification Problem - -## Verification Informal Problem statement - -Given a height *targetHeight* as an input, the *Verifier* eventually -stores a header *h* of height *targetHeight* locally. This header *h* -is generated by the Tendermint [blockchain][block]. In -particular, a header that was not generated by the blockchain should -never be stored. - -## Sequential Problem statement - -#### **[LCV-SEQ-LIVE.1]** - -The *Verifier* gets as input a height *targetHeight*, and eventually stores the -header of height *targetHeight* of the blockchain. - -#### **[LCV-SEQ-SAFE.1]** - -The *Verifier* never stores a header which is not in the blockchain. - -# Part III - Light Client as Distributed System - -## Incentives - -Faulty full nodes may benefit from lying to the light client, by making the -light client accept a block that deviates (e.g., contains additional -transactions) from the one generated by Tendermint consensus. -Users using the light client might be harmed by accepting a forged header. - -The [fork detector][fork-detector] of the light client may help the -correct full nodes to understand whether their header is a good one. -Hence, in combination with the light client detector, the correct full -nodes have the incentive to respond. We can thus base liveness -arguments on the assumption that correct full nodes reliably talk to -the light client. - -## Computational Model - -#### **[LCV-A-PEER.1]** - -The verifier communicates with a full node called *primary*. No assumption is made about the full node (it may be correct or faulty). - -#### **[LCV-A-COMM.1]** - -Communication between the light client 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 processes 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. - -#### **[LCV-A-TFM.1]** - -The Tendermint blockchain satisfies the Tendermint failure model [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. - -#### **[LCV-A-VAL.1]** - -The system satisfies [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] and -[**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. Thus, there is a -blockchain that satisfies the soundness requirements (that is, the -validation rules in [[block]]). - -## Distributed Problem Statement - -### Two Kinds of Termination - -We do not assume that *primary* is correct. Under this assumption no -protocol can guarantee the combination of the sequential -properties. Thus, in the (unreliable) distributed setting, we consider -two kinds of termination (successful and failure) and we will specify -below under what (favorable) conditions *Core Verification* ensures to -terminate successfully, and satisfy the requirements of the sequential -problem statement: - -#### **[LCV-DIST-TERM.1]** - -*Core Verification* either *terminates -successfully* or it *terminates with failure*. - -### Design choices - -#### **[LCV-DIST-STORE.1]** - -*Core Verification* has a local data structure called *LightStore* that -contains light blocks (that contain a header). For each light block we -record whether it is verified. - -#### **[LCV-DIST-PRIMARY.1]** - -*Core Verification* has a local variable *primary* that contains the PeerID of a full node. - -#### **[LCV-DIST-INIT.1]** - -*LightStore* is initialized with a header *trustedHeader* that was correctly -generated by the Tendermint consensus. We say *trustedHeader* is verified. - -### Temporal Properties - -#### **[LCV-DIST-SAFE.1]** - -It is always the case that every verified header in *LightStore* was -generated by an instance of Tendermint consensus. - -#### **[LCV-DIST-LIVE.1]** - -From time to time, a new instance of *Core Verification* is called with a -height *targetHeight* greater than the height of any header in *LightStore*. -Each instance must eventually terminate. - -- If - - the *primary* is correct (and locally has the block of - *targetHeight*), and - - *LightStore* always contains a verified header whose age is less than the - trusting period, - then *Core Verification* adds a verified header *hd* with height - *targetHeight* to *LightStore* and it **terminates successfully** - -> These definitions imply that if the primary is faulty, a header may or -> may not be added to *LightStore*. In any case, -> [**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) must hold. -> The invariant [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) and the liveness -> requirement [**[LCV-DIST-LIVE.1]**](#lcv-dist-life) -> allow that verified headers are added to *LightStore* whose -> height was not passed -> to the verifier (e.g., intermediate headers used in bisection; see below). -> Note that for liveness, initially having a *trustedHeader* within -> the *trustinPeriod* is not sufficient. However, as this -> specification will leave some freedom with respect to the strategy -> in which order to download intermediate headers, we do not give a -> more precise liveness specification here. After giving the -> specification of the protocol, we will discuss some liveness -> scenarios [below](#liveness-scenarios). - -### Solving the sequential specification - -This specification provides a partial solution to the sequential specification. -The *Verifier* solves the invariant of the sequential part - -[**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) => [**[LCV-SEQ-SAFE.1]**](#lcv-seq-inv) - -In the case the primary is correct, and there is a recent header in *LightStore*, the verifier satisfies the liveness requirements. - -⋀ *primary is correct* -⋀ always ∃ verified header in LightStore. *header.Time* > *now* - *trustingPeriod* -⋀ [**[LCV-A-Comm.1]**](#lcv-a-comm) ⋀ ( - ( [**[TMBC-CorrFull.1]**][TMBC-CorrFull-link] ⋀ - [**[LCV-DIST-LIVE.1]**](#lcv-vc-live) ) - ⟹ [**[LCV-SEQ-LIVE.1]**](#lcv-seq-live) -) - -# Part IV - Light Client Verification Protocol - -We provide a specification for Light Client Verification. The local -code for verification is presented by a sequential function -`VerifyToTarget` to highlight the control flow of this functionality. -We note that if a different concurrency model is considered for -an implementation, the sequential flow of the function may be -implemented with mutexes, etc. However, the light client verification -is partitioned into three blocks that can be implemented and tested -independently: - -- `FetchLightBlock` is called to download a light block (header) of a - given height from a peer. -- `ValidAndVerified` is a local code that checks the header. -- `Schedule` decides which height to try to verify next. We keep this - underspecified as different implementations (currently in Goland and - Rust) may implement different optimizations here. We just provide - necessary conditions on how the height may evolve. - - - - -## Definitions - -### Data Types - -The core data structure of the protocol is the LightBlock. - -#### **[LCV-DATA-LIGHTBLOCK.1]** - -```go -type LightBlock struct { - Header Header - Commit Commit - Validators ValidatorSet - NextValidators ValidatorSet - Provider PeerID -} -``` - -#### **[LCV-DATA-LIGHTSTORE.1]** - -LightBlocks are stored in a structure which stores all LightBlock from -initialization or received from peers. - -```go -type LightStore struct { - ... -} - -``` - -Each LightBlock is in one of the following states: - -```go -type VerifiedState int - -const ( - StateUnverified = iota + 1 - StateVerified - StateFailed - StateTrusted -) -``` - -> Only the detector module sets a lightBlock state to `StateTrusted` -> and only if it was `StateVerified` before. - -The LightStore exposes the following functions to query stored LightBlocks. - -```go -func (ls LightStore) Get(height Height) (LightBlock, bool) -``` - -- Expected postcondition - - returns a LightBlock at a given height or false in the second argument if - the LightStore does not contain the specified LightBlock. - -```go -func (ls LightStore) LatestVerified() LightBlock -``` - -- Expected postcondition - - returns the highest light block whose state is `StateVerified` - or `StateTrusted` - -#### **[LCV-FUNC-UPDATE.1]** - -```go -func (ls LightStore) Update(lightBlock LightBlock, verfiedState VerifiedState) -``` - -- Expected postcondition - - The state of the LightBlock is set to *verifiedState*. - -> The following function is used only in the detector specification -> listed here for completeness. - -```go -func (ls LightStore) LatestTrusted() LightBlock -``` - -- Expected postcondition - - returns the highest light block that has been verified and - checked by the detector. - -### Inputs - -- *lightStore*: stores light blocks that have been downloaded and that - passed verification. Initially it contains a light block with - *trustedHeader*. -- *primary*: peerID -- *targetHeight*: the height of the needed header - -### Configuration Parameters - -- *trustThreshold*: a float. Can be used if correctness should not be based on more voting power and 1/3. -- *trustingPeriod*: a time duration [**[TMBC-TIME_PARAMS.1]**][TMBC-TIME_PARAMS-link]. -- *clockDrift*: a time duration. Correction parameter dealing with only approximately synchronized clocks. - -### Variables - -- *nextHeight*: initially *targetHeight* - > *nextHeight* should be thought of the "height of the next header we need - > to download and verify" - -### Assumptions - -#### **[LCV-A-INIT.1]** - -- *trustedHeader* is from the blockchain - -- *targetHeight > LightStore.LatestVerified.Header.Height* - -### Invariants - -#### **[LCV-INV-TP.1]** - -It is always the case that *LightStore.LatestTrusted.Header.Time > now - trustingPeriod*. - -> If the invariant is violated, the light client does not have a -> header it can trust. A trusted header must be obtained externally, -> its trust can only be based on social consensus. - -### Used Remote Functions - -We use the functions `commit` and `validators` that are provided -by the [RPC client for Tendermint][RPC]. - -```go -func Commit(height int64) (SignedHeader, error) -``` - -- Implementation remark - - RPC to full node *n* - - JSON sent: - -```javascript -// POST /commit -{ - "jsonrpc": "2.0", - "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request - "method": "commit", - "params": { - "height": 1234 - } -} -``` - -- Expected precondition - - header of `height` exists on blockchain -- Expected postcondition - - if *n* is correct: Returns the signed header of height `height` - from the blockchain if communication is timely (no timeout) - - if *n* is faulty: Returns a signed header with arbitrary content -- Error condition - - if *n* is correct: precondition violated or timeout - - if *n* is faulty: arbitrary error - ----- - -```go -func Validators(height int64) (ValidatorSet, error) -``` - -- Implementation remark - - RPC to full node *n* - - JSON sent: - -```javascript -// POST /validators -{ - "jsonrpc": "2.0", - "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request - "method": "validators", - "params": { - "height": 1234 - } -} -``` - -- Expected precondition - - header of `height` exists on blockchain -- Expected postcondition - - if *n* is correct: Returns the validator set of height `height` - from the blockchain if communication is timely (no timeout) - - if *n* is faulty: Returns arbitrary validator set -- Error condition - - if *n* is correct: precondition violated or timeout - - if *n* is faulty: arbitrary error - ----- - -### Communicating Function - -#### **[LCV-FUNC-FETCH.1]** - - ```go -func FetchLightBlock(peer PeerID, height Height) LightBlock -``` - -- Implementation remark - - RPC to peer at *PeerID* - - calls `Commit` for *height* and `Validators` for *height* and *height+1* -- Expected precondition - - `height` is less than or equal to height of the peer **[LCV-IO-PRE-HEIGHT.1]** -- Expected postcondition: - - if *node* is correct: - - Returns the LightBlock *lb* of height `height` - that is consistent with the blockchain - - *lb.provider = peer* **[LCV-IO-POST-PROVIDER.1]** - - *lb.Header* is a header consistent with the blockchain - - *lb.Validators* is the validator set of the blockchain at height *nextHeight* - - *lb.NextValidators* is the validator set of the blockchain at height *nextHeight + 1* - - if *node* is faulty: Returns a LightBlock with arbitrary content - [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] -- Error condition - - if *n* is correct: precondition violated - - if *n* is faulty: arbitrary error - - if *lb.provider != peer* - - times out after 2 Delta (by assumption *n* is faulty) - ----- - -## Core Verification - -### Outline - -The `VerifyToTarget` is the main function and uses the following functions. - -- `FetchLightBlock` is called to download the next light block. It is - the only function that communicates with other nodes -- `ValidAndVerified` checks whether header is valid and checks if a - new lightBlock should be trusted - based on a previously verified lightBlock. -- `Schedule` decides which height to try to verify next - -In the following description of `VerifyToTarget` we do not deal with error -handling. If any of the above function returns an error, VerifyToTarget just -passes the error on. - -#### **[LCV-FUNC-MAIN.1]** - -```go -func VerifyToTarget(primary PeerID, lightStore LightStore, - targetHeight Height) (LightStore, Result) { - - nextHeight := targetHeight - - for lightStore.LatestVerified.height < targetHeight { - - // Get next LightBlock for verification - current, found := lightStore.Get(nextHeight) - if !found { - current = FetchLightBlock(primary, nextHeight) - lightStore.Update(current, StateUnverified) - } - - // Verify - verdict = ValidAndVerified(lightStore.LatestVerified, current) - - // Decide whether/how to continue - if verdict == OK { - lightStore.Update(current, StateVerified) - } - else if verdict == CANNOT_VERIFY { - // do nothing - // the light block current passed validation, but the validator - // set is too different to verify it. We keep the state of - // current at StateUnverified. For a later iteration, Schedule - // might decide to try verification of that light block again. - } - else { - // verdict is some error code - lightStore.Update(current, StateFailed) - // possibly remove all LightBlocks from primary - return (lightStore, ResultFailure) - } - nextHeight = Schedule(lightStore, nextHeight, targetHeight) - } - return (lightStore, ResultSuccess) -} -``` - -- Expected precondition - - *lightStore* contains a LightBlock within the *trustingPeriod* **[LCV-PRE-TP.1]** - - *targetHeight* is greater than the height of all the LightBlocks in *lightStore* -- Expected postcondition: - - returns *lightStore* that contains a LightBlock that corresponds to a block - of the blockchain of height *targetHeight* - (that is, the LightBlock has been added to *lightStore*) **[LCV-POST-LS.1]** -- Error conditions - - if the precondition is violated - - if `ValidAndVerified` or `FetchLightBlock` report an error - - if [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) is violated - -### Details of the Functions - -#### **[LCV-FUNC-VALID.1]** - -```go -func ValidAndVerified(trusted LightBlock, untrusted LightBlock) Result -``` - -- Expected precondition: - - *untrusted* is valid, that is, satisfies the soundness [checks][block] - - *untrusted* is **well-formed**, that is, - - *untrusted.Header.Time < now + clockDrift* - - *untrusted.Validators = hash(untrusted.Header.Validators)* - - *untrusted.NextValidators = hash(untrusted.Header.NextValidators)* - - *trusted.Header.Time > now - trustingPeriod* - - *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 - - the `Height` and `Time` of `trusted` are smaller than the Height and - `Time` of `untrusted`, respectively - - the *untrusted.Header* is well-formed (passes the tests from - [[block]]), and in particular - - if the untrusted header `unstrusted.Header` is the immediate - successor of `trusted.Header`, then it holds that - - *trusted.Header.NextValidators = - untrusted.Header.Validators*, and - moreover, - - *untrusted.Header.Commit* - - contains signatures by more than two-thirds of the validators - - contains no signature from nodes that are not in *trusted.Header.NextValidators* -- Expected postcondition: - - Returns `OK`: - - if *untrusted* is the immediate successor of *trusted*, or otherwise, - - if the signatures of a set of validators that have more than - *max(1/3,trustThreshold)* of voting power in - *trusted.Nextvalidators* is contained in - *untrusted.Commit* (that is, header passes the tests - [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] - and [**[TMBC-VAL-COMMIT.1]**][TMBC-VAL-COMMIT-link]) - - Returns `CANNOT_VERIFY` if: - - *untrusted* is *not* the immediate successor of - *trusted* - and the *max(1/3,trustThreshold)* threshold is not reached - (that is, if - [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] - fails and header is does not violate the soundness - checks [[block]]). -- Error condition: - - if precondition violated - ----- - -#### **[LCV-FUNC-SCHEDULE.1]** - -```go -func Schedule(lightStore, nextHeight, targetHeight) Height -``` - -- Implementation remark: If picks the next height to be verified. - We keep the precise choice of the next header under-specified. It is - subject to performance optimizations that do not influence the correctness -- Expected postcondition: **[LCV-SCHEDULE-POST.1]** - Return *H* s.t. - 1. if *lightStore.LatestVerified.Height = nextHeight* and - *lightStore.LatestVerified < targetHeight* then - *nextHeight < H <= targetHeight* - 2. if *lightStore.LatestVerified.Height < nextHeight* and - *lightStore.LatestVerified.Height < targetHeight* then - *lightStore.LatestVerified.Height < H < nextHeight* - 3. if *lightStore.LatestVerified.Height = targetHeight* then - *H = targetHeight* - -> Case i. captures the case where the light block at height *nextHeight* -> has been verified, and we can choose a height closer to the *targetHeight*. -> As we get the *lightStore* as parameter, the choice of the next height can -> depend on the *lightStore*, e.g., we can pick a height for which we have -> already downloaded a light block. -> In Case ii. the header of *nextHeight* could not be verified, and we need to pick a smaller height. -> In Case iii. is a special case when we have verified the *targetHeight*. - -### Solving the distributed specification - -*trustedStore* is implemented by the light blocks in lightStore that -have the state *StateVerified*. - -#### Argument for [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) - -- `ValidAndVerified` implements the soundness checks and the checks - [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] and - [**[TMBC-VAL-COMMIT.1]**][TMBC-VAL-COMMIT-link] under - the assumption [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link] -- Only if `ValidAndVerified` returns with `OK`, the state of a light block is - set to *StateVerified*. - -#### Argument for [**[LCV-DIST-LIVE.1]**](#lcv-dist-life) - -- If *primary* is correct, - - `FetchLightBlock` will always return a light block consistent - with the blockchain - - `ValidAndVerified` either verifies the header using the trusting - period or falls back to sequential - verification - - If [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) holds, eventually every - header will be verified and core verification **terminates successfully**. - - successful termination depends on the age of *lightStore.LatestVerified* - (for instance, initially on the age of *trustedHeader*) and the - changes of the validator sets on the blockchain. - We will give some examples [below](#liveness-scenarios). -- If *primary* is faulty, - - it either provides headers that pass all the tests, and we - return with the header - - it provides one header that fails a test, core verification - **terminates with failure**. - - it times out and core verification - **terminates with failure**. - -## Liveness Scenarios - -The liveness argument above assumes [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) - -which requires that there is a header that does not expire before the -target height is reached. Here we discuss scenarios to ensure this. - -Let *startHeader* be *LightStore.LatestVerified* when core -verification is called (*trustedHeader*) and *startTime* be the time -core verification is invoked. - -In order to ensure liveness, *LightStore* always needs to contain a -verified (or initially trusted) header whose time is within the -trusting period. To ensure this, core verification needs to add new -headers to *LightStore* and verify them, before all headers in -*LightStore* expire. - -#### Many changes in validator set - - Let's consider `Schedule` implements - bisection, that is, it halves the distance. - Assume the case where the validator set changes completely in each -block. Then the - method in this specification needs to -sequentially verify all headers. That is, for - -- *W = log_2 (targetHeight - startHeader.Height)*, - -*W* headers need to be downloaded and checked before the -header of height *startHeader.Height + 1* is added to *LightStore*. - -- Let *Comp* - be the local computation time needed to check headers and signatures - for one header. -- Then we need in the worst case *Comp + 2 Delta* to download and - check one header. -- Then the first time a verified header could be added to *LightStore* is - startTime + W * (Comp + 2 Delta) -- [TP.1] However, it can only be added if we still have a header in - *LightStore*, - which is not - expired, that is only the case if - - startHeader.Time > startTime + WCG * (Comp + 2 Delta) - - trustingPeriod, - - that is, if core verification is started at - startTime < startHeader.Time + trustingPeriod - WCG * (Comp + 2 Delta) - -- one may then do an inductive argument from this point on, depending - on the implementation of `Schedule`. We may have to account for the - headers that are already - downloaded, but they are checked against the new *LightStore.LatestVerified*. - -> We observe that -> the worst case time it needs to verify the header of height -> *targetHeight* depends mainly on how frequent the validator set on the -> blockchain changes. That core verification terminates successfully -> crucially depends on the check [TP.1], that is, that the headers in -> *LightStore* do not expire in the time needed to download more -> headers, which depends on the creation time of the headers in -> *LightStore*. That is, termination of core verification is highly -> depending on the data stored in the blockchain. -> The current light client core verification protocol exploits that, in -> practice, changes in the validator set are rare. For instance, -> consider the following scenario. - -#### No change in validator set - -If on the blockchain the validator set of the block at height -*targetHeight* is equal to *startHeader.NextValidators*: - -- there is one round trip in `FetchLightBlock` to download the light - block - of height - *targetHeight*, and *Comp* to check it. -- as the validator sets are equal, `Verify` returns `OK`, if - *startHeader.Time > now - trustingPeriod*. -- that is, if *startTime < startHeader.Header.Time + trustingPeriod - - 2 Delta - Comp*, then core verification terminates successfully - -# Part V - Supporting the IBC Relayer - -The above specification focuses on the most common case, which also -constitutes the most challenging task: using the Tendermint [security -model][TMBC-FM-2THIRDS-link] to verify light blocks without -downloading all intermediate blocks. To focus on this challenge, above -we have restricted ourselves to the case where *targetHeight* is -greater than the height of any trusted header. This simplified -presentation of the algorithm as initially -`lightStore.LatestVerified()` is less than *targetHeight*, and in the -process of verification `lightStore.LatestVerified()` increases until -*targetHeight* is reached. - -For [IBC][ibc-rs] it might be that some "older" header is -needed, that is, *targetHeight < lightStore.LatestVerified()*. In this section we present a preliminary design, and we mark some -remaining open questions. -If *targetHeight < lightStore.LatestVerified()* our design separates -the following cases: - -- A previous instance of `VerifyToTarget` has already downloaded the - light block of *targetHeight*. There are two cases - - the light block has been verified - - the light block has not been verified yet -- No light block of *targetHeight* had been downloaded before. There - are two cases: - - there exists a verified light block of height less than *targetHeight* - - otherwise. In this case we need to do "backwards verification" - using the hash of the previous block in the `LastBlockID` field - of a header. - -**Open Question:** what are the security assumptions for backward -verification. Should we check that the light block we verify from -(and/or the checked light block) is within the trusting period? - -The design just presents the above case -distinction as a function, and defines some auxiliary functions in the -same way the protocol was presented in -[Part IV](#part-iv---light-client-verification-protocol). - -```go -func (ls LightStore) LatestPrevious(height Height) (LightBlock, bool) -``` - -- Expected postcondition - - returns a light block *lb* that satisfies: - - *lb* is in lightStore - - *lb* is verified and not expired - - *lb.Header.Height < height* - - for all *b* in lightStore s.t. *b* is verified and not expired it - holds *lb.Header.Height >= b.Header.Height* - - *false* in the second argument if - the LightStore does not contain such an *lb*. - -```go -func (ls LightStore) MinVerified() (LightBlock, bool) -``` - -- Expected postcondition - - returns a light block *lb* that satisfies: - - *lb* is in lightStore - - *lb* is verified **Open Question:** replace by trusted? - - *lb.Header.Height* is minimal in the lightStore - - **Open Question:** according to this, it might be expired (outside the - trusting period). This approach appears safe. Are there reasons we - should not do that? - - *false* in the second argument if - the LightStore does not contain such an *lb*. - -If a height that is smaller than the smallest height in the lightstore -is required, we check the hashes backwards. This is done with the -following function: - -#### **[LCV-FUNC-BACKWARDS.1]** - -```go -func Backwards (primary PeerID, lightStore LightStore, targetHeight Height) - (LightStore, Result) { - - lb,res = lightStore.MinVerified() - if res = false { - return (lightStore, ResultFailure) - } - - latest := lb.Header - for i := lb.Header.height - 1; i >= targetHeight; i-- { - // here we download height-by-height. We might first download all - // headers down to targetHeight and then check them. - current := FetchLightBlock(primary,i) - if (hash(current) != latest.Header.LastBlockId) { - return (lightStore, ResultFailure) - } - else { - lightStore.Update(current, StateVerified) - // **Open Question:** Do we need a new state type for - // backwards verified light blocks? - } - latest = current - } - return (lightStore, ResultSuccess) -} -``` - -The following function just decided based on the required height which -method should be used. - -#### **[LCV-FUNC-IBCMAIN.1]** - -```go -func Main (primary PeerID, lightStore LightStore, targetHeight Height) - (LightStore, Result) { - - b1, r1 = lightStore.Get(targetHeight) - if r1 = true and b1.State = StateVerified { - // block already there - return (lightStore, ResultSuccess) - } - - if targetHeight > lightStore.LatestVerified.height { - // case of Part IV - return VerifyToTarget(primary, lightStore, targetHeight) - } - else { - b2, r2 = lightStore.LatestPrevious(targetHeight); - if r2 = true { - // make auxiliary lightStore auxLS to call VerifyToTarget. - // VerifyToTarget uses LatestVerified of the given lightStore - // For that we need: - // auxLS.LatestVerified = lightStore.LatestPrevious(targetHeight) - auxLS.Init; - auxLS.Update(b2,StateVerified); - if r1 = true { - // we need to verify a previously downloaded light block. - // we add it to the auxiliary store so that VerifyToTarget - // does not download it again - auxLS.Update(b1,b1.State); - } - auxLS, res2 = VerifyToTarget(primary, auxLS, targetHeight) - // move all lightblocks from auxLS to lightStore, - // maintain state - // we do that whether VerifyToTarget was successful or not - for i, s range auxLS { - lighStore.Update(s,s.State) - } - return (lightStore, res2) - } - else { - return Backwards(primary, lightStore, targetHeight) - } - } -} -``` - - - - - - - - - - - - - - - - - - - -# References - -[[block]] Specification of the block data structure. - -[[RPC]] RPC client for Tendermint - -[[fork-detector]] The specification of the light client fork detector. - -[[fullnode]] Specification of the full node API - -[[ibc-rs]] Rust implementation of IBC modules and relayer. - -[[lightclient]] The light client ADR [77d2651 on Dec 27, 2019]. - -[RPC]: https://docs.tendermint.com/master/rpc/ - -[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md - -[TMBC-HEADER-link]: #tmbc-header1 -[TMBC-SEQ-link]: #tmbc-seq1 -[TMBC-CorrFull-link]: #tmbc-corr-full1 -[TMBC-Auth-Byz-link]: #tmbc-auth-byz1 -[TMBC-TIME_PARAMS-link]: #tmbc-time-params1 -[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds1 -[TMBC-VAL-CONTAINS-CORR-link]: #tmbc-val-contains-corr1 -[TMBC-VAL-COMMIT-link]: #tmbc-val-commit1 -[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1 - -[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md -[fork-detector]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_001_reviewed.md - - -[ibc-rs]:https://github.com/informalsystems/ibc-rs - - - -[blockchain-validator-set]: https://github.com/tendermint/spec/blob/master/spec/blockchain/blockchain.md#data-structures -[fullnode-data-structures]: https://github.com/tendermint/spec/blob/master/spec/core/data_structures.md - - - -[arXiv]: https://arxiv.org/abs/1807.04938 +We changed the naming convention and versioning of specifications. +See [verification_001_published.md](./verification_001_published.md) +for the file that used to be called `verification.md`. There are also newer +versions of this specification in this directory. \ No newline at end of file diff --git a/rust-spec/lightclient/verification/verification_001_published.md b/rust-spec/lightclient/verification/verification_001_published.md new file mode 100644 index 000000000..05baedb3f --- /dev/null +++ b/rust-spec/lightclient/verification/verification_001_published.md @@ -0,0 +1,1181 @@ +# Light Client Verification + +The light client implements a read operation of a +[header][TMBC-HEADER-link] from the [blockchain][TMBC-SEQ-link], by +communicating with full nodes. 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*. The fault-tolerant read +operation is designed for this security model. + +The challenge addressed here is that the light client might have a +block of height *h1* and needs to read the block of height *h2* +greater than *h1*. Checking all headers of heights from *h1* to *h2* +might be too costly (e.g., in terms of energy for mobile devices). +This specification tries to reduce the number of intermediate blocks +that need to be checked, by exploiting the guarantees provided by the +[security model][TMBC-FM-2THIRDS-link]. + +# Status + +This document is thoroughly reviewed, and the protocol has been +formalized in TLA+ and model checked. + +## Issues that need to be addressed + +As it is part of the larger light node, its data structures and +functions interact with the fork dectection functionality of the light +client. As a result of the work on +[Pull Request 479](https://github.com/informalsystems/tendermint-rs/pull/479) we +established the need for an update in the data structures in [Issue 499](https://github.com/informalsystems/tendermint-rs/issues/499). This +will not change the verification logic, but it will record information +about verification that can be used in fork detection (in particular +in computing more efficiently the proof of fork). + +# Outline + +- [Part I](#part-i---tendermint-blockchain): Introduction of + relevant terms of the Tendermint +blockchain. + +- [Part II](#part-ii---sequential-definition-of-the-verification-problem): Introduction +of the problem addressed by the Lightclient Verification protocol. + - [Verification Informal Problem + statement](#Verification-Informal-Problem-statement): For the general + audience, that is, engineers who want to get an overview over what + the component is doing from a bird's eye view. + - [Sequential Problem statement](#Sequential-Problem-statement): + Provides a mathematical definition of the problem statement in + its sequential form, that is, ignoring the distributed aspect of + the implementation of the blockchain. + +- [Part III](#part-iii---light-client-as-distributed-system): Distributed + aspects of the light client, system assumptions and temporal + logic specifications. + + - [Incentives](#incentives): how faulty full nodes may benefit from + misbehaving and how correct full nodes benefit from cooperating. + + - [Computational Model](#Computational-Model): + timing and correctness assumptions. + + - [Distributed Problem Statement](#Distributed-Problem-Statement): + temporal properties that formalize safety and liveness + properties in the distributed setting. + +- [Part IV](#part-iv---light-client-verification-protocol): + Specification of the protocols. + + - [Definitions](#Definitions): Describes inputs, outputs, + variables used by the protocol, auxiliary functions + + - [Core Verification](#core-verification): gives an outline of the solution, + and details of the functions used (with preconditions, + postconditions, error conditions). + + - [Liveness Scenarios](#liveness-scenarios): when the light + client makes progress depends heavily on the changes in the + validator sets of the blockchain. We discuss some typical scenarios. + +- [Part V](#part-v---supporting-the-ibc-relayer): The above parts + focus on a common case where the last verified block has height *h1* + and the + requested height *h2* satisfies *h2 > h1*. For IBC, there are + scenarios where this might not be the case. In this part, we provide + some preliminaries for supporting this. As not all details of the + IBC requirements are clear by now, we do not provide a complete + specification at this point. We mark with "Open Question" points + that need to be addressed in order to finalize this specification. + It should be noted that the technically + most challenging case is the one specified in Part IV. + +In this document we quite extensively use tags in order to be able to +reference assumptions, invariants, etc. in future communication. In +these tags we frequently use the following short forms: + +- TMBC: Tendermint blockchain +- SEQ: for sequential specifications +- LCV: Lightclient Verification +- LIVE: liveness +- SAFE: safety +- FUNC: function +- INV: invariant +- A: assumption + +# Part I - Tendermint Blockchain + +## Header Fields necessary for the Light Client + +#### **[TMBC-HEADER.1]** + +A set of blockchain transactions is stored in a data structure called +*block*, which contains a field called *header*. (The data structure +*block* is defined [here][block]). As the header contains hashes to +the relevant fields of the block, for the purpose of this +specification, we will assume that the blockchain is a list of +headers, rather than a list of blocks. + +#### **[TMBC-HASH-UNIQUENESS.1]** + +We assume that every hash in the header identifies the data it hashes. +Therefore, in this specification, we do not distinguish between hashes and the +data they represent. + +#### **[TMBC-HEADER-FIELDS.1]** + +A header contains the following fields: + +- `Height`: non-negative integer +- `Time`: time (integer) +- `LastBlockID`: Hashvalue +- `LastCommit` DomainCommit +- `Validators`: DomainVal +- `NextValidators`: DomainVal +- `Data`: DomainTX +- `AppState`: DomainApp +- `LastResults`: DomainRes + +#### **[TMBC-SEQ.1]** + +The Tendermint blockchain is a list *chain* of headers. + +#### **[TMBC-VALIDATOR-PAIR.1]** + +Given a full node, a +*validator pair* is a pair *(peerID, voting_power)*, where + +- *peerID* is the PeerID (public key) of a full node, +- *voting_power* is an integer (representing the full node's + voting power in a certain consensus instance). + +> In the Golang implementation the data type for *validator +pair* is called `Validator` + +#### **[TMBC-VALIDATOR-SET.1]** + +A *validator set* is a set of validator pairs. For a validator set +*vs*, we write *TotalVotingPower(vs)* for the sum of the voting powers +of its validator pairs. + +#### **[TMBC-VOTE.1]** + +A *vote* contains a `prevote` or `precommit` message sent and signed by +a validator node during the execution of [consensus][arXiv]. Each +message contains the following fields + +- `Type`: prevote or precommit +- `Height`: positive integer +- `Round` a positive integer +- `BlockID` a Hashvalue of a block (not necessarily a block of the chain) + +#### **[TMBC-COMMIT.1]** + +A commit is a set of `precommit` message. + +## Tendermint Failure Model + +#### **[TMBC-AUTH-BYZ.1]** + +We assume the authenticated Byzantine fault model in which no node (faulty or +correct) may break digital signatures, but otherwise, no additional +assumption is made about the internal behavior of faulty +nodes. That is, faulty nodes are only limited in that they cannot forge +messages. + +#### **[TMBC-TIME-PARAMS.1]** + +A Tendermint blockchain has the following configuration parameters: + +- *unbondingPeriod*: a time duration. +- *trustingPeriod*: a time duration smaller than *unbondingPeriod*. + +#### **[TMBC-CORRECT.1]** + +We define a predicate *correctUntil(n, t)*, where *n* is a node and *t* is a +time point. +The predicate *correctUntil(n, t)* is true if and only if the node *n* +follows all the protocols (at least) until time *t*. + +#### **[TMBC-FM-2THIRDS.1]** + +If a block *h* is in the chain, +then there exists a subset *CorrV* +of *h.NextValidators*, such that: + +- *TotalVotingPower(CorrV) > 2/3 + TotalVotingPower(h.NextValidators)*; cf. [TMBC-VALIDATOR-SET.1] +- For every validator pair *(n,p)* in *CorrV*, it holds *correctUntil(n, + h.Time + trustingPeriod)*; cf. [TMBC-CORRECT.1] + +> The definition of correct +> [**[TMBC-CORRECT.1]**][TMBC-CORRECT-link] refers to realtime, while it +> is used here with *Time* and *trustingPeriod*, which are "hardware +> times". We do not make a distinction here. + +#### **[TMBC-CORR-FULL.1]** + +Every correct full node locally stores a prefix of the +current list of headers from [**[TMBC-SEQ.1]**][TMBC-SEQ-link]. + +## What the Light Client Checks + +> From [TMBC-FM-2THIRDS.1] we directly derive the following observation: + +#### **[TMBC-VAL-CONTAINS-CORR.1]** + +Given a (trusted) block *tb* of the blockchain, a given set of full nodes +*N* contains a correct node at a real-time *t*, if + +- *t - trustingPeriod < tb.Time < t* +- the voting power in tb.NextValidators of nodes in *N* is more + than 1/3 of *TotalVotingPower(tb.NextValidators)* + +> The following describes how a commit for a given block *b* must look +> like. + +#### **[TMBC-SOUND-DISTR-POSS-COMMIT.1]** + +For a block *b*, each element *pc* of *PossibleCommit(b)* satisfies: + +- *pc* contains only votes (cf. [TMBC-VOTE.1]) + by validators from *b.Validators* +- the sum of the voting powers in *pc* is greater than 2/3 + *TotalVotingPower(b.Validators)* +- and there is an *r* such that each vote *v* in *pc* satisfies + - v.Type = precommit + - v.Height = b.Height + - v.Round = r + - v.blockID = hash(b) + +> The following property comes from the validity of the [consensus][arXiv]: A +> correct validator node only sends `prevote` or `precommit`, if +> `BlockID` of the new (to-be-decided) block is equal to the hash of +> the last block. + +#### **[TMBC-VAL-COMMIT.1]** + +If for a block *b*, a commit *c* + +- contains at least one validator pair *(v,p)* such that *v* is a + **correct** validator node, and +- is contained in *PossibleCommit(b)* + +then the block *b* is on the blockchain. + +## Context of this document + +In this document we specify the light client verification component, +called *Core Verification*. The *Core Verification* communicates with +a full node. As full nodes may be faulty, it cannot trust the +received information, but the light client has to check whether the +header it receives coincides with the one generated by Tendermint +consensus. + +The two + properties [[TMBC-VAL-CONTAINS-CORR.1]][TMBC-VAL-CONTAINS-CORR-link] and +[[TMBC-VAL-COMMIT]][TMBC-VAL-COMMIT-link] formalize the checks done + by this specification: +Given a trusted block *tb* and an untrusted block *ub* with a commit *cub*, +one has to check that *cub* is in *PossibleCommit(ub)*, and that *cub* +contains a correct node using *tb*. + +# Part II - Sequential Definition of the Verification Problem + +## Verification Informal Problem statement + +Given a height *targetHeight* as an input, the *Verifier* eventually +stores a header *h* of height *targetHeight* locally. This header *h* +is generated by the Tendermint [blockchain][block]. In +particular, a header that was not generated by the blockchain should +never be stored. + +## Sequential Problem statement + +#### **[LCV-SEQ-LIVE.1]** + +The *Verifier* gets as input a height *targetHeight*, and eventually stores the +header of height *targetHeight* of the blockchain. + +#### **[LCV-SEQ-SAFE.1]** + +The *Verifier* never stores a header which is not in the blockchain. + +# Part III - Light Client as Distributed System + +## Incentives + +Faulty full nodes may benefit from lying to the light client, by making the +light client accept a block that deviates (e.g., contains additional +transactions) from the one generated by Tendermint consensus. +Users using the light client might be harmed by accepting a forged header. + +The [fork detector][fork-detector] of the light client may help the +correct full nodes to understand whether their header is a good one. +Hence, in combination with the light client detector, the correct full +nodes have the incentive to respond. We can thus base liveness +arguments on the assumption that correct full nodes reliably talk to +the light client. + +## Computational Model + +#### **[LCV-A-PEER.1]** + +The verifier communicates with a full node called *primary*. No assumption is made about the full node (it may be correct or faulty). + +#### **[LCV-A-COMM.1]** + +Communication between the light client 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 processes 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. + +#### **[LCV-A-TFM.1]** + +The Tendermint blockchain satisfies the Tendermint failure model [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. + +#### **[LCV-A-VAL.1]** + +The system satisfies [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] and +[**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. Thus, there is a +blockchain that satisfies the soundness requirements (that is, the +validation rules in [[block]]). + +## Distributed Problem Statement + +### Two Kinds of Termination + +We do not assume that *primary* is correct. Under this assumption no +protocol can guarantee the combination of the sequential +properties. Thus, in the (unreliable) distributed setting, we consider +two kinds of termination (successful and failure) and we will specify +below under what (favorable) conditions *Core Verification* ensures to +terminate successfully, and satisfy the requirements of the sequential +problem statement: + +#### **[LCV-DIST-TERM.1]** + +*Core Verification* either *terminates +successfully* or it *terminates with failure*. + +### Design choices + +#### **[LCV-DIST-STORE.1]** + +*Core Verification* has a local data structure called *LightStore* that +contains light blocks (that contain a header). For each light block we +record whether it is verified. + +#### **[LCV-DIST-PRIMARY.1]** + +*Core Verification* has a local variable *primary* that contains the PeerID of a full node. + +#### **[LCV-DIST-INIT.1]** + +*LightStore* is initialized with a header *trustedHeader* that was correctly +generated by the Tendermint consensus. We say *trustedHeader* is verified. + +### Temporal Properties + +#### **[LCV-DIST-SAFE.1]** + +It is always the case that every verified header in *LightStore* was +generated by an instance of Tendermint consensus. + +#### **[LCV-DIST-LIVE.1]** + +From time to time, a new instance of *Core Verification* is called with a +height *targetHeight* greater than the height of any header in *LightStore*. +Each instance must eventually terminate. + +- If + - the *primary* is correct (and locally has the block of + *targetHeight*), and + - *LightStore* always contains a verified header whose age is less than the + trusting period, + then *Core Verification* adds a verified header *hd* with height + *targetHeight* to *LightStore* and it **terminates successfully** + +> These definitions imply that if the primary is faulty, a header may or +> may not be added to *LightStore*. In any case, +> [**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) must hold. +> The invariant [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) and the liveness +> requirement [**[LCV-DIST-LIVE.1]**](#lcv-dist-life) +> allow that verified headers are added to *LightStore* whose +> height was not passed +> to the verifier (e.g., intermediate headers used in bisection; see below). +> Note that for liveness, initially having a *trustedHeader* within +> the *trustinPeriod* is not sufficient. However, as this +> specification will leave some freedom with respect to the strategy +> in which order to download intermediate headers, we do not give a +> more precise liveness specification here. After giving the +> specification of the protocol, we will discuss some liveness +> scenarios [below](#liveness-scenarios). + +### Solving the sequential specification + +This specification provides a partial solution to the sequential specification. +The *Verifier* solves the invariant of the sequential part + +[**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) => [**[LCV-SEQ-SAFE.1]**](#lcv-seq-inv) + +In the case the primary is correct, and there is a recent header in *LightStore*, the verifier satisfies the liveness requirements. + +⋀ *primary is correct* +⋀ always ∃ verified header in LightStore. *header.Time* > *now* - *trustingPeriod* +⋀ [**[LCV-A-Comm.1]**](#lcv-a-comm) ⋀ ( + ( [**[TMBC-CorrFull.1]**][TMBC-CorrFull-link] ⋀ + [**[LCV-DIST-LIVE.1]**](#lcv-vc-live) ) + ⟹ [**[LCV-SEQ-LIVE.1]**](#lcv-seq-live) +) + +# Part IV - Light Client Verification Protocol + +We provide a specification for Light Client Verification. The local +code for verification is presented by a sequential function +`VerifyToTarget` to highlight the control flow of this functionality. +We note that if a different concurrency model is considered for +an implementation, the sequential flow of the function may be +implemented with mutexes, etc. However, the light client verification +is partitioned into three blocks that can be implemented and tested +independently: + +- `FetchLightBlock` is called to download a light block (header) of a + given height from a peer. +- `ValidAndVerified` is a local code that checks the header. +- `Schedule` decides which height to try to verify next. We keep this + underspecified as different implementations (currently in Goland and + Rust) may implement different optimizations here. We just provide + necessary conditions on how the height may evolve. + + + + +## Definitions + +### Data Types + +The core data structure of the protocol is the LightBlock. + +#### **[LCV-DATA-LIGHTBLOCK.1]** + +```go +type LightBlock struct { + Header Header + Commit Commit + Validators ValidatorSet + NextValidators ValidatorSet + Provider PeerID +} +``` + +#### **[LCV-DATA-LIGHTSTORE.1]** + +LightBlocks are stored in a structure which stores all LightBlock from +initialization or received from peers. + +```go +type LightStore struct { + ... +} + +``` + +Each LightBlock is in one of the following states: + +```go +type VerifiedState int + +const ( + StateUnverified = iota + 1 + StateVerified + StateFailed + StateTrusted +) +``` + + +> Only the detector module sets a lightBlock state to `StateTrusted` +> and only if it was `StateVerified` before. + +The LightStore exposes the following functions to query stored LightBlocks. + +#### **[LCV-FUNC-GET.1]** + +```go +func (ls LightStore) Get(height Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a LightBlock at a given height or false in the second argument if + the LightStore does not contain the specified LightBlock. + +#### **[LCV-FUNC-LATEST-VERIF.1]** + +```go +func (ls LightStore) LatestVerified() LightBlock +``` + +- Expected postcondition + - returns the highest light block whose state is `StateVerified` + or `StateTrusted` + +#### **[LCV-FUNC-UPDATE.2]** + +```go +func (ls LightStore) Update(lightBlock LightBlock, + verfiedState VerifiedState + verifiedBy Height) +``` + +- Expected postcondition + - The state of the LightBlock is set to *verifiedState*. + - verifiedBy of the Lightblock is set to *Height* + +> The following function is used only in the detector specification +> listed here for completeness. + +#### **[LCV-FUNC-LATEST-TRUSTED.1]** + +```go +func (ls LightStore) LatestTrusted() LightBlock +``` + +- Expected postcondition + - returns the highest light block that has been verified and + checked by the detector. + +#### **[LCV-FUNC-FILTER.1]** + +```go +func (ls LightStore) FilterVerified() LightSTore +``` + +- Expected postcondition + - returns only the LightBlocks with state verified. + +### Inputs + +- *lightStore*: stores light blocks that have been downloaded and that + passed verification. Initially it contains a light block with + *trustedHeader*. +- *primary*: peerID +- *targetHeight*: the height of the needed header + +### Configuration Parameters + +- *trustThreshold*: a float. Can be used if correctness should not be based on more voting power and 1/3. +- *trustingPeriod*: a time duration [**[TMBC-TIME_PARAMS.1]**][TMBC-TIME_PARAMS-link]. +- *clockDrift*: a time duration. Correction parameter dealing with only approximately synchronized clocks. + +### Variables + +- *nextHeight*: initially *targetHeight* + > *nextHeight* should be thought of the "height of the next header we need + > to download and verify" + +### Assumptions + +#### **[LCV-A-INIT.1]** + +- *trustedHeader* is from the blockchain + +- *targetHeight > LightStore.LatestVerified.Header.Height* + +### Invariants + +#### **[LCV-INV-TP.1]** + +It is always the case that *LightStore.LatestTrusted.Header.Time > now - trustingPeriod*. + +> If the invariant is violated, the light client does not have a +> header it can trust. A trusted header must be obtained externally, +> its trust can only be based on social consensus. + +### Used Remote Functions + +We use the functions `commit` and `validators` that are provided +by the [RPC client for Tendermint][RPC]. + +```go +func Commit(height int64) (SignedHeader, error) +``` + +- Implementation remark + - RPC to full node *n* + - JSON sent: + +```javascript +// POST /commit +{ + "jsonrpc": "2.0", + "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request + "method": "commit", + "params": { + "height": 1234 + } +} +``` + +- Expected precondition + - header of `height` exists on blockchain +- Expected postcondition + - if *n* is correct: Returns the signed header of height `height` + from the blockchain if communication is timely (no timeout) + - if *n* is faulty: Returns a signed header with arbitrary content +- Error condition + - if *n* is correct: precondition violated or timeout + - if *n* is faulty: arbitrary error + +---- + +```go +func Validators(height int64) (ValidatorSet, error) +``` + +- Implementation remark + - RPC to full node *n* + - JSON sent: + +```javascript +// POST /validators +{ + "jsonrpc": "2.0", + "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request + "method": "validators", + "params": { + "height": 1234 + } +} +``` + +- Expected precondition + - header of `height` exists on blockchain +- Expected postcondition + - if *n* is correct: Returns the validator set of height `height` + from the blockchain if communication is timely (no timeout) + - if *n* is faulty: Returns arbitrary validator set +- Error condition + - if *n* is correct: precondition violated or timeout + - if *n* is faulty: arbitrary error + +---- + +### Communicating Function + +#### **[LCV-FUNC-FETCH.1]** + + ```go +func FetchLightBlock(peer PeerID, height Height) LightBlock +``` + +- Implementation remark + - RPC to peer at *PeerID* + - calls `Commit` for *height* and `Validators` for *height* and *height+1* +- Expected precondition + - `height` is less than or equal to height of the peer **[LCV-IO-PRE-HEIGHT.1]** +- Expected postcondition: + - if *node* is correct: + - Returns the LightBlock *lb* of height `height` + that is consistent with the blockchain + - *lb.provider = peer* **[LCV-IO-POST-PROVIDER.1]** + - *lb.Header* is a header consistent with the blockchain + - *lb.Validators* is the validator set of the blockchain at height *nextHeight* + - *lb.NextValidators* is the validator set of the blockchain at height *nextHeight + 1* + - if *node* is faulty: Returns a LightBlock with arbitrary content + [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] +- Error condition + - if *n* is correct: precondition violated + - if *n* is faulty: arbitrary error + - if *lb.provider != peer* + - times out after 2 Delta (by assumption *n* is faulty) + +---- + +## Core Verification + +### Outline + +The `VerifyToTarget` is the main function and uses the following functions. + +- `FetchLightBlock` is called to download the next light block. It is + the only function that communicates with other nodes +- `ValidAndVerified` checks whether header is valid and checks if a + new lightBlock should be trusted + based on a previously verified lightBlock. +- `Schedule` decides which height to try to verify next + +In the following description of `VerifyToTarget` we do not deal with error +handling. If any of the above function returns an error, VerifyToTarget just +passes the error on. + +#### **[LCV-FUNC-MAIN.1]** + +```go +func VerifyToTarget(primary PeerID, lightStore LightStore, + targetHeight Height) (LightStore, Result) { + + nextHeight := targetHeight + + for lightStore.LatestVerified.height < targetHeight { + + // Get next LightBlock for verification + current, found := lightStore.Get(nextHeight) + if !found { + current = FetchLightBlock(primary, nextHeight) + lightStore.Update(current, StateUnverified) + } + + // Verify + verdict = ValidAndVerified(lightStore.LatestVerified, current) + + // Decide whether/how to continue + if verdict == SUCCESS { + lightStore.Update(current, StateVerified) + } + else if verdict == NOT_ENOUGH_TRUST { + // do nothing + // the light block current passed validation, but the validator + // set is too different to verify it. We keep the state of + // current at StateUnverified. For a later iteration, Schedule + // might decide to try verification of that light block again. + } + else { + // verdict is some error code + lightStore.Update(current, StateFailed) + // possibly remove all LightBlocks from primary + return (lightStore, ResultFailure) + } + nextHeight = Schedule(lightStore, nextHeight, targetHeight) + } + return (lightStore, ResultSuccess) +} +``` + +- Expected precondition + - *lightStore* contains a LightBlock within the *trustingPeriod* **[LCV-PRE-TP.1]** + - *targetHeight* is greater than the height of all the LightBlocks in *lightStore* +- Expected postcondition: + - returns *lightStore* that contains a LightBlock that corresponds to a block + of the blockchain of height *targetHeight* + (that is, the LightBlock has been added to *lightStore*) **[LCV-POST-LS.1]** +- Error conditions + - if the precondition is violated + - if `ValidAndVerified` or `FetchLightBlock` report an error + - if [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) is violated + +### Details of the Functions + +#### **[LCV-FUNC-VALID.1]** + +```go +func ValidAndVerified(trusted LightBlock, untrusted LightBlock) Result +``` + +- Expected precondition: + - *untrusted* is valid, that is, satisfies the soundness [checks][block] + - *untrusted* is **well-formed**, that is, + - *untrusted.Header.Time < now + clockDrift* + - *untrusted.Validators = hash(untrusted.Header.Validators)* + - *untrusted.NextValidators = hash(untrusted.Header.NextValidators)* + - *trusted.Header.Time > now - trustingPeriod* + - *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 + - the `Height` and `Time` of `trusted` are smaller than the Height and + `Time` of `untrusted`, respectively + - the *untrusted.Header* is well-formed (passes the tests from + [[block]]), and in particular + - if the untrusted header `unstrusted.Header` is the immediate + successor of `trusted.Header`, then it holds that + - *trusted.Header.NextValidators = + untrusted.Header.Validators*, and + moreover, + - *untrusted.Header.Commit* + - contains signatures by more than two-thirds of the validators + - contains no signature from nodes that are not in *trusted.Header.NextValidators* +- Expected postcondition: + - Returns `SUCCESS`: + - if *untrusted* is the immediate successor of *trusted*, or otherwise, + - if the signatures of a set of validators that have more than + *max(1/3,trustThreshold)* of voting power in + *trusted.Nextvalidators* is contained in + *untrusted.Commit* (that is, header passes the tests + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] + and [**[TMBC-VAL-COMMIT.1]**][TMBC-VAL-COMMIT-link]) + - Returns `NOT_ENOUGH_TRUST` if: + - *untrusted* is *not* the immediate successor of + *trusted* + and the *max(1/3,trustThreshold)* threshold is not reached + (that is, if + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] + fails and header is does not violate the soundness + checks [[block]]). +- Error condition: + - if precondition violated + +---- + +#### **[LCV-FUNC-SCHEDULE.1]** + +```go +func Schedule(lightStore, nextHeight, targetHeight) Height +``` + +- Implementation remark: If picks the next height to be verified. + We keep the precise choice of the next header under-specified. It is + subject to performance optimizations that do not influence the correctness +- Expected postcondition: **[LCV-SCHEDULE-POST.1]** + Return *H* s.t. + 1. if *lightStore.LatestVerified.Height = nextHeight* and + *lightStore.LatestVerified < targetHeight* then + *nextHeight < H <= targetHeight* + 2. if *lightStore.LatestVerified.Height < nextHeight* and + *lightStore.LatestVerified.Height < targetHeight* then + *lightStore.LatestVerified.Height < H < nextHeight* + 3. if *lightStore.LatestVerified.Height = targetHeight* then + *H = targetHeight* + +> Case i. captures the case where the light block at height *nextHeight* +> has been verified, and we can choose a height closer to the *targetHeight*. +> As we get the *lightStore* as parameter, the choice of the next height can +> depend on the *lightStore*, e.g., we can pick a height for which we have +> already downloaded a light block. +> In Case ii. the header of *nextHeight* could not be verified, and we need to pick a smaller height. +> In Case iii. is a special case when we have verified the *targetHeight*. + +### Solving the distributed specification + +*trustedStore* is implemented by the light blocks in lightStore that +have the state *StateVerified*. + +#### Argument for [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) + +- `ValidAndVerified` implements the soundness checks and the checks + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] and + [**[TMBC-VAL-COMMIT.1]**][TMBC-VAL-COMMIT-link] under + the assumption [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link] +- Only if `ValidAndVerified` returns with `SUCCESS`, the state of a light block is + set to *StateVerified*. + +#### Argument for [**[LCV-DIST-LIVE.1]**](#lcv-dist-life) + +- If *primary* is correct, + - `FetchLightBlock` will always return a light block consistent + with the blockchain + - `ValidAndVerified` either verifies the header using the trusting + period or falls back to sequential + verification + - If [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) holds, eventually every + header will be verified and core verification **terminates successfully**. + - successful termination depends on the age of *lightStore.LatestVerified* + (for instance, initially on the age of *trustedHeader*) and the + changes of the validator sets on the blockchain. + We will give some examples [below](#liveness-scenarios). +- If *primary* is faulty, + - it either provides headers that pass all the tests, and we + return with the header + - it provides one header that fails a test, core verification + **terminates with failure**. + - it times out and core verification + **terminates with failure**. + +## Liveness Scenarios + +The liveness argument above assumes [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) + +which requires that there is a header that does not expire before the +target height is reached. Here we discuss scenarios to ensure this. + +Let *startHeader* be *LightStore.LatestVerified* when core +verification is called (*trustedHeader*) and *startTime* be the time +core verification is invoked. + +In order to ensure liveness, *LightStore* always needs to contain a +verified (or initially trusted) header whose time is within the +trusting period. To ensure this, core verification needs to add new +headers to *LightStore* and verify them, before all headers in +*LightStore* expire. + +#### Many changes in validator set + + Let's consider `Schedule` implements + bisection, that is, it halves the distance. + Assume the case where the validator set changes completely in each +block. Then the + method in this specification needs to +sequentially verify all headers. That is, for + +- *W = log_2 (targetHeight - startHeader.Height)*, + +*W* headers need to be downloaded and checked before the +header of height *startHeader.Height + 1* is added to *LightStore*. + +- Let *Comp* + be the local computation time needed to check headers and signatures + for one header. +- Then we need in the worst case *Comp + 2 Delta* to download and + check one header. +- Then the first time a verified header could be added to *LightStore* is + startTime + W * (Comp + 2 Delta) +- [TP.1] However, it can only be added if we still have a header in + *LightStore*, + which is not + expired, that is only the case if + - startHeader.Time > startTime + WCG * (Comp + 2 Delta) - + trustingPeriod, + - that is, if core verification is started at + startTime < startHeader.Time + trustingPeriod - WCG * (Comp + 2 Delta) + +- one may then do an inductive argument from this point on, depending + on the implementation of `Schedule`. We may have to account for the + headers that are already + downloaded, but they are checked against the new *LightStore.LatestVerified*. + +> We observe that +> the worst case time it needs to verify the header of height +> *targetHeight* depends mainly on how frequent the validator set on the +> blockchain changes. That core verification terminates successfully +> crucially depends on the check [TP.1], that is, that the headers in +> *LightStore* do not expire in the time needed to download more +> headers, which depends on the creation time of the headers in +> *LightStore*. That is, termination of core verification is highly +> depending on the data stored in the blockchain. +> The current light client core verification protocol exploits that, in +> practice, changes in the validator set are rare. For instance, +> consider the following scenario. + +#### No change in validator set + +If on the blockchain the validator set of the block at height +*targetHeight* is equal to *startHeader.NextValidators*: + +- there is one round trip in `FetchLightBlock` to download the light + block + of height + *targetHeight*, and *Comp* to check it. +- as the validator sets are equal, `Verify` returns `SUCCESS`, if + *startHeader.Time > now - trustingPeriod*. +- that is, if *startTime < startHeader.Header.Time + trustingPeriod - + 2 Delta - Comp*, then core verification terminates successfully + +# Part V - Supporting the IBC Relayer + +The above specification focuses on the most common case, which also +constitutes the most challenging task: using the Tendermint [security +model][TMBC-FM-2THIRDS-link] to verify light blocks without +downloading all intermediate blocks. To focus on this challenge, above +we have restricted ourselves to the case where *targetHeight* is +greater than the height of any trusted header. This simplified +presentation of the algorithm as initially +`lightStore.LatestVerified()` is less than *targetHeight*, and in the +process of verification `lightStore.LatestVerified()` increases until +*targetHeight* is reached. + +For [IBC][ibc-rs] it might be that some "older" header is +needed, that is, *targetHeight < lightStore.LatestVerified()*. In this section we present a preliminary design, and we mark some +remaining open questions. +If *targetHeight < lightStore.LatestVerified()* our design separates +the following cases: + +- A previous instance of `VerifyToTarget` has already downloaded the + light block of *targetHeight*. There are two cases + - the light block has been verified + - the light block has not been verified yet +- No light block of *targetHeight* had been downloaded before. There + are two cases: + - there exists a verified light block of height less than *targetHeight* + - otherwise. In this case we need to do "backwards verification" + using the hash of the previous block in the `LastBlockID` field + of a header. + +**Open Question:** what are the security assumptions for backward +verification. Should we check that the light block we verify from +(and/or the checked light block) is within the trusting period? + +The design just presents the above case +distinction as a function, and defines some auxiliary functions in the +same way the protocol was presented in +[Part IV](#part-iv---light-client-verification-protocol). + +```go +func (ls LightStore) LatestPrevious(height Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a light block *lb* that satisfies: + - *lb* is in lightStore + - *lb* is verified and not expired + - *lb.Header.Height < height* + - for all *b* in lightStore s.t. *b* is verified and not expired it + holds *lb.Header.Height >= b.Header.Height* + - *false* in the second argument if + the LightStore does not contain such an *lb*. + +```go +func (ls LightStore) MinVerified() (LightBlock, bool) +``` + +- Expected postcondition + - returns a light block *lb* that satisfies: + - *lb* is in lightStore + - *lb* is verified **Open Question:** replace by trusted? + - *lb.Header.Height* is minimal in the lightStore + - **Open Question:** according to this, it might be expired (outside the + trusting period). This approach appears safe. Are there reasons we + should not do that? + - *false* in the second argument if + the LightStore does not contain such an *lb*. + +If a height that is smaller than the smallest height in the lightstore +is required, we check the hashes backwards. This is done with the +following function: + +#### **[LCV-FUNC-BACKWARDS.1]** + +```go +func Backwards (primary PeerID, lightStore LightStore, targetHeight Height) + (LightStore, Result) { + + lb,res = lightStore.MinVerified() + if res = false { + return (lightStore, ResultFailure) + } + + latest := lb.Header + for i := lb.Header.height - 1; i >= targetHeight; i-- { + // here we download height-by-height. We might first download all + // headers down to targetHeight and then check them. + current := FetchLightBlock(primary,i) + if (hash(current) != latest.Header.LastBlockId) { + return (lightStore, ResultFailure) + } + else { + lightStore.Update(current, StateVerified) + // **Open Question:** Do we need a new state type for + // backwards verified light blocks? + } + latest = current + } + return (lightStore, ResultSuccess) +} +``` + +The following function just decided based on the required height which +method should be used. + +#### **[LCV-FUNC-IBCMAIN.1]** + +```go +func Main (primary PeerID, lightStore LightStore, targetHeight Height) + (LightStore, Result) { + + b1, r1 = lightStore.Get(targetHeight) + if r1 = true and b1.State = StateVerified { + // block already there + return (lightStore, ResultSuccess) + } + + if targetHeight > lightStore.LatestVerified.height { + // case of Part IV + return VerifyToTarget(primary, lightStore, targetHeight) + } + else { + b2, r2 = lightStore.LatestPrevious(targetHeight); + if r2 = true { + // make auxiliary lightStore auxLS to call VerifyToTarget. + // VerifyToTarget uses LatestVerified of the given lightStore + // For that we need: + // auxLS.LatestVerified = lightStore.LatestPrevious(targetHeight) + auxLS.Init; + auxLS.Update(b2,StateVerified); + if r1 = true { + // we need to verify a previously downloaded light block. + // we add it to the auxiliary store so that VerifyToTarget + // does not download it again + auxLS.Update(b1,b1.State); + } + auxLS, res2 = VerifyToTarget(primary, auxLS, targetHeight) + // move all lightblocks from auxLS to lightStore, + // maintain state + // we do that whether VerifyToTarget was successful or not + for i, s range auxLS { + lighStore.Update(s,s.State) + } + return (lightStore, res2) + } + else { + return Backwards(primary, lightStore, targetHeight) + } + } +} +``` + + + + + + + + + + + + + + + + + + + +# References + +[[block]] Specification of the block data structure. + +[[RPC]] RPC client for Tendermint + +[[fork-detector]] The specification of the light client fork detector. + +[[fullnode]] Specification of the full node API + +[[ibc-rs]] Rust implementation of IBC modules and relayer. + +[[lightclient]] The light client ADR [77d2651 on Dec 27, 2019]. + +[RPC]: https://docs.tendermint.com/master/rpc/ + +[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md + +[TMBC-HEADER-link]: #tmbc-header1 +[TMBC-SEQ-link]: #tmbc-seq1 +[TMBC-CorrFull-link]: #tmbc-corr-full1 +[TMBC-Auth-Byz-link]: #tmbc-auth-byz1 +[TMBC-TIME_PARAMS-link]: #tmbc-time-params1 +[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds1 +[TMBC-VAL-CONTAINS-CORR-link]: #tmbc-val-contains-corr1 +[TMBC-VAL-COMMIT-link]: #tmbc-val-commit1 +[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1 + +[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md +[fork-detector]: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/detection.md +[fullnode]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md + +[ibc-rs]:https://github.com/informalsystems/ibc-rs + +[FN-LuckyCase-link]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#fn-luckycase + +[blockchain-validator-set]: https://github.com/tendermint/spec/blob/master/spec/blockchain/blockchain.md#data-structures +[fullnode-data-structures]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#data-structures + +[FN-ManifestFaulty-link]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#fn-manifestfaulty + +[arXiv]: https://arxiv.org/abs/1807.04938 diff --git a/rust-spec/lightclient/verification/verification_002_draft.md b/rust-spec/lightclient/verification/verification_002_draft.md new file mode 100644 index 000000000..80a1890c4 --- /dev/null +++ b/rust-spec/lightclient/verification/verification_002_draft.md @@ -0,0 +1,1061 @@ +# Light Client Verification + +The light client implements a read operation of a +[header][TMBC-HEADER-link] from the [blockchain][TMBC-SEQ-link], by +communicating with full nodes. 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*. The fault-tolerant read +operation is designed for this security model. + +The challenge addressed here is that the light client might have a +block of height *h1* and needs to read the block of height *h2* +greater than *h1*. Checking all headers of heights from *h1* to *h2* +might be too costly (e.g., in terms of energy for mobile devices). +This specification tries to reduce the number of intermediate blocks +that need to be checked, by exploiting the guarantees provided by the +[security model][TMBC-FM-2THIRDS-link]. + +# Status + +## Previous Versions + +- [[001_published]](./verification_001_published.md) + is thoroughly reviewed, and the protocol has been +formalized in TLA+ and model checked. + +## Issues that are addressed in this revision + +As it is part of the larger light node, its data structures and +functions interact with the attack dectection functionality of the light +client. As a result of the work on + +- [attack detection](https://github.com/tendermint/spec/pull/164) for light nodes + +- attack detection for IBC and [relayer requirements](https://github.com/informalsystems/tendermint-rs/issues/497) + +- light client + [supervisor](https://github.com/tendermint/spec/pull/159) (also in + [Rust proposal](https://github.com/informalsystems/tendermint-rs/pull/509)) + +adaptations to the semantics and functions exposed by the LightStore +needed to be made. In contrast to [version +001](./verification_001_published.md) we specify the following: + +- `VerifyToTarget` and `Backwards` are called with a single lightblock + as root of trust in contrast to passing the complete lightstore. + +- During verification, we record for each lightblock which other + lightblock can be used to verify it in one step. This is needed to + generate verification traces that are needed for IBC. + +# Outline + +- [Part I](#part-i---tendermint-blockchain): Introduction of + relevant terms of the Tendermint +blockchain. + +- [Part II](#part-ii---sequential-definition-of-the-verification-problem): Introduction +of the problem addressed by the Lightclient Verification protocol. + - [Verification Informal Problem + statement](#Verification-Informal-Problem-statement): For the general + audience, that is, engineers who want to get an overview over what + the component is doing from a bird's eye view. + - [Sequential Problem statement](#Sequential-Problem-statement): + Provides a mathematical definition of the problem statement in + its sequential form, that is, ignoring the distributed aspect of + the implementation of the blockchain. + +- [Part III](#part-iii---light-client-as-distributed-system): Distributed + aspects of the light client, system assumptions and temporal + logic specifications. + + - [Incentives](#incentives): how faulty full nodes may benefit from + misbehaving and how correct full nodes benefit from cooperating. + + - [Computational Model](#Computational-Model): + timing and correctness assumptions. + + - [Distributed Problem Statement](#Distributed-Problem-Statement): + temporal properties that formalize safety and liveness + properties in the distributed setting. + +- [Part IV](#part-iv---light-client-verification-protocol): + Specification of the protocols. + + - [Definitions](#Definitions): Describes inputs, outputs, + variables used by the protocol, auxiliary functions + + - [Core Verification](#core-verification): gives an outline of the solution, + and details of the functions used (with preconditions, + postconditions, error conditions). + + - [Liveness Scenarios](#liveness-scenarios): when the light + client makes progress depends heavily on the changes in the + validator sets of the blockchain. We discuss some typical scenarios. + +- [Part V](#part-v---supporting-the-ibc-relayer): The above parts + focus on a common case where the last verified block has height *h1* + and the + requested height *h2* satisfies *h2 > h1*. For IBC, there are + scenarios where this might not be the case. In this part, we provide + some preliminaries for supporting this. As not all details of the + IBC requirements are clear by now, we do not provide a complete + specification at this point. We mark with "Open Question" points + that need to be addressed in order to finalize this specification. + It should be noted that the technically + most challenging case is the one specified in Part IV. + +In this document we quite extensively use tags in order to be able to +reference assumptions, invariants, etc. in future communication. In +these tags we frequently use the following short forms: + +- TMBC: Tendermint blockchain +- SEQ: for sequential specifications +- LCV: Lightclient Verification +- LIVE: liveness +- SAFE: safety +- FUNC: function +- INV: invariant +- A: assumption + +# Part I - Tendermint Blockchain + +## Header Fields necessary for the Light Client + +#### **[TMBC-HEADER.1]** + +A set of blockchain transactions is stored in a data structure called +*block*, which contains a field called *header*. (The data structure +*block* is defined [here][block]). As the header contains hashes to +the relevant fields of the block, for the purpose of this +specification, we will assume that the blockchain is a list of +headers, rather than a list of blocks. + +#### **[TMBC-HASH-UNIQUENESS.1]** + +We assume that every hash in the header identifies the data it hashes. +Therefore, in this specification, we do not distinguish between hashes and the +data they represent. + +#### **[TMBC-HEADER-FIELDS.2]** + +A header contains the following fields: + +- `Height`: non-negative integer +- `Time`: time (non-negative integer) +- `LastBlockID`: Hashvalue +- `LastCommit` DomainCommit +- `Validators`: DomainVal +- `NextValidators`: DomainVal +- `Data`: DomainTX +- `AppState`: DomainApp +- `LastResults`: DomainRes + +#### **[TMBC-SEQ.1]** + +The Tendermint blockchain is a list *chain* of headers. + +#### **[TMBC-VALIDATOR-PAIR.1]** + +Given a full node, a +*validator pair* is a pair *(peerID, voting_power)*, where + +- *peerID* is the PeerID (public key) of a full node, +- *voting_power* is an integer (representing the full node's + voting power in a certain consensus instance). + +> In the Golang implementation the data type for *validator +pair* is called `Validator` + +#### **[TMBC-VALIDATOR-SET.1]** + +A *validator set* is a set of validator pairs. For a validator set +*vs*, we write *TotalVotingPower(vs)* for the sum of the voting powers +of its validator pairs. + +#### **[TMBC-VOTE.1]** + +A *vote* contains a `prevote` or `precommit` message sent and signed by +a validator node during the execution of [consensus][arXiv]. Each +message contains the following fields + +- `Type`: prevote or precommit +- `Height`: positive integer +- `Round` a positive integer +- `BlockID` a Hashvalue of a block (not necessarily a block of the chain) + +#### **[TMBC-COMMIT.1]** + +A commit is a set of `precommit` message. + +## Tendermint Failure Model + +#### **[TMBC-AUTH-BYZ.1]** + +We assume the authenticated Byzantine fault model in which no node (faulty or +correct) may break digital signatures, but otherwise, no additional +assumption is made about the internal behavior of faulty +nodes. That is, faulty nodes are only limited in that they cannot forge +messages. + +#### **[TMBC-TIME-PARAMS.1]** + +A Tendermint blockchain has the following configuration parameters: + +- *unbondingPeriod*: a time duration. +- *trustingPeriod*: a time duration smaller than *unbondingPeriod*. + +#### **[TMBC-CORRECT.1]** + +We define a predicate *correctUntil(n, t)*, where *n* is a node and *t* is a +time point. +The predicate *correctUntil(n, t)* is true if and only if the node *n* +follows all the protocols (at least) until time *t*. + +#### **[TMBC-FM-2THIRDS.1]** + +If a block *h* is in the chain, +then there exists a subset *CorrV* +of *h.NextValidators*, such that: + +- *TotalVotingPower(CorrV) > 2/3 + TotalVotingPower(h.NextValidators)*; cf. [TMBC-VALIDATOR-SET.1] +- For every validator pair *(n,p)* in *CorrV*, it holds *correctUntil(n, + h.Time + trustingPeriod)*; cf. [TMBC-CORRECT.1] + +> The definition of correct +> [**[TMBC-CORRECT.1]**][TMBC-CORRECT-link] refers to realtime, while it +> is used here with *Time* and *trustingPeriod*, which are "hardware +> times". We do not make a distinction here. + +#### **[TMBC-CORR-FULL.1]** + +Every correct full node locally stores a prefix of the +current list of headers from [**[TMBC-SEQ.1]**][TMBC-SEQ-link]. + +## What the Light Client Checks + +> From [TMBC-FM-2THIRDS.1] we directly derive the following observation: + +#### **[TMBC-VAL-CONTAINS-CORR.1]** + +Given a (trusted) block *tb* of the blockchain, a given set of full nodes +*N* contains a correct node at a real-time *t*, if + +- *t - trustingPeriod < tb.Time < t* +- the voting power in tb.NextValidators of nodes in *N* is more + than 1/3 of *TotalVotingPower(tb.NextValidators)* + +> The following describes how a commit for a given block *b* must look +> like. + +#### **[TMBC-SOUND-DISTR-POSS-COMMIT.1]** + +For a block *b*, each element *pc* of *PossibleCommit(b)* satisfies: + +- *pc* contains only votes (cf. [TMBC-VOTE.1]) + by validators from *b.Validators* +- the sum of the voting powers in *pc* is greater than 2/3 + *TotalVotingPower(b.Validators)* +- and there is an *r* such that each vote *v* in *pc* satisfies + - v.Type = precommit + - v.Height = b.Height + - v.Round = r + - v.blockID = hash(b) + +> The following property comes from the validity of the [consensus][arXiv]: A +> correct validator node only sends `prevote` or `precommit`, if +> `BlockID` of the new (to-be-decided) block is equal to the hash of +> the last block. + +#### **[TMBC-VAL-COMMIT.1]** + +If for a block *b*, a commit *c* + +- contains at least one validator pair *(v,p)* such that *v* is a + **correct** validator node, and +- is contained in *PossibleCommit(b)* + +then the block *b* is on the blockchain. + +## Context of this document + +In this document we specify the light client verification component, +called *Core Verification*. The *Core Verification* communicates with +a full node. As full nodes may be faulty, it cannot trust the +received information, but the light client has to check whether the +header it receives coincides with the one generated by Tendermint +consensus. + +The two + properties [[TMBC-VAL-CONTAINS-CORR.1]][TMBC-VAL-CONTAINS-CORR-link] and +[[TMBC-VAL-COMMIT]][TMBC-VAL-COMMIT-link] formalize the checks done + by this specification: +Given a trusted block *tb* and an untrusted block *ub* with a commit *cub*, +one has to check that *cub* is in *PossibleCommit(ub)*, and that *cub* +contains a correct node using *tb*. + +# Part II - Sequential Definition of the Verification Problem + +## Verification Informal Problem statement + +Given a height *targetHeight* as an input, the *Verifier* eventually +stores a header *h* of height *targetHeight* locally. This header *h* +is generated by the Tendermint [blockchain][block]. In +particular, a header that was not generated by the blockchain should +never be stored. + +## Sequential Problem statement + +#### **[LCV-SEQ-LIVE.1]** + +The *Verifier* gets as input a height *targetHeight*, and eventually stores the +header of height *targetHeight* of the blockchain. + +#### **[LCV-SEQ-SAFE.1]** + +The *Verifier* never stores a header which is not in the blockchain. + +# Part III - Light Client as Distributed System + +## Incentives + +Faulty full nodes may benefit from lying to the light client, by making the +light client accept a block that deviates (e.g., contains additional +transactions) from the one generated by Tendermint consensus. +Users using the light client might be harmed by accepting a forged header. + +The [attack detector][attack-detector] of the light client may help the +correct full nodes to understand whether their header is a good one. +Hence, in combination with the light client detector, the correct full +nodes have the incentive to respond. We can thus base liveness +arguments on the assumption that correct full nodes reliably talk to +the light client. + +## Computational Model + +#### **[LCV-A-PEER.1]** + +The verifier communicates with a full node called *primary*. No assumption is made about the full node (it may be correct or faulty). + +#### **[LCV-A-COMM.1]** + +Communication between the light client 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 processes 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. + +#### **[LCV-A-TFM.1]** + +The Tendermint blockchain satisfies the Tendermint failure model [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. + +#### **[LCV-A-VAL.1]** + +The system satisfies [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] and +[**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. Thus, there is a +blockchain that satisfies the soundness requirements (that is, the +validation rules in [[block]]). + +## Distributed Problem Statement + +### Two Kinds of Termination + +We do not assume that *primary* is correct. Under this assumption no +protocol can guarantee the combination of the sequential +properties. Thus, in the (unreliable) distributed setting, we consider +two kinds of termination (successful and failure) and we will specify +below under what (favorable) conditions *Core Verification* ensures to +terminate successfully, and satisfy the requirements of the sequential +problem statement: + +#### **[LCV-DIST-TERM.1]** + +*Core Verification* either *terminates +successfully* or it *terminates with failure*. + +### Design choices + +#### **[LCV-DIST-STORE.2]** + +*Core Verification* returns a data structure called *LightStore* that +contains light blocks (that contain a header). + +#### **[LCV-DIST-INIT.2]** + +*Core Verification* is called with + +- *primary*: the PeerID of a full node (with verification communicates) +- *root*: a light block (the root of trust) +- *targetHeight*: a height (the height of a header that should be obtained) + +### Temporal Properties + +#### **[LCV-DIST-SAFE.2]** + +It is always the case that every header in *LightStore* was +generated by an instance of Tendermint consensus. + +#### **[LCV-DIST-LIVE.2]** + +If a new instance of *Core Verification* is called with a +height *targetHeight* greater than root.Header.Height it must +must eventually terminate. + +- If + - the *primary* is correct (and locally has the block of + *targetHeight*), and + - the age of root is always less than the trusting period, + then *Core Verification* adds a verified header *hd* with height + *targetHeight* to *LightStore* and it **terminates successfully** + +> These definitions imply that if the primary is faulty, a header may or +> may not be added to *LightStore*. In any case, +> [**[LCV-DIST-SAFE.2]**](#lcv-dist-safe2) must hold. +> The invariant [**[LCV-DIST-SAFE.2]**](#lcv-dist-safe2) and the liveness +> requirement [**[LCV-DIST-LIVE.2]**](#lcv-dist-life) +> allow that verified headers are added to *LightStore* whose +> height was not passed +> to the verifier (e.g., intermediate headers used in bisection; see below). +> Note that for liveness, initially having a *root* within +> the *trustinPeriod* is not sufficient. However, as this +> specification will leave some freedom with respect to the strategy +> in which order to download intermediate headers, we do not give a +> more precise liveness specification here. After giving the +> specification of the protocol, we will discuss some liveness +> scenarios [below](#liveness-scenarios). + +### Solving the sequential specification + +This specification provides a partial solution to the sequential specification. +The *Verifier* solves the invariant of the sequential part + +[**[LCV-DIST-SAFE.2]**](#lcv-dist-safe2) => [**[LCV-SEQ-SAFE.1]**](#lcv-seq-safe1) + +In the case the primary is correct, and *root* is a recent header in *LightStore*, the verifier satisfies the liveness requirements. + +⋀ *primary is correct* +⋀ *root.header.Time* > *now* - *trustingPeriod* +⋀ [**[LCV-A-Comm.1]**](#lcv-a-comm) ⋀ ( + ( [**[TMBC-CorrFull.1]**][TMBC-CorrFull-link] ⋀ + [**[LCV-DIST-LIVE.2]**](#lcv-dist-live2) ) + ⟹ [**[LCV-SEQ-LIVE.1]**](#lcv-seq-live1) +) + +# Part IV - Light Client Verification Protocol + +We provide a specification for Light Client Verification. The local +code for verification is presented by a sequential function +`VerifyToTarget` to highlight the control flow of this functionality. +We note that if a different concurrency model is considered for +an implementation, the sequential flow of the function may be +implemented with mutexes, etc. However, the light client verification +is partitioned into three blocks that can be implemented and tested +independently: + +- `FetchLightBlock` is called to download a light block (header) of a + given height from a peer. +- `ValidAndVerified` is a local code that checks the header. +- `Schedule` decides which height to try to verify next. We keep this + underspecified as different implementations (currently in Goland and + Rust) may implement different optimizations here. We just provide + necessary conditions on how the height may evolve. + + + + +## Definitions + +### Data Types + +The core data structure of the protocol is the LightBlock. + +#### **[LCV-DATA-LIGHTBLOCK.1]** + +```go +type LightBlock struct { + Header Header + Commit Commit + Validators ValidatorSet + NextValidators ValidatorSet + Provider PeerID +} +``` + +#### **[LCV-DATA-LIGHTSTORE.2]** + +LightBlocks are stored in a structure which stores all LightBlock from +initialization or received from peers. + +```go +type LightStore struct { + ... +} + +``` + +#### **[LCV-DATA-LS-ROOT.2]** + +For each lightblock in a lightstore we record in a field `verification-root` of +type Height. + +> `verification-root` records the height of a lightblock that can be used to verify +> the lightblock in one step + +#### **[LCV-INV-LS-ROOT.2]** + +At all times, if a lightblock *b* in a lightstore has *b.verification-root = h*, +then + +- the lightstore contains a lightblock with height *h*, or +- *b* has the minimal height of all lightblocks in lightstore, then + b.verification-root should be nil. + +The LightStore exposes the following functions to query stored LightBlocks. + +#### **[LCV-DATA-LS-STATE.1]** +Each LightBlock is in one of the following states: +```go +type VerifiedState int + +const ( + StateUnverified = iota + 1 + StateVerified + StateFailed + StateTrusted +) +``` + +#### **[LCV-FUNC-GET.1]** + +```go +func (ls LightStore) Get(height Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a LightBlock at a given height or false in the second argument if + the LightStore does not contain the specified LightBlock. + +#### **[LCV-FUNC-LATEST.1]** + +```go +func (ls LightStore) Latest() LightBlock +``` + +- Expected postcondition + - returns the highest light block + +#### **[LCV-FUNC-ADD.1]** +```go +func (ls LightStore) Add(newBlock) +``` +- Expected precondition + - the lightstore is empty +- Expected postcondition + - adds newBlock into light store + + +#### **[LCV-FUNC-STORE.1]** + +```go +func (ls LightStore) store_chain(newLS LightStore) +``` + +- Expected postcondition + - adds `newLS` to the lightStore. + + + +#### **[LCV-FUNC-LATEST-VERIF.2]** + +```go +func (ls LightStore) LatestVerified() LightBlock +``` + +- Expected postcondition + - returns the highest light block whose state is `StateVerified` + +#### **[LCV-FUNC-FILTER.1]** + +```go +func (ls LightStore) FilterVerified() LightStore +``` + +- Expected postcondition + - returns all the lightblocks of the lightstore with state `StateVerified` + +#### **[LCV-FUNC-UPDATE.2]** + +```go +func (ls LightStore) Update(lightBlock LightBlock, verfiedState +VerifiedState, root-height Height) +``` + +- Expected postcondition + - the lightblock is part of the lightstore + - The state of the LightBlock is set to *verifiedState*. + - The verification-root of the LightBlock is set to *root-height* + + +```go +func (ls LightStore) TraceTo(lightBlock LightBlock) (LightBlock, LightStore) +``` +- Expected postcondition + - returns a **trusted** lightblock `root` from the lightstore with a height + less than `lightBlock` + - returns a lightstore that contains lightblocks that constitute a + [verification trace](TODOlinkToDetectorSpecOnceThere) from + `root` to `lightBlock` (including `lightBlock`) + + + +### Inputs + +- *root*: A light block that is trusted +- *primary*: peerID +- *targetHeight*: the height of the needed header + +### Configuration Parameters + +- *trustThreshold*: a float. Can be used if correctness should not be based on more voting power and 1/3. +- *trustingPeriod*: a time duration [**[TMBC-TIME_PARAMS.1]**][TMBC-TIME_PARAMS-link]. +- *clockDrift*: a time duration. Correction parameter dealing with only approximately synchronized clocks. + +### Variables + +- *nextHeight*: initially *targetHeight* + > *nextHeight* should be thought of the "height of the next header we need + > to download and verify" + +### Assumptions + +#### **[LCV-A-INIT.2]** + +- *root* is from the blockchain + +- *targetHeight > root.Header.Height* + +### Invariants + +#### **[LCV-INV-TP.2]** + +It is always the case that *LightStore.LatestVerified.Header.Time > now - trustingPeriod*. + +> If the invariant is violated, the light client does not have a +> header it can trust. A trusted header must be obtained externally, +> its trust can only be based on social consensus. +> We use the convention that root is assumed to be verified. + +### Used Remote Functions + +We use the functions `commit` and `validators` that are provided +by the [RPC client for Tendermint][RPC]. + +```go +func Commit(height int64) (SignedHeader, error) +``` + +- Implementation remark + - RPC to full node *n* + - JSON sent: + +```javascript +// POST /commit +{ + "jsonrpc": "2.0", + "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request + "method": "commit", + "params": { + "height": 1234 + } +} +``` + +- Expected precondition + - header of `height` exists on blockchain +- Expected postcondition + - if *n* is correct: Returns the signed header of height `height` + from the blockchain if communication is timely (no timeout) + - if *n* is faulty: Returns a signed header with arbitrary content +- Error condition + - if *n* is correct: precondition violated or timeout + - if *n* is faulty: arbitrary error + +---- + +```go +func Validators(height int64) (ValidatorSet, error) +``` + +- Implementation remark + - RPC to full node *n* + - JSON sent: + +```javascript +// POST /validators +{ + "jsonrpc": "2.0", + "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request + "method": "validators", + "params": { + "height": 1234 + } +} +``` + +- Expected precondition + - header of `height` exists on blockchain +- Expected postcondition + - if *n* is correct: Returns the validator set of height `height` + from the blockchain if communication is timely (no timeout) + - if *n* is faulty: Returns arbitrary validator set +- Error condition + - if *n* is correct: precondition violated or timeout + - if *n* is faulty: arbitrary error + +---- + +### Communicating Function + +#### **[LCV-FUNC-FETCH.1]** + + ```go +func FetchLightBlock(peer PeerID, height Height) LightBlock +``` + +- Implementation remark + - RPC to peer at *PeerID* + - calls `Commit` for *height* and `Validators` for *height* and *height+1* +- Expected precondition + - `height` is less than or equal to height of the peer **[LCV-IO-PRE-HEIGHT.1]** +- Expected postcondition: + - if *node* is correct: + - Returns the LightBlock *lb* of height `height` + that is consistent with the blockchain + - *lb.provider = peer* **[LCV-IO-POST-PROVIDER.1]** + - *lb.Header* is a header consistent with the blockchain + - *lb.Validators* is the validator set of the blockchain at height *nextHeight* + - *lb.NextValidators* is the validator set of the blockchain at height *nextHeight + 1* + - if *node* is faulty: Returns a LightBlock with arbitrary content + [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] +- Error condition + - if *n* is correct: precondition violated + - if *n* is faulty: arbitrary error + - if *lb.provider != peer* + - times out after 2 Delta (by assumption *n* is faulty) + +---- + +## Core Verification + +### Outline + +The `VerifyToTarget` is the main function and uses the following functions. + +- `FetchLightBlock` is called to download the next light block. It is + the only function that communicates with other nodes +- `ValidAndVerified` checks whether header is valid and checks if a + new lightBlock should be trusted + based on a previously verified lightBlock. +- `Schedule` decides which height to try to verify next + +In the following description of `VerifyToTarget` we do not deal with error +handling. If any of the above function returns an error, VerifyToTarget just +passes the error on. + +#### **[LCV-FUNC-MAIN.2]** + +```go +func VerifyToTarget(primary PeerID, root LightBlock, + targetHeight Height) (LightStore, Result) { + + lightStore = new LightStore; + lightStore.Update(root, StateVerified, root.verifiedBy); + nextHeight := targetHeight; + + for lightStore.LatestVerified.height < targetHeight { + + // Get next LightBlock for verification + current, found := lightStore.Get(nextHeight) + if !found { + current = FetchLightBlock(primary, nextHeight) + lightStore.Update(current, StateUnverified, nil) + } + + // Verify + verdict = ValidAndVerified(lightStore.LatestVerified, current) + + // Decide whether/how to continue + if verdict == SUCCESS { + lightStore.Update(current, StateVerified, lightStore.LatestVerified.Height) + } + else if verdict == NOT_ENOUGH_TRUST { + // do nothing + // the light block current passed validation, but the validator + // set is too different to verify it. We keep the state of + // current at StateUnverified. For a later iteration, Schedule + // might decide to try verification of that light block again. + } + else { + // verdict is some error code + lightStore.Update(current, StateFailed, nil) + return (nil, ResultFailure) + } + nextHeight = Schedule(lightStore, nextHeight, targetHeight) + } + return (lightStore.FilterVerified, ResultSuccess) +} +``` + +- Expected precondition + - *root* is within the *trustingPeriod* **[LCV-PRE-TP.1]** + - *targetHeight* is greater than the height of *root* +- Expected postcondition: + - returns *lightStore* that contains a LightBlock that corresponds to a block + of the blockchain of height *targetHeight* + (that is, the LightBlock has been added to *lightStore*) **[LCV-POST-LS.1]** +- Error conditions + - if the precondition is violated + - if `ValidAndVerified` or `FetchLightBlock` report an error + - if [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) is violated + +### Details of the Functions + +#### **[LCV-FUNC-VALID.2]** + +```go +func ValidAndVerified(trusted LightBlock, untrusted LightBlock) Result +``` + +- Expected precondition: + - *untrusted* is valid, that is, satisfies the soundness [checks][block] + - *untrusted* is **well-formed**, that is, + - *untrusted.Header.Time < now + clockDrift* + - *untrusted.Validators = hash(untrusted.Header.Validators)* + - *untrusted.NextValidators = hash(untrusted.Header.NextValidators)* + - *trusted.Header.Time > now - trustingPeriod* + - the `Height` and `Time` of `trusted` are smaller than the Height and + `Time` of `untrusted`, respectively + - the *untrusted.Header* is well-formed (passes the tests from + [[block]]), and in particular + - if the untrusted header `unstrusted.Header` is the immediate + successor of `trusted.Header`, then it holds that + - *trusted.Header.NextValidators = + untrusted.Header.Validators*, and + moreover, + - *untrusted.Header.Commit* + - contains signatures by more than two-thirds of the validators + - contains no signature from nodes that are not in *trusted.Header.NextValidators* +- Expected postcondition: + - Returns `SUCCESS`: + - if *untrusted* is the immediate successor of *trusted*, or otherwise, + - if the signatures of a set of validators that have more than + *max(1/3,trustThreshold)* of voting power in + *trusted.Nextvalidators* is contained in + *untrusted.Commit* (that is, header passes the tests + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] + and [**[TMBC-VAL-COMMIT.1]**][TMBC-VAL-COMMIT-link]) + - Returns `NOT_ENOUGH_TRUST` if: + - *untrusted* is *not* the immediate successor of + *trusted* + and the *max(1/3,trustThreshold)* threshold is not reached + (that is, if + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] + fails and header is does not violate the soundness + checks [[block]]). +- Error condition: + - if precondition violated + +---- + +#### **[LCV-FUNC-SCHEDULE.1]** + +```go +func Schedule(lightStore, nextHeight, targetHeight) Height +``` + +- Implementation remark: If picks the next height to be verified. + We keep the precise choice of the next header under-specified. It is + subject to performance optimizations that do not influence the correctness +- Expected postcondition: **[LCV-SCHEDULE-POST.1]** + Return *H* s.t. + 1. if *lightStore.LatestVerified.Height = nextHeight* and + *lightStore.LatestVerified < targetHeight* then + *nextHeight < H <= targetHeight* + 2. if *lightStore.LatestVerified.Height < nextHeight* and + *lightStore.LatestVerified.Height < targetHeight* then + *lightStore.LatestVerified.Height < H < nextHeight* + 3. if *lightStore.LatestVerified.Height = targetHeight* then + *H = targetHeight* + +> Case i. captures the case where the light block at height *nextHeight* +> has been verified, and we can choose a height closer to the *targetHeight*. +> As we get the *lightStore* as parameter, the choice of the next height can +> depend on the *lightStore*, e.g., we can pick a height for which we have +> already downloaded a light block. +> In Case ii. the header of *nextHeight* could not be verified, and we need to pick a smaller height. +> In Case iii. is a special case when we have verified the *targetHeight*. + +### Solving the distributed specification + +Analogous to [[001_published]](./verification_001_published.md#solving-the-distributed-specification) + +## Liveness Scenarios + +Analogous to [[001_published]](./verification_001_published.md#liveness-scenarios) + +# Part V - Supporting the IBC Relayer + +The above specification focuses on the most common case, which also +constitutes the most challenging task: using the Tendermint [security +model][TMBC-FM-2THIRDS-link] to verify light blocks without +downloading all intermediate blocks. To focus on this challenge, above +we have restricted ourselves to the case where *targetHeight* is +greater than the height of any trusted header. This simplified +presentation of the algorithm as initially +`lightStore.LatestVerified()` is less than *targetHeight*, and in the +process of verification `lightStore.LatestVerified()` increases until +*targetHeight* is reached. + +For [IBC][ibc-rs] there are two additional challenges: + +1. it might be that some "older" header is needed, that is, +*targetHeight < lightStore.LatestVerified()*. The +[supervisor](../supervisor/supervisor.md) checks whether it is in this +case by calling `LatestPrevious` and `MinVerified` and if so it calls +`Backwards`. All these functions are specified below. + +2. In order to submit proof of a light client attack, a relayer may + need to submit a verification trace. This it is important to + compute such a trace efficiently. That it can be done is based on + the invariant [[LCV-INV-LS-ROOT.2]](#LCV-INV-LS-ROOT2) that needs + to be maintained by the light client. In particular + `VerifyToTarget` and `Backwards` need to take care of setting + `verification-root`. + +#### **[LCV-FUNC-LATEST-PREV.2]** + +```go +func (ls LightStore) LatestPrevious(height Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a light block *lb* that satisfies: + - *lb* is in lightStore + - *lb* is in StateTrusted + - *lb* is not expired + - *lb.Header.Height < height* + - for all *b* in lightStore s.t. *b* is trusted and not expired it + holds *lb.Header.Height >= b.Header.Height* + - *false* in the second argument if + the LightStore does not contain such an *lb*. +--- + +#### **[LCV-FUNC-LOWEST.2]** + +```go +func (ls LightStore) Lowest() (LightBlock) +``` +- Expected postcondition + - returns the lowest trusted light block within trusting period +--- + +#### **[LCV-FUNC-MIN.2]** + +```go +func (ls LightStore) MinVerified() (LightBlock, bool) +``` + +- Expected postcondition + - returns a light block *lb* that satisfies: + - *lb* is in lightStore + - *lb.Header.Height* is minimal in the lightStore + - *false* in the second argument if + the LightStore does not contain such an *lb*. + +If a height that is smaller than the smallest height in the lightstore +is required, we check the hashes backwards. This is done with the +following function: + +#### **[LCV-FUNC-BACKWARDS.2]** + +```go +func Backwards (primary PeerID, root LightBlock, targetHeight Height) + (LightStore, Result) { + + lb := root; + lightStore := new LightStore; + lightStore.Update(lb, StateTrusted, lb.verifiedBy) + + latest := lb.Header + for i := lb.Header.height - 1; i >= targetHeight; i-- { + // here we download height-by-height. We might first download all + // headers down to targetHeight and then check them. + current := FetchLightBlock(primary,i) + if (hash(current) != latest.Header.LastBlockId) { + return (nil, ResultFailure) + } + else { + // latest and current are linked together by LastBlockId + // therefore it is not relevant which we verified first + // for consistency, we store latest was veried using + // current so that the verifiedBy is always pointing down + // the chain + lightStore.Update(current, StateTrusted, nil) + lightStore.Update(latest, StateTrusted, current.Header.Height) + } + latest = current + } + return (lightStore, ResultSuccess) +} +``` + +# References + +[[block]] Specification of the block data structure. + +[[RPC]] RPC client for Tendermint + +[[attack-detector]] The specification of the light client attack detector. + +[[fullnode]] Specification of the full node API + +[[ibc-rs]] Rust implementation of IBC modules and relayer. + +[[lightclient]] The light client ADR [77d2651 on Dec 27, 2019]. + +[RPC]: https://docs.tendermint.com/master/rpc/ + +[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md + +[TMBC-HEADER-link]: #tmbc-header1 +[TMBC-SEQ-link]: #tmbc-seq1 +[TMBC-CorrFull-link]: #tmbc-corr-full1 +[TMBC-Auth-Byz-link]: #tmbc-auth-byz1 +[TMBC-TIME_PARAMS-link]: #tmbc-time-params1 +[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds1 +[TMBC-VAL-CONTAINS-CORR-link]: #tmbc-val-contains-corr1 +[TMBC-VAL-COMMIT-link]: #tmbc-val-commit1 +[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1 + +[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md +[attack-detector]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_001_reviewed.md +[fullnode]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md + +[ibc-rs]:https://github.com/informalsystems/ibc-rs + +[blockchain-validator-set]: https://github.com/tendermint/spec/blob/master/spec/blockchain/blockchain.md#data-structures +[fullnode-data-structures]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#data-structures + +[FN-ManifestFaulty-link]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#fn-manifestfaulty + +[arXiv]: https://arxiv.org/abs/1807.04938