| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava

Izpis gradiva Pomoč

Naslov:Improved formal verification of SDN-based firewalls by using TLA+
Avtorji:ID Kapus, Tatjana (Avtor)
Datoteke:.pdf Improved_Formal_Verification_of_SDN-Based_Firewalls_by_Using_TLA.pdf (1,24 MB)
MD5: 32497106BE3D1B3A72E0EBC708406B0B
 
URL 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 Novo okno
UDK:004.5
COBISS.SI-ID:166373891 Novo okno
DOI:10.1109/ACCESS.2023.3320050 Novo okno
ISSN pri članku:2169-3536
Avtorske pravice:2023 The Authors
Datum objave v DKUM:04.12.2023
Število ogledov:285
Število prenosov:30
Metapodatki:XML DC-XML DC-RDF
Področja:Ostalo
:
Kopiraj citat
  
Skupna ocena:(0 glasov)
Vaša ocena:Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
Objavi na:Bookmark and Share


Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše podrobnosti ali sproži prenos.

Gradivo je del revije

Naslov:IEEE access
Založnik:Institute of Electrical and Electronics Engineers
ISSN:2169-3536
COBISS.SI-ID:519839513 Novo okno

Gradivo je financirano iz projekta

Financer:ARRS - Agencija za raziskovalno dejavnost Republike Slovenije
Številka projekta:P2-0069
Naslov:Napredne metode interakcij v telekomunikacijah

Licence

Licenca:CC BY 4.0, Creative Commons Priznanje avtorstva 4.0 Mednarodna
Povezava:http://creativecommons.org/licenses/by/4.0/deed.sl
Opis:To je standardna licenca Creative Commons, ki daje uporabnikom največ možnosti za nadaljnjo uporabo dela, pri čemer morajo navesti avtorja.

Sekundarni jezik

Jezik:Slovenski jezik
Ključne besede:požarni zid, formalna specifikacija, formalna verifikacija, preverjanje modelov


Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)
0 - 0 / 0
 
Ni komentarjev!

Nazaj
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici