NUK - logo
Library of Technical Faculties, Maribor (KTFMB)
  • Improved formal verification of SDN-based firewalls by using TLA+ [Elektronski vir]
    Kapus, Tatjana
    In an article published in IEEE Access in 2020, researchers present an approach to using TLA + for the formal verification of whether a network of SDN (Software-Defined Networking) switches ... implements the filtering rules of a given monolithic firewall. The distributed as well as monolithic firewalls are specified with TLA + . It is shown that the correctness of the former with respect to the latter can be verified automatically by using the TLC model checker. The main contributions of this paper are the following improvements of that approach. Firstly, by specifying switches without using any variables, the time needed for the model checking is reduced significantly. For example, the verification of the same networks takes a few seconds with the new approach and does not end after several hours with the previous one. Secondly, the following problem is solved. With the latter, if a monolithic firewall allows a packet to pass through, all the paths in the distributed firewall which the packet is routed on must allow the same. Otherwise, the model checker proclaims the distributed firewall to be in error. We present an additional approach to the verification, which gives a positive answer if at least one of the paths allows the packet to pass through.
    Source: IEEE access [Elektronski vir]. - ISSN 2169-3536 (Vol. 11, 27 September 2023, str. 107126 - 107134)
    Type of material - e-article ; adult, serious
    Publish date - 2023
    Language - english
    COBISS.SI-ID - 166373891

    Link(s):

    Digital Library of the University of Maribor – DLUM
    DOI

Shelf entry