The flexibility and dynamism brought over by softwarization for network management have increased the frequency of configuration changes. In this context, when a distributed security function is subject to a series of configuration changes, a problem that arises is the preservation of the security. The transient from the application of the first change to the last one may present unsecure temporary states, where the required security protection is missing. Establishing a safe scheduling of the configuration changes can significantly limit the number of unsecure states and decrease the time period where the network may be at risk. However, the literature challenged this problem only for centralized firewalls or SDN switches, and without applying formal methods to ensure the correctness of the computed scheduling. In order to overcome these limitations, this paper addresses the problem for distributed firewalls, aiming to satisfy the largest number of user-specified network security policies in each transient state. To this end, it proposes a formal methodology relying on the combination of three main features: automation, formal verification and optimization. This combination is achieved by pursuing a correctness-by-construction approach, based on the formulation of a Maximum Satisfiability Modulo Theories problem. A framework has been developed on the basis of this methodology, so that validation tests have been experimentally executed to assess the feasibility, efficacy and scalability of the approach.

Optimizing distributed firewall reconfiguration transients / Bringhenti, Daniele; Valenza, Fulvio. - In: COMPUTER NETWORKS. - ISSN 1389-1286. - ELETTRONICO. - 215:(2022). [10.1016/j.comnet.2022.109183]

Optimizing distributed firewall reconfiguration transients

Daniele Bringhenti;Fulvio Valenza
2022

Abstract

The flexibility and dynamism brought over by softwarization for network management have increased the frequency of configuration changes. In this context, when a distributed security function is subject to a series of configuration changes, a problem that arises is the preservation of the security. The transient from the application of the first change to the last one may present unsecure temporary states, where the required security protection is missing. Establishing a safe scheduling of the configuration changes can significantly limit the number of unsecure states and decrease the time period where the network may be at risk. However, the literature challenged this problem only for centralized firewalls or SDN switches, and without applying formal methods to ensure the correctness of the computed scheduling. In order to overcome these limitations, this paper addresses the problem for distributed firewalls, aiming to satisfy the largest number of user-specified network security policies in each transient state. To this end, it proposes a formal methodology relying on the combination of three main features: automation, formal verification and optimization. This combination is achieved by pursuing a correctness-by-construction approach, based on the formulation of a Maximum Satisfiability Modulo Theories problem. A framework has been developed on the basis of this methodology, so that validation tests have been experimentally executed to assess the feasibility, efficacy and scalability of the approach.
File in questo prodotto:
File Dimensione Formato  
AcceptedManuscript.pdf

Open Access dal 17/07/2024

Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: Creative commons
Dimensione 639.37 kB
Formato Adobe PDF
639.37 kB Adobe PDF Visualizza/Apri
1-s2.0-S138912862200281X-main.pdf

non disponibili

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 1.25 MB
Formato Adobe PDF
1.25 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2970045