kubasiemion
commented
5 years ago Closing, as we have agreed to include the relevant content into Glossary and Assumptions (meeting 31.07.2019)
Closed saltiniroberto closed 5 years ago
kubasiemion
commented
5 years ago Closing, as we have agreed to include the relevant content into Glossary and Assumptions (meeting 31.07.2019)
GPAv1 feedback The GPAv1 document states that the safety and liveness issues identified in the “Correctness Analysis of IBFT” paper are based on weak assumptions, lack practical evidence and the limitations cannot be concretely reproduced.
Reply Before starting the actual reply to the feedback I want to ensure that we are on the same page when using the adjective “weak”/”weaker” for describing assumptions. In this context, “weaker” means that we take “less things” for granted and therefore the protocol designed can cope with a wider range of situations. For example, we assume an eventual synchronous network model, a stronger assumption would be assuming a synchronous network model where it is guaranteed that messages are always transmitted within a known message delay. All of the assumptions used by the "Correctness Analysis of IBFT” are precisely stated in its Section 2. These assumptions define the system model including network model, adversarial model and cryptographic assumptions. If there is a concern that some of the assumptions are too weak (i.e. that we can actually assume more guarantees than what is assumed in the “Correctness Analysis of IBFT” paper), then it must be clearly stated which of the assumptions are too weak and to which extent they can be strengthened (I.e. made more restrictive). To this effect we note that GPAv1 agrees with the “Correctness Analysis of IBFT” paper on the network model (which is one of the most important assumptions for the analysis): “The definition of the eventually synchronous network applies to the blockchain model and appears to be accurate.” (see bottom of page 1 of GPAv1). See Issue #4 for a discussion on the choice of the network model.
Once the set of assumptions describing how we expect the real environment to behave is identified, then if a sequence of events leading to a non-safe situation or a deadlock is identified, given that this scenario is allowed by the assumption describing how the real environment is expected to behave, it means that the scenario can realistically happen.
In summary, once the system model and its set of assumptions describing how the real environment is expected to behave is defined, if a scenario leading to a "bad" situation is identified, there is no need to spend time and energy in reproducing the scenario in practice because we already know that it can happen. Also if we know that a given protocol may not behave correctly in some scenarios and we know how to fix it, why do not fix it?