-
Notifications
You must be signed in to change notification settings - Fork 326
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Introduce malicious behaviour in ICS3 TLA+ spec. #70
Comments
Related branch that includes prior work on this issue: https://github.com/informalsystems/ibc-rs/commits/adi/ics3_tla_malicious |
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. |
It would be great to leave the faulty relayer's behavior unrestricted. @istoilkovska proposes to fix the scenario above as follows:
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:
|
Closing, as this is o longer relevant (#404 supersedes it). |
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:
correct parameters:
the following parameters:
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.
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.
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
The text was updated successfully, but these errors were encountered: