Naslov: | Improved formal verification of SDN-based firewalls by using TLA+ |
---|
Avtorji: | ID Kapus, Tatjana (Avtor) |
Datoteke: | Improved_Formal_Verification_of_SDN-Based_Firewalls_by_Using_TLA.pdf (1,24 MB) MD5: 32497106BE3D1B3A72E0EBC708406B0B
https://ieeexplore.ieee.org/document/10265049
|
---|
Jezik: | Angleški jezik |
---|
Vrsta gradiva: | Članek v reviji |
---|
Tipologija: | 1.01 - Izvirni znanstveni članek |
---|
Organizacija: | FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
|
---|
Opis: | 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. |
---|
Ključne besede: | firewalls, formal specification, formal verification, logic, model checking, software defined networking |
---|
Status publikacije: | Objavljeno |
---|
Verzija publikacije: | Objavljena publikacija |
---|
Poslano v recenzijo: | 31.08.2023 |
---|
Datum sprejetja članka: | 23.09.2023 |
---|
Datum objave: | 27.09.2023 |
---|
Založnik: | IEEE |
---|
Leto izida: | 2023 |
---|
Št. strani: | str. 107126 - 107134 |
---|
Številčenje: | Vol. 11, vol. 11 |
---|
PID: | 20.500.12556/DKUM-86425  |
---|
UDK: | 004.5 |
---|
COBISS.SI-ID: | 166373891  |
---|
DOI: | 10.1109/ACCESS.2023.3320050  |
---|
ISSN pri članku: | 2169-3536 |
---|
Avtorske pravice: | 2023 The Authors |
---|
Datum objave v DKUM: | 04.12.2023 |
---|
Število ogledov: | 285 |
---|
Število prenosov: | 30 |
---|
Metapodatki: |  |
---|
Področja: | Ostalo
|
---|
:
|
Kopiraj citat |
---|
| | | Skupna ocena: | (0 glasov) |
---|
Vaša ocena: | Ocenjevanje je dovoljeno samo prijavljenim uporabnikom. |
---|
Objavi na: |  |
---|
Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše
podrobnosti ali sproži prenos. |