The Research Of Network Verification Method Based On The Header Space Of Packets In SDN

Nowadays,the network structure becomes more and more complicated,which leads to the error-prone of the configuration.In the world of network,the cost of solving network failures is a debilitating source of operational expenditures.Recently,network verification and testing has got an increasing interest in the academic community.In addition,Software Defined Networking(SDN)has been proposed for improving network flexibility and programmability by decoupling control plane and data plane of the network.The centralized observation of the data plane of the network provides the opportunity to verify network behaviors automatically and dynamically.In the field of network data plane verification and testing,SDN makes it possible to perform realtime data plane verification and testing.On the other hand,it raises a new requirement to quickly verify and test the data plane in real-time.Most of the former verification tools on the data plane are suffered from the problem of bad scalability and dynamic performance.They are hard to be extended in the multi-fields or the multi-layers SDNs.Therefore,we proposed the Pre Checker to dynamically identify the conflicting rules and divide the rules into equivalence classes(ECs)in real-time.Then we extend the MTBDD based ECs dividing method into the field of network testing.It improves the dynamic performance of the generation of the testing packets.Then we model the SDN network based on the Header Space and propose the algorithm to dynamically maintain the information of reachability.The prototype Net V has been implemented for the network verification.At last,some common network invariants are represented by this model and then verified by the Net V.It improves the dynamic performance of the dynamic performance of the verification of the network invariant violation in real-time.The main contributions of this thesis are:1)We redefine the intra-switch(table)conflicts with action sets.It narrows the intra-switch conflict to the incompatibility in the exact match field.We leverage the MTBDD to maintain ECs.The incrementally updating algorithm is proposed for effectively partition ECs when updating rules in real-time.The Pre Checker is implemented and applied to the verification tools as the preprocessing for speeding up the verification.2)We extend the MTBDD based partition method to incrementally generate the test packets in the field of data plane testing.We redesign the structure and the operation between the terminal nodes of MTBDD based on the requirement of the test packets.The MTBDD based method can improve the incremental generating efficiency3)We define the network model based on the Header Space.We first define the composition of actions on header space,which makes the connection of rules can be represented by the composition of the functions.Then we design an algorithm for applying the modify action on a BDD.We leverage the advantage of the BDD expression to merge rules in same switch by their action sets,which removes the redundancy of the rule set.The connection matrix is used to represent the connections of rules.We propose the incremental updating algorithms for verifying the reachability requirements when rules are inserting to the network.The prototype Net V is also implemented.4)Some common network invariants are represented by this model and then verified by the Net V by using the incremental updating method.We further extend this model for the network of multilayer controller.The information of the intra-domain paths is hided,whereas the inter-domain information can be captured by the controller of this layer.The interdomain invariants can also be verified by using the incremental updating method with NetV.