Modeling and Verifying Basic Modules of Floodlight

Software-Defined Networking (SDN) is an emerging networking paradigm that provides flexible network programmability and reduces the complexity of network management and control. OpenFlow Protocol is the best-known southbound interface of SDN. As one of the most popular OpenFlow controllers, Floodlight is famous for its excellent basic modules, which are used by many other mainstream controllers. Due to the popularity and widespread use of the Floodlight’s modules, it is important to analyze them in a formal framework. In this paper, we focus on six modules of Floodlight that are mainly responsible for pushing decisions and discovering topology. In order to verify whether these modules meet two important requirements, including Decision Pushed Correctly and Rule Installed Once, we propose a system model that formalizes these modules as well as hosts and switches using Communicating Sequential Processes (CSP). Moreover, we add two types of attacks: Link Fabrication and Host Hijacking, which aim at poisoning the topology information collected by a controller, to construct a second system model. Finally, we implement these two system models in Process Analysis Toolkit (PAT), a model checker, to verify whether our models cater for four assertions based on two requirements and if Floodlight is vulnerable to these two attacks.