A Model Checking Based Approach for Detecting SDN Races

The paper is devoted to the verification of Software Defined Networking (SDN) components and their compositions. We focus on the interaction between three basic entities, an application, a controller, and a switch. When the application submits a request to the controller, containing a set of rules to configure, these rules are expected to be ‘pushed’ and correctly applied by the switch of interest. However, this is not always the case, and one of the reasons is the presence of races or concurrency issues in SDN components and related interfaces. We propose a model checking based approach for deriving test sequences that can identify SDN races. The test generation strategy is based on model checking, and related formal verification is performed with the use of extended automata specifying the behavior of the components of interest; Linear Temporal Logic (LTL) formulas are utilized to express the properties to check. We generalize the races of interest and propose an approach for deriving the corresponding LTL formulas that are later used for verifiation. The Spin model checker is used for that purpose and thus, Promela specifications for interacting components are also provided; those are: the ONOS REST API, the ONOS controller and an OpenFlow Switch. An experimental evaluation with the aforementioned components showcases the existence of race conditions in their compositions.