CCV: System Model and Properties

CCV: System Model and Properties

Outline

Assumptions

As part of a modular ABCI application, CCV interacts with both the consensus engine (via ABCI) and other application modules (e.g, the Staking module). As an IBC application, CCV interacts with external relayers (defined in ICS 18). In this section we specify what we assume about these other components. A more thorough discussion of the environment in which CCV operates is given in the section Placing CCV within an ABCI Application.

Intuition:

CCV safety relies on the Safe Blockchain assumption, i.e., neither Live Blockchain and Correct Relayer are required for safety. Note though that CCV liveness relies on both Live Blockchain and Correct Relayer assumptions; furthermore, the Correct Relayer assumption relies on both Safe Blockchain and Live Blockchain assumptions.

The Validator Update Provision, Unbonding Safety, Slashing Warranty, and Distribution Warranty assumptions define what is needed from the ABCI application of the provider chain.

The Evidence Provision assumptions defines what is needed from the ABCI application of the consumer chains.

Safe Blockchain: Both the provider and the consumer chains are safe. This means that, for every chain, the underlying consensus engine satisfies safety (e.g., the chain does not fork) and the execution of the state machine follows the described protocol.
Live Blockchain: Both the provider and the consumer chains are live. This means that, for every chain, the underlying consensus engine satisfies liveness (i.e., new blocks are eventually added to the chain).

Note: Both Safe Blockchain and Live Blockchain assumptions require the consensus engine's assumptions to hold, e.g., less than a third of the voting power is Byzantine. For an example, take a look at the Tendermint Paper ↗ OPEN PDF, 1807.04938.pdf.
Correct Relayer: There is at least one correct, live relayer between the provider and consumer chains. This assumption has the following implications.
- The opening handshake messages on the CCV channel are relayed before the Channel Initialization subprotocol times out (see initTimeout).
- Every packet sent on the CCV channel is relayed to the receiving end before the packet timeout elapses (see both vscTimeout and ccvTimeoutTimestamp).
- A correct relayer will eventually relay packets on the token transfer channel.
Clearly, the CCV protocol is responsible of setting the timeouts (see ccvTimeoutTimestamp, vscTimeout, initTimeout in the CCV State), such that the Correct Relayer assumption is feasible.

Discussion: IBC relies on timeouts to signal that a sent packet is not going to be received on the other end. Once an ordered IBC channel timeouts, the channel is closed (see ICS 4). The Correct Relayer assumption is necessary to ensure that the CCV channel cannot ever timeout and, as a result, cannot transit to the closed state.

In practice, the Correct Relayer assumption is realistic since any validator could play the role of the relayer and it is in the best interest of correct validators to successfully relay packets.

The following strategy is a practical example of how to ensure the Correct Relayer assumption holds. Let S denote the sending chain and D the destination chain; and let drift(S,D) be the time drift between S and D, i.e., drift(S,D) = S.currentTimestamp() - D.currentTimestamp() (drift(S,D) > 0 means that S is "ahead" of D). For every packet, S only sets timeoutTimestamp = S.currentTimestamp() + to, with to an application-level parameter. The timeoutTimestamp indicates a timestamp on the destination chain after which the packet will no longer be processed (cf. ICS 4). Therefore, the packet MUST be relayed within a time period of to - drift(S,D), i.e., to - drift(S,D) > RTmax, where RTmax is the maximum relaying time across all packet. Theoretically, choosing the value of to requires knowing the value of drift(S,D) (i.e., to > drift(S,D)); yet, drift(S,D) is not known at a chain level. In practice, choosing to such that to >> drift(S,D) and to >> RTmax, e.g., to = 4 weeks, makes the Correct Relayer assumption feasible.
Validator Update Provision: Let {U1, U2, ..., Ui} be a batch of validator updates applied (by the provider Staking module) to the validator set of the provider chain at block height h. Then, the batch of validator updates obtained (by the provider CCV module) from the provider Staking module at height h MUST be exactly the batch {U1, U2, ..., Ui}.
Unbonding Safety: Let uo be any unbonding operation that starts with an unbonding transaction being executed and completes with the event that returns the corresponding stake; let U(uo) be the validator update caused by initiating uo; let vsc(uo) be the VSC that contains U(uo). Then,
- (unbonding initiation) the provider CCV module MUST be notified of uo's initiation before receiving U(uo);
- (unbonding completion) uo MUST NOT complete on the provider chain before the provider chain registers notifications of vsc(uo)'s maturity from all consumer chains.
Note: Depending on the implementation, the (unbonding initiation) part of the Unbonding Safety MAY NOT be necessary for validator unbonding operations.
Slashing Warranty: If the provider ABCI application (e.g., the Slashing module) receives a request to slash a validator val that misbehaved at block height h, then it slashes the amount of tokens val had bonded at height h except the amount that has already completely unbonded.
Evidence Provision: If the consumer ABCI application receives a valid evidence of misbehavior at block height h, then it MUST submit it to the consumer CCV module exactly once and at the same height h. Furthermore, the consumer ABCI application MUST NOT submit invalid evidence to the consumer CCV module.

