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.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.
https://hdl.handle.net/11583/3003972