Validate coordinated head protocol against formal model

[ch1bo]

Why

Although the Hydra Head protocol has been peer-reviewed as a research paper and the security it provides proven, this does not guarantee our implementation indeed provides the same level of security. This is all the more true given we have been simplifying the "Simplified Head protocol" of the paper even further in collaboration with the original protocol researchers.

Therefore, we should validate the implementation of this "Coordinated Hydra Head" protocol, as we coined it, both from a theoretical standpoint (eg. does it provide the same security as the paper's protocol) and a practical standpoint (verifies the implementation is secure).

What

Within this feature we want to work toward enabling auditors to convince themselves that our implementation Hydra Head protocol is solid. To do so, we first need to convince ourselves by closing some known gaps in our testing strategy, namely the fact we don't have much coverage of the possibles sequences of actions in the head protocol.

How

Create such evidences by:

• Providing a (basic) executable model of the Hydra Head Protocol within an existing framework (eg. quickcheck-dynamic),

• Stating security properties from the paper,

• Quickchecking those properties hold for our current implementation,

• Validating the model and properties code against what's written in the research paper.

• One property is enough for a start.

Tasks

• Translate code into semi-formal notation for verification purpose #337
• Spike: Model-based testing of Hydra protocol using quickcheck-dynamic #375
• Spike: Model chain interaction layer using ContractModel #377
• Include Direct chain component in the Model-based testing stack #410
• Upgrade to quickcheck-dynamic 1.0.0 from hackage #466
• Express conflict-free liveness property using Dynamic Logic #467
• Extend QD Model to cover the whole head lifecycle -> have follow-ups instead
• Update Test strategy document and/or write extensive module documentation and/or write an ADR #641

[abailly-iohk]

I think this issue's priority should be raised and researchers pulled in ASAP to provide us static feedback, while Quviq works on contracts' certification

[ch1bo]

We plan to go through an example of our "HeadLogic" (after some refactoring maybe) with the original paper authors to find a common denominator to review the protocol logic.

[ch1bo]

After a quick tour of the code (mostly Hydra.HeadLogic) and the paper (mostly section 6.2) we identified the following

• We have implemented the "Coordinated" version of the Head protocol, which is not using individual transaction signing or socalled "hanging transactions" and currently is not formalized
• There is a good chance of drawing a parallel between the HeadLogic and the "off-chain" or protocol logic in the paper
• The on-chain verification from the paper is very different to the real world in cardano because it is not only verifying, but also "producing values"

Next steps:

• Write out the current version of Hydra.HeadLogic into similar pseudo code as in the paper (by IOG engineering)
• Separate OCV + "Chain/Head Interaction" from the protocol in the paper into actual verification and determining values ("glue code")

[ch1bo]

Changing to 🟡 as it's scope is actually unclear and we only get started on this one now.

[ch1bo]

@abailly-iohk This has become quite related/overlapping with #197 now. Shall we just ditch that one and capture our current tasks in this one? We ought to define the scope of this one also a bit better!

[ch1bo]

We discussed also that a kind of conformance test suite is actually an outcome of this! i.e. the model test can be used to perform actions against any implementation of a hydra-node (in fact, our e2e tests could be as well)

[pgrange]

Some notes from today's discussion about this tests.

The current situation with this test system:

• Emulates a perfect network and a perfect blockchain
• Does not validate L1 transactions

The current property that we check:

• Conflict free liveness

What we would like to do: Implement all the proofs from spec v1 as properties with this system

• Consistency
• Liveness
• Completeness

For that, we will need to:

• code the properties
• update the model with a network adversary
• update the model to validate L1 transactions
• update the model with an active adversary