Note: What constitutes a valid evidence of misbehavior depends on the type of misbehavior and it is outside the scope of this specification.
Distribution Warranty: The provider ABCI application (e.g., the Distribution module) distributes the tokens from the distribution module account among the validators that are part of the validator set.

Desired Properties

The following properties are concerned with one provider chain providing security to multiple consumer chains. Between the provider chain and each consumer chain, a separate (unique) CCV channel is established.

Note: Except for liveness properties -- Channel Liveness, Apply VSC Liveness, Register Maturity Liveness, and Distribution Liveness -- none of the properties of CCV require the Correct Relayer assumption to hold. Nonetheless, the Correct Relayer assumption is necessary to guarantee the systems properties (except for Validator Set Replication) -- Bond-Based Consumer Voting Power, Slashable Consumer Misbehavior, and Consumer Rewards Distribution.

System Properties

↑ Back to Outline

We use the following notations:

ts(h) is the timestamp of a block with height h, i.e., ts(h) = B.currentTimestamp(), where B is the block at height h;
pBonded(h,val) is the number of tokens bonded by validator val on the provider chain at block height h;
pUnbonding(h,val) is the number of tokens a validator val starts unbonding on the provider at block height h;
VP(T) is the voting power associated to a number T of tokens;
Power(c,h,val) is the voting power granted to a validator val on a chain c at block height h;
Token(power) is the amount of tokens necessary to be bonded (on the provider chain) by a validator to be granted power voting power, i.e., Token(VP(T)) = T;
slash(val, h, hi, sf) is the amount of token slashed from a validator val on the provider chain (i.e., pc) at height h for an infraction (with a slashing fraction of sf) committed at (provider) height hi, i.e., slash(val, h, hi, sf) = sf * Token(Power(pc,hi,val)); note that the infraction can be committed also on a consumer chain, in which case hi is the corresponding height on the provider chain.

Also, we use ha << hb to denote an order relation between heights, i.e., the block at height ha happens before the block at height hb. For heights on the same chain, << is equivalent to <, i.e., ha << hb entails hb is larger than ha. For heights on two different chains, << is establish by the packets sent over an order channel between two chains, i.e., if a chain A sends at height ha a packet to a chain B and B receives it at height hb, then ha << hb.

Note: << is transitive, i.e., ha << hb and hb << hc entail ha << hc.

Note: The block on the proposer chain that handles a governance proposal to spawn a new consumer chain cc happens before all the blocks of cc.

CCV provides the following system properties.

