Research On SDN Testing And Invariant Verification Based On Network States

Along with the concept of "Internet plus",informatization plays an increasingly important role in social production and life.Among them,the network plays a central role as an important carrier and specific means to promote information interaction.In the current context of resource pooling,new concepts are constantly being put forward.With the appearance of new network paradigms,the network dimension has expanded from the initial land-based network to sea-based network,space-based network,and sky-based network.While the network is becoming more and more important,its form of expression is becoming more and more complex.Therefore,how to continuously ensure the correctness of the underlying network and provide a reliability guarantee for the upper application not only plays an important role in network engineering and network maintenance but also increasingly highlights its position in the academic research of network theory.The state-based network testing and the network invariant verification are studied in a software-defined network environment.The research work includes the following three parts: the research of network state in a software-defined network environment,the research of network behavior formal model and path sequence generation,and the research of network invariant verification based on path matrix.Through the study of network state,the overall network situation is obtained.Under its guidance,the constraint-based formal modeling is carried out,and the path sequence is obtained.Then the path matrix is constructed to test Open Flow protocol.With the path matrix,the network invariants are verified to judge whether the underlying network behavior is correct or consistent with the user's needs.In this dissertation,the module of Floodlight is expanded for support network invariant verification.The main work and innovative results of this dissertation are as follows:1.The definition of network global state view and the expansion algorithm of state view stack is proposed.After analyzing the network state according to the Internet architecture,the concepts and formal definitions of unified network state view and network state view stack are proposed.Combined with the above concepts,the algorithm of constructing the global state view of the network and the algorithm of expanding the network state view stack are proposed.The application of the above view and view stack with the application of "knocking door" in the network are illustrated.From the result,the generality of the above expansion algorithm is displayed.Logically,the algorithm can analyze the network state from whole dimensions,and expanding the state view stack continuously.It can provide a solid underlying state data guarantee for the network in software-defined network environment.2.A constraint-based sequence generation algorithm is proposed to increase the fitting degree of the model.Building a network model based on concerns problem is an important means in network research.The follow-up research relies on the built model,such as the corresponding verification and testing worked.Therefore,how to build the network model and make the built model more closely fit with the actual requirements is a problem that needs to be focused in the network research.In this dissertation,a constraint-based sequence generation algorithm is proposed.It adds constraint information to the network model and also modifies the constraints according to feedbacks,which makes the network model more closely fitted with the actual situation.After that Open Flow protocol is taken as an example to illustrate the validity of the above constraint-based network model.The testing of the Open Flow protocol is carried out.Finally a test system framework is proposed based on the formal guidance and implemented,and the framework is expanded to support different test methods.3.A network invariant verification algorithm is proposed based on path matrix.A general formal definition of network invariants are proposed.Combined with the verification process of network invariants,a network invariants verification algorithm based on a path matrix is putting forward.The specific definitions of network invariants involved in common network scenarios are given,and the invariants verification algorithm is used to realize the above invariants verification.In the software-defined network environment,the verification process of invariants is carried out for the verification of properties of network such as forwarding loop invariants,network black hole invariants,network multipath consistent priority invariants,network reachability invariants,network isolation invariants,network path disjoint invariants,network boundedness invariants and so on.The validity of the algorithm in this dissertation is proved with positive results.After reading all the source code of Floodlight,the corresponding functional modules are expanded and the formal modeling module is increased.Based on integrating the constraints-based modeling process,the global network state view and state view stack are constructed to serve the upper network applications.To ensure the correctness of the underlying network,an open and easily expanded underlying data structure is established.A verification and test plane is logically constructed from the view of the software-defined network to continuously verify the running state of the network.