Formal models of software-defined networks

Feng, H. (2024)

Doctoral Thesis

SDN (Software-Defined Networking) represents a revolutionary approach to network architecture that enables the dynamic and flexible management of network resources through software-based control. This dissertation introduces the idea of SDN and its southbound protocol OpenFlow, then presents the formal expressions for them. We first introduce a coordination language Reo and its operational semantics constraint automata, they provide a rigorous and flexible framework for modelling the intricate behaviours of SDNs. To verify this formal model by SPIN model checker, we also give a translation of symbolic constraint automata used in our model of SDNs to Promela. This translation facilitates the formal verification of essential SDN characteristics, including reachability, consistency, and the correctness of network policies. Moreover, we extend NetKAT, a formal language for specifying network policies, to support concurrency through the introduction of ports. This extension enhances NetKAT’s capability to model stateful and concurrent systems, aligning it with the Reo-based formalism and broadening its applicability to more complex SDN scenarios. To pioneer the integration of causality reasoning into SDN models, detecting and removing the hazardous events in a railway crossing system is the first step towards causal reasoning for SDN, it lays the groundwork for more sophisticated causality analyses in future work.

• Software-Defined Networks
• Reo
• Formal methods
• Formal verification
• Model checking
• Constraint automata
• Railway crossing system
• Causality
• Concurrent NetKAT
• Promela

• All authors: Feng, H.
• Supervisor: Bonsangue, M.M.
• Committee: Barbosa, L.; Sirjani, M.; Boer, F. de; Kleijn, J.; Plaat, A.; Chen, Q.
• Qualification: Doctor (dr.)
• Awarding Institution: Leiden Institute of Advanced Computer Science (LIACS), Faculty of Science, Leiden University
• Date: 2024-12-03
• ISBN (print): 9789036107815