Validator Set Replication: Every validator set on any consumer chain MUST either be or have been a validator set on the provider chain.
Bond-Based Consumer Voting Power: Let val be a validator, cc be a consumer chain, both hc and hc' be heights on cc, and both hp and hp' be heights on the provider chain, such that
- val has Power(cc,hc,val) voting power on cc at height hc;
- hc' is the smallest height on cc that satisfies ts(hc') >= ts(hc) + UnbondingPeriod, i.e., val cannot completely unbond on cc before hc';
- hp is the largest height on the provider chain that satisfies hp << hc, i.e., Power(pc,hp,val) = Power(cc,hc,val), where pc is the provider chain;
- hp' is the smallest height on the provider chain that satisfies hc' << hp', i.e., val cannot completely unbond on the provider chain before hp';
- sumUnbonding(hp, h, val) is the sum of all tokens of val that start unbonding on the provider at all heights hu and are still unbonding at height h, such that hp < hu <= h
- sumSlash(hp, h, val) is the sum of the slashes of val at all heights hs for infractions committed at hp, such that hp < hs <= h.
Then for all heights h on the provider chain,
```
hp <= h < hp': 
Power(cc,hc,val) <= VP( pBonded(h,val) + sumUnbonding(hp, h, val) + sumSlash(hp, h, val) )
```
Note: The reason for + sumUnbonding(hp, h, val) in the above inequality is that tokens that val start unbonding after hp have contributed to the power granted to val at height hc on cc (i.e., Power(cc,hc,val)). As a result, these tokens should be available for slashing until hp'.

Note: The reason for + sumSlash(hp, h, val) in the above inequality is that slashing val reduces its locked tokens (i.e., pBonded(h,val) and sumUnbonding(hp, h, val)), however it does not reduce the power already granted to it at height hc on cc (i.e., Power(cc,hc,val)).

Intuition: The Bond-Based Consumer Voting Power property ensures that validators that validate on the consumer chains have enough tokens bonded on the provider chain for a sufficient amount of time such that the security model holds. This means that if the validators misbehave on the consumer chains, their tokens bonded on the provider chain can be slashed during the unbonding period. For example, if one unit of voting power requires 1.000.000 bonded tokens (i.e., VP(1.000.000)=1), then a validator that gets one unit of voting power on a consumer chain must have at least 1.000.000 tokens bonded on the provider chain until the unbonding period elapses on the consumer chain.

Note: When an existing chain becomes a consumer chain (see Channel Initialization: Existing Chains), the existing validator set is replaced by the provider validator set. For safety, the stake bonded by the existing validator set must remain bonded until the unbonding period elapses. Thus, the existing Staking module must be kept for at least the unbonding period.
Slashable Consumer Misbehavior: If a validator val commits an infraction, with a slashing fraction of sf, on a consumer chain cc at a block height hi, then any evidence of misbehavior that is received by cc at height he, such that ts(he) < ts(hi) + UnbondingPeriod, MUST results in exactly the amount of tokens sf*Token(Power(cc,hi,val)) to be slashed on the provider chain. Furthermore, val MUST NOT be slashed more than once for the same misbehavior.

Note: Unlike in single-chain validation, in CCV the tokens sf*Token(Power(cc,hi,val)) MAY be slashed even if the evidence of misbehavior is received at height he such that ts(he) >= ts(hi) + UnbondingPeriod, since unbonding operations need to reach maturity on both the provider and all the consumer chains.

Note: The Slashable Consumer Misbehavior property also ensures that if a delegator starts unbonding an amount x of tokens from val before height hi, then x will not be slashed, since x is not part of Token(Power(c,hi,val)).
Consumer Rewards Distribution: If a consumer chain sends to the provider chain an amount T of tokens as reward for providing security, then
- T (equivalent) tokens MUST be eventually minted on the provider chain and then distributed among the validators that are part of the validator set;
- the total supply of tokens MUST be preserved, i.e., the T (original) tokens are escrowed on the consumer chain.

CCV Channel

↑ Back to Outline

