Formal Modelling and Verification of Software Defined Network
This work addresses the need for reliable SDN verification in cloud computing, but it is incremental as it applies existing formal methods to SDNs without novel breakthroughs.
The paper tackles the problem of ensuring correctness in software-defined networks (SDNs) for secure data transmission by using model-checking with CTL and LTL to formally verify SDN properties, resulting in a verified Kripke model of the SDN structure.
In cloud computing, software-defined network (SDN) gaining more attention due to its advantages in network configuration to improve network performance and network monitoring. SDN addresses an issue of static architecture in traditional networks by allowing centralised control of a network system. SDN contains centralised network intelligence module which separates a process of forwarding packets (data plane) from packet routing process (control plane). It is essential to ensure the correctness of SDN due to secure data transmitting in it. In this paper. Model-checking is chosen to verify an SDN network. The Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) used as a specification to express properties of an SDN. Then complete SDN structure is defined formally along with its Kripke structure. Finally, temporal properties are analysed against the SDN Kripke model to assure the properties of SDN is correct.