Introduce malicious behaviour in ICS3 TLA+ spec.

[adizere]

Summary

We would like to model malicious behavior as part of ICS3 spec.

Problem Definition

Preliminary work on this has been started on the following branch: https://github.com/informalsystems/ibc-rs/tree/adi/ics3_tla_malicious
as part of the work in #58.

Discussion from ongoing work

Initially, the environment is non-malicious. The environment starts
acting maliciously once the connection on both chains transitions out
of state "UNINIT" (the initials state). It is important to
initialize the protocol like this, otherwise the env. can provoke a
deadlock. This can happen with the following sequence of actions:

1. Environment injects a ICS3MsgInit to chain A with the following
   correct parameters:

    localEnd |-> [connectionID |-> "connAtoB",
                  clientID |-> "clientIDChainB"]
    remoteEnd |-> [connectionID |-> "connBtoA",
                   clientID |-> "clientIDChainA"]

2. Environment injects, maliciously, a ICS3MsgInit to chain B with
   the following parameters:

    localEnd |-> [connectionID |-> "connBtoA",
                  clientID |-> "clientIDChainA"]
    remoteEnd |-> [connectionID |-> "connBtoA",
                   clientID |-> "clientIDChainA"]

Notice that the localEnd is correct, so chain B will validate and
process this message; the remoteEnd is incorrect, however, but chain
B is not able to validate that part of the connection, so it will
accept it as it is.

3. Chain A processes the ICS3MsgInit (action HandleInitMsg) and
   updates its store.connection with the parameters from step 1 above.
   At this point, chain A "locks onto" these parameters and will not
   accept any others. Chain A also produces a ICS3MsgTry message.

4. Chain B processes the ICS3MsgInit (action HandleInitMsg) and
   updates its store.connection with the parameters from step 2 above.
   Chain B "locks onto" these parameters and will not accept any others.
   At this step, chain B produces a ICS3MsgTry message with the local
   parameters from its connection.

Both chains will be locked on a different set of connection parameters,
and neither chain will accept their corresponding ICS3MsgTry, hence a
deadlock. To avoid this problem, we prevent the environment from
acting maliciously in the preliminary parts of the ICS3 protocol, until
both chains finish locking on the same set of connection parameters.

---

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned

[adizere]

Related branch that includes prior work on this issue: https://github.com/informalsystems/ibc-rs/commits/adi/ics3_tla_malicious

[istoilkovska]

As far as I understand from your example above, the sequence of steps that causes a deadlock is not due to the malicious environment, but to the protocol itself. Selectively turning a faulty environment on or off may cause the specification to ignore some undesirable behaviors of the protocol that can appear in the implementation. The faulty environment is unpredictable and non-deterministic, and in my opinion, its behavior in the specification should not be restricted. Maybe it is better to rather think about how to improve the protocol and the specification such that it deals with this scenario.

[adizere]

The faulty environment is unpredictable and non-deterministic, and in my opinion, its behavior in the specification should not be restricted.

It would be great to leave the faulty relayer's behavior unrestricted. @istoilkovska proposes to fix the scenario above as follows:

One easy fix that comes to mind is that a chain should discard datagrams that have the same connection ID in both fields localConnectionID and remoteConnectionID. This is a purely syntactic check on the local chain side, and does not require checking if remoteConnectionID is a valid connection ID.

This fix has the advantage that it permits arbitrary behavior for malicious relayer(s). The disadvantage is that we're adding a syntactic check that might not be in line with the ICS3 module implementation. To summarize, I think the problem in this scenario arises because we’re capturing a single connection. It seems like we have two options at the moment:

1. Prevent the relayer from initializing two distinct connections on each chain, or
2. A syntactic check along the lines proposed above.

[adizere]

Closing, as this is o longer relevant (#404 supersedes it).