Formal Modeling And Verification Of Software-defined Networking

Software-Defined Networking(SDN)is a new network architecture,which can solve the problems of traditional network,for example,the high complexity that makes it difficult for management and innovation.SDN separates the control logic from the forwarding devices to compose a logical central controller,providing programmability of the network.The emergence of SDN not only promotes the iteration of network architecture,but also brings the revolution of network development.In the future,formal methods must play an extremely important role in the field of network development.In this thesis,we model and verify SDN by formal methods.To support model checking of the properties for forwarding logic,we extends the well-known SDN programming language NetKAT to propose a more expressive language PDNet,which can describe Virtual Local Area Network(VLAN).Then we study the operational semantics of PDNet,and prove the relationship and difference between PDNet and NetKAT based on operation semantics.In order to discover the design,functionality and safety related problems in SDN,we propose the system modeling framework based on the process algebra CSP,which is proposed by Professor C.A.R.Hoare,a Turing prize winner.We also implement the framework in the model checker PAT.To show the usage and practical value of the framework,we model and verify the open-source controller Floodlight and the secure controller TopoGuard.The main contributions of this thesis include:· We propose a new network programming language PDNet based on Kleene algebra(KA)to describe the forwarding logic of data layer.PDNet extends the advanced network programming language NetKAT,to describe software-defined networks that support VLAN tags.We also study the operation semantics of PDNet based on pushdown system.Not only PDNet automata,but also a syntactic derivative is defined.In addition,we prove that PDNet is more expressive than NetKAT.· We summarize and classify the software and hardware devices in the three-tier architecture of SDN as well as the external environment to propose a parameterized system modeling framework based on CSP.Besides,we propose an instantiable data layer model,four kinds of host models,and two kinds of attack models.Moreover,we provide the modeling schemes for nine kinds of possible attacks in SDN.· We model and verify six basic modules of Floodlight as well as the attack defense mechanism of TopoGuard.For Floodlight,we verify the design,functionality and security related properties.The verification results show that the topology discovery and device management methods of Floodlight,which are used by almost all the open-source controllers,are vulnerable to two kinds of attacks.So,we verify TopoGuard,a security controller designed to defend against the two attacks.Two serious loopholes are found.At the last,we give an improvement mechanism based on the verification results and simulation.