VDD for Connection Handshake [master issue]

[adizere]

Summary

The idea is to use a verification-based approach at all steps of the development cycle of Connection Handshake.

Problem Definition

The goal is to catch bugs, prevent security problems, and finally obtain a formally verified implementation of Connection Handshake. To do so, this feature aims to align the development of Connection Handshake with our VDD approach. For a high-level description of how we will achieve this alignment, see VDD/#2 and the VDD/connection write-up.

Proposal

List of deliverables that we'll target to have in the current repository for the Connection Handshake problem:

• L1: High level English specification of the problem -- Connection Handshake: English specification of the problem #34
• L2: High-level English specification of system model -- Connection Handshake: English specification of system model #35
• L2: English description of the protocol -- Connection Handshake: English protocol description #36
• L2: TLA+ specification of the protocol -- TLA+ for IBC Connection handshake #4
• L2: TLA+ specification of properties -- handled in TLA+ for IBC Connection handshake #4
• L2: Abstract test scenarios unclear if this is useful at this moment; will be addressed potentially in later work.

---

For Admin Use

• Individual issues raised to track each subordinate deliverable
• Not duplicate issue
• Appropriate labels applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned