Actor-Based Model Checking and Analysis of Software Defined Networks by Rebeca

Abstract: Today, computer networks are an integral part of our lives, and the quality of services provided on these networks directly affects our quality of life. We are moving towards a future where even sensitive services like surgery can be performed online through networks. Therefore, we need networks that not only have correct functionality but also have higher reliability than traditional networks in order to ensure the quality of services (QoS). To this end, major companies such as Google, Amazon, Cisco, etc., have moved towards networks known as Software Defined Networks (SDN), which, unlike traditional networks, have programmability and high management capabilities to guarantee QoS. Alongside the ease of use and agility of SDN, there are also undesirable aspects. In fact, alongside the possibility of programming, the possibility of errors also exists. Therefore, we need to ensure the correctness of the program we have written to control the network. In this research, we have taken a step towards preventing undesirable events in mission-critical applications of SDN. Traditional methods for detecting errors in SDN, such as manual inspections, simulations, and repeated executions, despite their advantages, are unable to guarantee the detection of all errors due to the inherent concurrency existing in networks as distributed systems. Some errors occur under very specific and rare conditions that cannot be identified through simulations. To verify the correctness of the operation of these networks under critical conditions, a precise and less addressed approach is to provide an abstraction model of the network and ensure its functionality in all conditions by examining all possible states or using model checking. In this research, using the modeling language called Rebeca, we have developed methods for analyzing and debugging applications and common scenarios used in SDN. These methods model the topology and application scenario in the form of a Rebeca model and use supporting tools like Afra to validate the model and examine the correctness of these scenarios. If an error is found, it will be reported in the form of a series of actions or events that led to this error. Furthermore, we have proposed a synthetic algorithm that, in some cases, can find a way to prevent congestion in SDNs during dynamic updates of data flow paths. Keywords: software defined network, Rebeca, model checking, formal verification, Actor, Congestion