NetWords: Enabling the Understanding of Network Property Violation Occurrences
The problem of guaranteeing the absence of network connectivity property violations is investigated by combining the advantages of network monitoring for detecting property violations with the advantage of formal verification to model the network.
Abstract
A clear trend within the context of computer networks is the use of software as an alternative to specialized hardware. The benefit of this trend include an enhancement of flexibility, modularity, and maintainability of network components. Simultaneously, it is challenging to determine if everything is happening correctly in a computer network where software, possibly with bugs, is very present. Research in this field frequently tries to improve network testing with the use of formal verification techniques or network monitoring to detect property violations, such as configuration errors or policy conflicts. However, formal verification by itself cannot detect a property violation that was not anticipated and included in the model. Similarly, network monitoring needs to wait for a property violation to occur to detect it. Consequently, both enhancement efforts fail to achieve a complete result. In this paper, we investigate the problem of guaranteeing the absence of network connectivity property violations by combining the advantages of network monitoring for detecting property violations with the advantages of formal verification to model the network. A highlight related to the success of such a combination is the use of a model based on grammars to capture the communication patterns existing on the network. Our preliminary analysis allows the evaluation of high-level properties such as "Can network component x send HTTP packets?" and the detection of property violations, such as conflicting forwarding rules, as soon they occur in the network.