| Title: | Improved formal verification of SDN-based firewalls by using TLA+ |
|---|
| Authors: | ID Kapus, Tatjana (Author) |
|---|
| Files: |  Improved_Formal_Verification_of_SDN-Based_Firewalls_by_Using_TLA.pdf (1,24 MB)
MD5: 32497106BE3D1B3A72E0EBC708406B0B
 https://ieeexplore.ieee.org/document/10265049
|
|---|
| Language: | English |
|---|
| Work type: | Article |
|---|
| Typology: | 1.01 - Original Scientific Article |
|---|
| Organization: | FERI - Faculty of Electrical Engineering and Computer Science
|
|---|
| Abstract: | 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. |
|---|
| Keywords: | firewalls, formal specification, formal verification, logic, model checking, software defined networking |
|---|
| Publication status: | Published |
|---|
| Publication version: | Version of Record |
|---|
| Submitted for review: | 31.08.2023 |
|---|
| Article acceptance date: | 23.09.2023 |
|---|
| Publication date: | 27.09.2023 |
|---|
| Publisher: | IEEE |
|---|
| Year of publishing: | 2023 |
|---|
| Number of pages: | str. 107126 - 107134 |
|---|
| Numbering: | Vol. 11, vol. 11 |
|---|
| PID: | 20.500.12556/DKUM-86425  |
|---|
| UDC: | 004.5 |
|---|
| ISSN on article: | 2169-3536 |
|---|
| COBISS.SI-ID: | 166373891 |
|---|
| DOI: | 10.1109/ACCESS.2023.3320050 |
|---|
| Copyright: | 2023 The Authors |
|---|
| Publication date in DKUM: | 04.12.2023 |
|---|
| Views: | 451 |
|---|
| Downloads: | 56 |
|---|
| Metadata: |    |
|---|
| Categories: | Misc.
|
|---|
|
:
|
Copy citation |
|---|
| | | | Average score: | (0 votes) |
|---|
| Your score: | Voting is allowed only for logged in users. |
|---|
| Share: |  |
|---|
Hover the mouse pointer over a document title to show the abstract or click
on the title to get all document metadata. |
