Model Based Testing for Programmable Data Planes

Sammanfattning: The advent of Software Defined Networking (SDN) and programmable data planes has revolutionized the networking domain, enabling the programming of networking functions down to the silicon level responsible for data packet switching. Unfortunately, while this programmability offers greater flexibility and control, it also increases the likelihood of introducing software bugs. To counter this risk, rigorous testing methodologies and strategies are essential to ensure the reliability, security, and stability of SDN deployments. A comprehensive approach should combine various techniques, including formal verification, fuzz, and performance testing. Model-Based Testing (MBT) is a technique that can significantly enhance the effectiveness of SDN testing. By leveraging formal models of the system under test, MBT automatically generates test cases that can help identify potential issues in network configuration, data plane programming, and network protocols. Utilizing MBT allows network administrators to systematically explore SDN components’ possible states and transitions, resulting in a higher level of coverage and confidence in the system’s overall stability and security. However, a lack of information on applying MBT in an SDN environment challenges its full implementation and utilization in this field. This master thesis aims to investigate and demonstrate the application of MBT to programmable data plane functions. This work uses VLAN tagging as the target data plane function, and AltWalker is employed as the MBT tool for generating and executing tests on an SDN switch. The results present an initial testing methodology that, when applied to the VLAN tagging function, can provide insights into the potential benefits and challenges of using MBT for SDN testing. This thesis lays the groundwork for further exploration and refinement of MBT methodologies in the context of SDN and programmable data plane functions.