TLA+ specification of packet delay

[istoilkovska]

Summary

We want the following invariant to hold: packet-related data should be accepted only after some delay has passed since the corresponding header is installed. This allows a correct relayer to intervene if the header is from a fork and shutdown the IBC handler, preventing damage at the app level.

Problem Definition

cosmos/cosmos-sdk#8069
cosmos/ibc#507

High level use case: users are making token transfer from Cosmos Hub to an exchange zone. Once a lot of tokens are moved to a zone, the zone validators create invalid packet to steal tokens from the user by making single transfer from a zone to a hub.

Proposal

First solution (wrong)

Add a packet delay field to the packet data structure so users can configure it based on needed security level. The verification function depends on the specified packet delay. The issue is the fact that an attacker can create fake packet with 0 delay specified.

Second solution

Packet delay is enforced at the connection level.
Let t1 and t2 be BFT times of zone 1, with t2 >= t1. These timestamps are part of blockchain headers of zone 1.
Suppose t1 is the time at which a header h is installed at zone 1, and t2 is the time at which a packet is verified using the header h. We need to ensure that t2 - t1 > delay, where delay is some previously defined constant.

When a packet p that can be verified using a header h installed at time t1 is sent to zone 1, a correct relayer should not submit a PacketRecv datagram before it sees that on zone 1 the BFT time is greater than t1 + delay.

An attacker with more than 1/3 of voting power may:

1. create an arbitrary client state update with a lunatic attack. Then it can submit this client state update to a destination chain, which will go through verification and will be installed in the client state of the destination chain. This implies, that we have an invalid consensus state, i.e., the app hash is invalid.
2. any packet-related data, which references this invalid consensus state and which is correct with respect to the fake app hash will be verified.

While (1) cannot be prevented, we can prevent (2) by adding delay. In this case, a correct relayer can monitor the chain, and once it detects (1), it can submit evidence of misbehaviour and shut down the IBC handler, so no packet referencing the invalid consensus state is processed.

Proposed solution in TLA+

• Add a timestamp field to each chain store, that simply counts how many steps the chain has taken.
• Modify the counterpartyClientHeights to be a function from installed heights to timestamps instead of a set of installed heights.
• When a relayer creates packet datagrams, it puts them in a pending queue. Add an additional relayer step in which it scans the pending queue and depending on the current timestamp at the destination chain, as well as the specified delay, it submits the datagrams after the delay has passed.
• The delay is a parameter of the connection between two chains.

---

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate milestone (priority) applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned