English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

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.

Formal Verification of SDN-Based Firewalls by Using TLA+