From 3f24b4bde18dc6ecd2080b22efb25d253700fae6 Mon Sep 17 00:00:00 2001 From: mpoke Date: Mon, 2 May 2022 10:47:48 +0200 Subject: [PATCH] add note on safety implication of lockUnbondingOnTimeout --- .../system_model_and_properties.md | 33 ++++++++----------- .../technical_specification.md | 20 ++++++++--- 2 files changed, 28 insertions(+), 25 deletions(-) diff --git a/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md b/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md index 9e3066b13..fb0e8c040 100644 --- a/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md +++ b/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md @@ -86,6 +86,9 @@ furthermore, the *Correct Relayer* assumption relies on both *Safe Blockchain* a 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](#outline) @@ -138,14 +141,6 @@ CCV provides the following system properties. - `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. -- ***Distribution Invariant***: If a consumer chain sends to the provider chain an amount `T` of tokens as reward for providing security, then - - `T` (equivalent) tokens are eventually minted on the provider chain and then distributed among the validators that are part of the validator set; - - the total supply of tokens is preserved, i.e., the `T` (original) tokens are escrowed on the consumer chain. - -- ***Distribution Invariant***: If a consumer chain sends to the provider chain an amount `T` of tokens as reward for providing security, then - - `T` (equivalent) tokens are eventually minted on the provider chain and then distributed among the validators that are part of the validator set; - - the total supply of tokens is preserved, i.e., the `T` (original) tokens are escrowed on the consumer chain. - ### CCV Channel [↑ Back to Outline](#outline) @@ -221,8 +216,6 @@ The following properties define the guarantees of CCV on *registering* on the pr - ***Register Maturity Order***: If a VSC `vsc1` was provided by the provider chain before another VSC `vsc2`, then the provider chain MUST NOT register the maturity notification of `vsc2` before the maturity notification of `vsc1`. - ***Register Maturity Liveness***: If the provider chain provides a VSC `vsc` to the consumer chain, then the provider chain MUST eventually register a maturity notification of `vsc` from the consumer chain. -> Note that, except for *Apply VSC Liveness* and *Register Maturity Liveness*, none of the properties of CCV require the *Correct Relayer* assumption to hold. - ### Consumer Initiated Slashing [↑ Back to Outline](#outline) @@ -255,16 +248,16 @@ The following properties define the guarantees of CCV on *registering* on the pr In this section we argue the correctness of the CCV protocol described in the [Technical Specification](./technical_specification.md), i.e., we informally prove the properties described in the [previous section](#desired-properties). -- ***Channel Uniqueness*:** The provider chain side of the CCV channel is established when the provider CCV module receives the first `ChanOpenConfirm` message; all subsequent `ChanOpenConfirm` messages result in the underlying channel being closed (cf. *Safe Blockchain*). +- ***Channel Uniqueness***: The provider chain side of the CCV channel is established when the provider CCV module receives the first `ChanOpenConfirm` message; all subsequent `ChanOpenConfirm` messages result in the underlying channel being closed (cf. *Safe Blockchain*). Similarly, the consumer chain side of the CCV channel is established when the consumer CCV module receives the first `VSCPacket` and ignores any packets received on different channels (cf. *Safe Blockchain*). -- ***Channel Validity*:** Follows directly from the *Safe Blockchain* assumption. +- ***Channel Validity***: Follows directly from the *Safe Blockchain* assumption. -- ***Channel Order*:** The provider chain accepts only ordered channels when receiving a `ChanOpenTry` message (cf. *Safe Blockchain*). +- ***Channel Order***: The provider chain accepts only ordered channels when receiving a `ChanOpenTry` message (cf. *Safe Blockchain*). Similarly, the consumer chain accepts only ordered channels when receiving `ChanOpenInit` messages (cf. *Safe Blockchain*). Thus, the property follows directly from the fact that the CCV channel is ordered. -- ***Channel Liveness*:** The property follows from the *Correct Relayer* assumption. +- ***Channel Liveness***: The property follows from the *Correct Relayer* assumption. - ***Validator Update To VSC Validity***: The provider CCV module provides only VSCs that contain validator updates obtained from the Staking module, i.e., by calling the `GetValidatorUpdates()` method (cf. *Safe Blockchain*). @@ -281,11 +274,11 @@ i.e., we informally prove the properties described in the [previous section](#de However, at height `h`, the provider CCV module tries to obtain a new batch of validator updates from the provider Staking module (cf. *Safe Blockchain*). Thus, this batch of validator updates MUST contain all validator updates applied to the validator set of the provider chain at the end of block `B`, including `U` (cf. *Validator Update Provision*), which contradicts the initial assumption. -- ***Apply VSC Validity*:** The property follows from the following two assertions. +- ***Apply VSC Validity***: The property follows from the following two assertions. - The consumer chain only applies VSCs received in `VSCPacket`s through the CCV channel (cf. *Safe Blockchain*). - The provider chain only sends `VSCPacket`s containing provided VSCs (cf. *Safe Blockchain*). -- ***Apply VSC Order*:** We prove the property through contradiction. +- ***Apply VSC Order***: We prove the property through contradiction. Given two VSCs `vsc1` and `vsc2` such that the provider chain provides `vsc1` before `vsc2`, we assume the consumer chain applies the validator updates included in `vsc2` before the validator updates included in `vsc1`. The following sequence of assertions leads to a contradiction. - The provider chain could not have sent a `VSCPacket` `P2` containing `vsc2` before a `VSCPacket` `P1` containing `vsc1` (cf. *Safe Blockchain*). @@ -297,7 +290,7 @@ i.e., we informally prove the properties described in the [previous section](#de Then, it applies the validator updates included in both `vsc1` and `vsc2` at the end of the block. Thus, it could not have apply the validator updates included in `vsc2` before. -- ***Apply VSC Liveness*:** The provider chain eventually sends over the CCV channel a `VSCPacket` containing `vsc` (cf. *Safe Blockchain*, *Life Blockchain*). +- ***Apply VSC Liveness***: The provider chain eventually sends over the CCV channel a `VSCPacket` containing `vsc` (cf. *Safe Blockchain*, *Life Blockchain*). As a result, the consumer chain eventually receives this packet (cf. *Channel Liveness*). Then, the consumer chain aggregates all received VSCs at the end of the block and applies all the aggregated updates (cf. *Safe Blockchain*, *Life Blockchain*). As a result, the consumer chain applies all validator updates in `vsc` (cf. *Validator Update Inclusion*). @@ -309,7 +302,7 @@ i.e., we informally prove the properties described in the [previous section](#de - The consumer chain receives on the CCV channel only packets sent by the provider chain (cf. *Channel Validity*). - The provider chain only sends `VSCPacket`s containing provided VSCs (cf. *Safe Blockchain*). -- ***Register Maturity Timeliness*:** We prove the property through contradiction. +- ***Register Maturity Timeliness***: We prove the property through contradiction. Given a VSC `vsc` provided by the provider chain to the consumer chain, we assume that the provider chain registers a maturity notification of `vsc` before `UnbondingPeriod` has elapsed on the consumer chain since the consumer chain applied `vsc`. The following sequence of assertions leads to a contradiction. - The provider chain could not have register a maturity notification of `vsc` before receiving on the CCV channel a `VSCMaturedPacket` `P` with `P.id = vsc.id` (cf. *Safe Blockchain*). @@ -320,7 +313,7 @@ i.e., we informally prove the properties described in the [previous section](#de - The provider chain could not have sent `P'` before providing `vsc`. - Since the duration of sending packets through the CCV channel cannot be negative, the provider chain could not have registered a maturity notification of `vsc` before `UnbondingPeriod` has elapsed on the consumer chain since the consumer chain applied `vsc`. -- ***Register Maturity Order*:** We prove the property through contradiction. Given two VSCs `vsc1` and `vsc2` such that the provider chain provides `vsc1` before `vsc2`, we assume the provider chain registers the maturity notification of `vsc2` before the maturity notification of `vsc1`. +- ***Register Maturity Order***: We prove the property through contradiction. Given two VSCs `vsc1` and `vsc2` such that the provider chain provides `vsc1` before `vsc2`, we assume the provider chain registers the maturity notification of `vsc2` before the maturity notification of `vsc1`. The following sequence of assertions leads to a contradiction. - The provider chain could not have sent a `VSCPacket` `P2`, with `P2.updates = C2`, before a `VSCPacket` `P1`, with `P1.updates = C1` (cf. *Safe Blockchain*). - The consumer chain could not have received `P2` before `P1` (cf. *Channel Order*). @@ -328,7 +321,7 @@ i.e., we informally prove the properties described in the [previous section](#de - The provider chain could not have received `P2'` before `P1'` (cf. *Channel Order*). - The provider chain could not have registered the maturity notification of `vsc2` before the maturity notification of `vsc1` (cf. *Safe Blockchain*). -- ***Register Maturity Liveness*:** The property follows from the following sequence of assertions. +- ***Register Maturity Liveness***: The property follows from the following sequence of assertions. - The provider chain eventually sends on the CCV channel a `VSCPacket` `P`, with `P.updates = C` (cf. *Safe Blockchain*, *Life Blockchain*). - The consumer chain eventually receives `P` on the CCV channel (cf. *Channel Liveness*). - The consumer chain eventually sends on the CCV channel a `VSCMaturedPacket` `P'`, with `P'.id = P.id` (cf. *Safe Blockchain*, *Life Blockchain*). diff --git a/spec/app/ics-028-cross-chain-validation/technical_specification.md b/spec/app/ics-028-cross-chain-validation/technical_specification.md index dd8d322c7..3fdcfb65e 100644 --- a/spec/app/ics-028-cross-chain-validation/technical_specification.md +++ b/spec/app/ics-028-cross-chain-validation/technical_specification.md @@ -603,6 +603,16 @@ function StopConsumerChain(chainId: string, lockUnbonding: Bool) { - all the entries with `chainId` are removed from the `vscToUnbondingOps` mapping. - **Error Condition** - None + +> **Note**: Invoking `StopConsumerChain(chainId, lockUnbonding)` with `lockUnbonding == FALSE` entails that all outstanding unbonding operations can complete before the `UnbondingPeriod` elapses on the consumer chain with `chainId`. +> Thus, invoking `StopConsumerChain(chainId, false)` for any `chainId` MAY violate the *Bond-Based Consumer Voting Power* and *Slashable Consumer Misbehavior* properties (see the [System Properties](./system_model_and_properties.md#system-properties) section). +> +> `StopConsumerChain(chainId, false)` is invoked in two scenarios (see Trigger Event above). +> - In the first scenario (i.e., a governance proposal to stop the consumer chain with `chainId`), the validators on the provider chain MUST make sure that it is safe to stop the consumer chain. +> Since a governance proposal needs a majority of the voting power to pass, the safety of invoking `StopConsumerChain(chainId, false)` is ensured by the *Safe Blockchain* assumption (see the [Assumptions](./system_model_and_properties.md#assumptions) section). +> +> - The second scenario (i.e., a timeout) is only possible if the *Correct Relayer* assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section), +> which is necessary to guarantee both the *Bond-Based Consumer Voting Power* and *Slashable Consumer Misbehavior* properties (see the [Assumptions](./system_model_and_properties.md#correctness-reasoning) section). #### **[CCV-PCF-COINIT.1]** @@ -1167,7 +1177,7 @@ function onTimeoutPacket(packet Packet) { - the timeout height or timeout timestamp passing on the consumer chain without the packet being received (see `timeoutPacket` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#sending-end)); - or the channel being closed without the packet being received (see `timeoutOnClose` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#timing-out-on-close)). - **Precondition** - - The Correct Relayer assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). + - The *Correct Relayer* assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). - **Postcondition** - If the timeout is for a `VSCPacket`, the `onTimeoutVSCPacket` method is invoked. - Otherwise, the transaction is aborted. @@ -1257,7 +1267,7 @@ function onTimeoutPacket(packet Packet) { - the timeout height or timeout timestamp passing on the provider chain without the packet being received (see `timeoutPacket` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#sending-end)); - or the channel being closed without the packet being received (see `timeoutOnClose` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#timing-out-on-close)). - **Precondition** - - The Correct Relayer assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). + - The *Correct Relayer* assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). - **Postcondition** - If the timeout is for a `VSCMaturedPacket`, the `onTimeoutVSCMaturedPacket` method is invoked. - If the timeout is for a `SlashPacket`, the `onTimeoutSlashPacket` method is invoked. @@ -1439,7 +1449,7 @@ function onTimeoutVSCPacket(packet: Packet) { - the timeout height or timeout timestamp passing on the consumer chain without the packet being received (see `timeoutPacket` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#sending-end)); - or the channel being closed without the packet being received (see `timeoutOnClose` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#timing-out-on-close)). - **Precondition** - - The Correct Relayer assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). + - The *Correct Relayer* assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). - **Postcondition** - The transaction is aborted if the ID of the channel on which the packet was sent is not mapped to a chain ID (in `channelToChain`). - `StopConsumerChain(chainId, lockUnbondingOnTimeout[chainId])` is invoked, where `chainId = channelToChain[packet.getDestinationChannel()]`. @@ -1717,7 +1727,7 @@ function onTimeoutVSCMaturedPacket(packet Packet) { - the timeout height or timeout timestamp passing on the provider chain without the packet being received (see `timeoutPacket` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#sending-end)); - or the channel being closed without the packet being received (see `timeoutOnClose` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#timing-out-on-close)). - **Precondition** - - The Correct Relayer assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). + - The *Correct Relayer* assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). - **Postcondition** - The state is not changed. - **Error Condition** @@ -1969,7 +1979,7 @@ function onTimeoutSlashPacket(packet Packet) { - the timeout height or timeout timestamp passing on the provider chain without the packet being received (see `timeoutPacket` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#sending-end)); - or the channel being closed without the packet being received (see `timeoutOnClose` defined in [ICS4](../../core/ics-004-channel-and-packet-semantics/README.md#timing-out-on-close)). - **Precondition** - - The Correct Relayer assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). + - The *Correct Relayer* assumption is violated (see the [Assumptions](./system_model_and_properties.md#assumptions) section). - **Postcondition** - The state is not changed. - **Error Condition**