Channel Uniqueness: The channel between the provider chain and a consumer chain MUST be unique.
Channel Validity: If a packet P is received by one end of a CCV channel, then P MUST have been sent by the other end of the channel.
Channel Order: If a packet P1 is sent over a CCV channel before a packet P2, then P2 MUST NOT be received by the other end of the channel before P1.
Channel Liveness: Every packet sent over a CCV channel MUST eventually be received by the other end of the channel.

Validator Sets, Validator Updates and VSCs

↑ Back to Outline

In this section, we provide a short discussion on how the validator set, the validator updates, and the VSCs relates in the context of multiple chains.

Every chain consists of a sequence of blocks. At the end of each block, validator updates (i.e., changes in the validators voting power) results in changes in the validator set of the next block. Thus, the sequence of blocks produces a sequence of validator updates and a sequence of validator sets. Furthermore, the sequence of validator updates on the provider chain results in a sequence of VSCs to all consumer chains. Ideally, this sequence of VSCs is applied by every consumer chain, resulting in a sequence of validator sets identical to the one on the provider chain. However, in general this need not be the case. The reason is twofold:

first, given any two chains A and B, we cannot assume that A's rate of adding new block is the same as B's rate (i.e., we consider the sequences of blocks of any two chains to be completely asynchronous);
and second, due to relaying delays, we cannot assume that the rate of sending VSCs matches the rate of receiving VSCs.

As a result, it is possible for multiple VSCs to be received by a consumer chain within the same block and be applied together at the end of the block, i.e., the validator updates within the VSCs are being aggregated by keeping only the latest update per validator. As a consequence, some validator sets on the provider chain are not existing on all consumer chains. In other words, the validator sets on each consumer chain form a subsequence of the validator sets on the provider chain. Nonetheless, as a requirement of CCV, all the validator updates on the provider chain MUST be included in the sequence of validator sets on all consumer chains.

This is possible since every validator update contains the absolute voting power of that validator. Given a validator val, the sequence of validator updates targeting val (i.e., updates of the voting power of val) is the prefix sum of the sequence of relative changes of the voting power of val. Thus, given a validator update U targeting val that occurs at a block height h, U sums up all the relative changes of the voting power of val that occur until height h, i.e., U = c_1+c_2+...+c_i, such that c_i is the last relative change that occurs by h. Note that relative changes are integer values.

As a consequence, CCV can rely on the following property:

Validator Update Inclusion: Let U1 and U2 be two validator updates targeting the same validator val. If U1 occurs before U2, then U2 sums up all the changes of the voting power of val that are summed up by U1, i.e.,
- U1 = c_1+c_2+...+c_i and
- U2 = c_1+c_2+...+c_i+c_(i+1)+...+c_j.

The Validator Update Inclusion property enables CCV to aggregate multiple VSCs. It is sufficient for the consumer chains to apply only the last update per validator. Since the last update of a validator includes all the previous updates of that validator, once it is applied, all the previous updates are also applied.

Staking Module Interface

↑ Back to Outline

The following properties define the guarantees of CCV on providing VSCs to the consumer chains as a consequence of validator updates on the provider chain.

Validator Update To VSC Validity: Every VSC provided to a consumer chain MUST contain only validator updates that were applied to the validator set of the provider chain (i.e., resulted from a change in the amount of bonded tokens on the provider chain).
Validator Update To VSC Order: Let U1 and U2 be two validator updates on the provider chain. If U1 occurs before U2, then U2 MUST NOT be included in a provided VSC before U1. Note that the order within a single VSC is not relevant.
Validator Update To VSC Liveness: Every update of a validator in the validator set of the provider chain MUST eventually be included in a VSC provided to all consumer chains.

Note that as a consequence of the Validator Update To VSC Liveness property, CCV guarantees the following property:

Provide VSC uniformity: If the provider chain provides a VSC to a consumer chain, then it MUST eventually provide that VSC to all consumer chains.

Validator Set Update

↑ Back to Outline

The provider chain providing VSCs to the consumer chains has two

Excerpt (19994 of 41645 characters). Read the whole page on cosmos/ibc (ICS specifications) ↗

← Back to Documentation