Cyber attacks have been continuously becoming more frequent and powerful in modern computer networks, which interconnect a huge number of devices, including mobile ones. A main reason explaining the effectiveness of the attacks lies in the errors introduced by human administrators in the configuration of network security functions such as firewalls and VPN gateways. In literature, formal methods were used to check if a security configuration satisfies the policies describing the security properties to be enforced in the network. However, most existing proposals use a-posteriori formal verification, which still requires multiple tasks to be carried out by human administrators and may be time-consuming. In order to overcome these limitations, we have carried out research toward applying correctness-by-construction approaches for network security configuration. In this paper, we survey our most relevant contributions to this area, describing techniques based on constraint programming, like MaxSMT formulations, for a formal representation and resolution of the automatic security configuration problem, in such a way that the computed result is already proved to be correct and compliant with the requested policies.

Toward Correctness by Construction for Network Security Configuration / Bringhenti, Daniele; Sisto, Riccardo; Valenza, Fulvio. - ELETTRONICO. - 2597:(2026), pp. 391-404. (Intervento presentato al convegno The 8th International Conference, MobiSec 2024, Sapporo, Japan, December 17–19, 2024 tenutosi a Sapporo (JPN) nel December 17–19, 2024) [10.1007/978-981-95-0172-4_26].

Toward Correctness by Construction for Network Security Configuration

Bringhenti, Daniele;Sisto, Riccardo;Valenza, Fulvio
2026

Abstract

Cyber attacks have been continuously becoming more frequent and powerful in modern computer networks, which interconnect a huge number of devices, including mobile ones. A main reason explaining the effectiveness of the attacks lies in the errors introduced by human administrators in the configuration of network security functions such as firewalls and VPN gateways. In literature, formal methods were used to check if a security configuration satisfies the policies describing the security properties to be enforced in the network. However, most existing proposals use a-posteriori formal verification, which still requires multiple tasks to be carried out by human administrators and may be time-consuming. In order to overcome these limitations, we have carried out research toward applying correctness-by-construction approaches for network security configuration. In this paper, we survey our most relevant contributions to this area, describing techniques based on constraint programming, like MaxSMT formulations, for a formal representation and resolution of the automatic security configuration problem, in such a way that the computed result is already proved to be correct and compliant with the requested policies.
2026
9789819501717
9789819501724
File in questo prodotto:
File Dimensione Formato  
MobiSec_Accepted_Manuscript.pdf

embargo fino al 15/10/2026

Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: Pubblico - Tutti i diritti riservati
Dimensione 1.31 MB
Formato Adobe PDF
1.31 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
MobiSec_vor.pdf

accesso riservato

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 1.54 MB
Formato Adobe PDF
1.54 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/3003972