Formal Verification of SDN-Based Firewalls by Using TLA & x002B;
- Authors
- Kim, Young-Mi; Kang, Miyoung
- Issue Date
- 2020
- Publisher
- IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
- Keywords
- Tools; Network topology; Topology; Model checking; Firewalls (computing); Scalability; Companies; Firewall; formal methods; software-defined networking; TLA plus
- Citation
- IEEE ACCESS, v.8, pp.52100 - 52112
- Indexed
- SCIE
SCOPUS
- Journal Title
- IEEE ACCESS
- Volume
- 8
- Start Page
- 52100
- End Page
- 52112
- URI
- https://scholar.korea.ac.kr/handle/2021.sw.korea/58958
- DOI
- 10.1109/ACCESS.2020.2979894
- ISSN
- 2169-3536
- Abstract
- 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 & x002B;. We show that the firewall rule behavior of switches can be formalized using TLA & x002B;, and this is verified with the TLC model checker that uses TLA & x002B; 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.
- Files in This Item
- There are no files associated with this item.
- Appears in
Collections - ETC > 1. Journal Articles
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.