Formal Verification of SDN-Based Firewalls by Using TLA+

Software-defined networking (SDN) has generated increased interest due to the rapid growth in the amount of data generated by the development of the Internet and communications, the commercialization of 5G, and increasingly complex networks. While SDN is more advantageous than traditional networks in terms of efficient network management, rapid deployment, and dynamic scalability, the correctness of a network configuration must be ensured in advance. In other words, SDN components such as network devices, SDN controllers, and applications need to be deployed correctly and must be free of rule conflicts, particularly between various application policies; otherwise, it may result in network paralysis in the worst case. This paper assumes that the SDN network is free of rule conflicts when the rules in the SDN switches correctly obey firewall application or policies. To solve this problem, this paper proposes a verification framework for SDN using TLA+. We show that the firewall rule behavior of switches can be formalized using TLA+, and this is verified with the TLC model checker that uses TLA+ as the model description language. We check two different types of topology models through our verification framework to ensure that the same firewall rules are maintained even if the topology changes. The findings show that the firewall rules may be inconsistent as the topology changes.