Formalize security properties of IBC in proof assistant

[cwgoes]

I think we should define IBC sufficiently rigorously that important security properties of the protocol can be checked in a proof assistant such as Idris, Coq, or Agda (there are likely other options too).

Some examples of the kinds of properties I think should be formalized:

• Packet replay prevention: given some set of chains correctly following the IBC protocol with arbitrary connections between them, and some correctly generated & authenticated IBC packet, prove that the packet can only be confirmed on one chain.
• Timeout semantics: given an IBC connection between two chains which may not necessarily make progress, prove that a packet is either committed (perhaps along with its receipt) on both chains or that a timeout can be submitted to the source chain.
• Masquerade prevention: given an IBC connection between two chains correctly following the IBC protocol, prove that a third malicious chain cannot masquerade (send packets from) as either of the two connected chains
• Byzantine fault handling: given a Byzantine fault committed by a validator set on one chain connected to a set of other chains, prove that this fault cannot affect chains which are not directly connected to the Byzantine chain (particularly w.r.t. multi-hop packet relay)

Open questions:

• What priority should this have? Should we try to formalize the protocol before implementing it or not?
• Which proof assistant is best (w.r.t. expressivity, ease of on-boarding, similarity to implementation)?
• How can we best provide proofs / primitives on top of which application-level security properties can be formalized?

[cwgoes]

Currently I am leaning towards Agda:

• A skilled type theory practitioner recommended it
• It's designed as more of a proof assistant (compared to Idris), which is what we want I think
• The syntax seems relatively easy to grasp (compared to Coq)

[cwgoes]

• How best to structure this with the ICS folder structure?

[cwgoes]

Also documentation should note relevant resources for understanding the proofs, e.g. this.

[cwgoes]

I have been doing some more research into this topic.

There are interesting theoretical developments referred to as "session types" (e.g. here, here) which can provide quite nice guarantees of progress & termination in concurrent contexts over channels. I think those might be quite useful in the context of analyzing application-level IBC protocol properties, as the channels provided by IBC have similar behaviour to channels in session types.

For formalization of the core IBC protocol I am reasonably convinced that Agda is the best fit.

I plan to start on core formalization after v1.0.0 is released.

[cwgoes]

I think it makes sense to accelerate this work instead of working on typechecked pseudocode.

[cwgoes]

Closing in favour of informalsystems/verification#12.