The new architecture of the TezEdge node: bridging the gap between formal specification and implementation
Whenever developing a system that controls critically-important data, security is paramount. To achieve the highest degree of security, we need to check for potential vulnerabilities in every possible case. A system like this may have many different states, and the more complex it is, the more states it can have.
To ensure the highest possible degree of security, we have to perform so-called exhaustive testing, in which we go through every possible state (every possible data combination) to leave no scope of further testing. In other words, if exhaustive testing is thoroughly executed, then all testing parameters will be covered. This is to say that we have full confidence that our system has all the intended desirable properties and no undesirable properties.
However, exhaustive testing is infeasible if the system is too complex, as is the case with the TezEdge node. In systems with this level of complexity, there are an astronomical number of states to check; complexity leads to state space explosion. In order to formally verify such a system, we need to create a mathematical representation of each part of the TezEdge node.
Writing such mathematical representations of the node was impossible due to the actor model-based architecture that we have used until now. For this reason, we needed to redesign the architecture in a way that would reduce the node’s complexity and allow us to write a representation of the node in TLA+, which we could then formally verify. There are various methods for performing formal verification, and in our case, we are using a formalism known as Temporal Logic of Actions (TLA+).
You can see how we used TLA+ for the node’s specification by clicking here.Differences between formal specification and implementation
However, the main problem of formal verification is that even if we have a...