Formalization And Verification Of OpenFlow Bundle Mechanism Based On CSP

Software-Defined Networking(SDN)is a new form of networking architecture,which is different from the traditional networks.It breaks the limitation of the traditional networks and realizes the flexibility and programmability of the network management.The control panel and the data panel of traditional networks are closely integrated,which makes it difficult to configure and manage the complex networks,hindering the innovation and evolution of the networking infrastructure.SDN makes the breakthrough to centralize the management.It separates the control logic of network from the underlying devices of the data panel.It simplifies these devcise tasks to forward data and centralize the control logic in the controller(or networking operating system).The controller can directly manage the network and interact with the data panel.OpenFlow protocol is one of the core technologies of SDN and is one of the most ideal underlying implementation of SDN as well.OpenFlow protocol simplifies the management of networks and optimize the consistency and accuracy of the configurations.It has gained important influence in the whole world and has broad application prospect.At the same time,it also raises the requirements of network security and reliability.The object of this paper is OpenFlow Bundle Mechanism.It is a new mechanism proposed by OpenFlow protocol to improve security by guaranteeing the completeness and consistency of the message transmission.Based on the trustworthy property of formal methods and the need of security and reliability of OpenFlow protocol,we use Communication Sequential Processes(CSP)to formally verify and analyze the mechanism.We complete the abstraction modeling of components in the system.We respectively complete the CSP modeling of the three components,controller,switch and bundle.We also build the connection between the components to complete the formal modeling of the whole system.Next,we use the model checker Process Analysis Toolkit(PAT)to automatically simulate and verify the established CSP model.According to the verification results,we conclude that the five properties of the mechanism is valid,including Deadlock Freeness,Atomicity,Order Property,Parallelism and Schedulability.The strict and complete mathematical model theory proves that OpenFlow Bundle Mechanism can guarantee the consistency and completeness of transmission.Finally,we introduce a case study with the intruder's attack in real network.We specify the behavior of the intruder and add it into the established model.After verifying and analyzing of attacks,we discover the insecurity of the mechanism and put forward the practical optimization solution to improve security and reliability of OpenFlow protocol.