The configuration of security systems for communication protection, such as VPNs, is traditionally performed manually by human beings. However, because the complexity of this task becomes soon difficult to manage when its size increases, critical errors that may open the door to cyberattacks may be introduced. Moreover, even when a solution is computed correctly, sub-optimizations that may afflict the performance of the configured VPNs may be introduced. Unfortunately, the possible solution that consists in automating the definition of VPN configurations has been scarcely studied in literature so far. Therefore, this paper proposes an automatic approach to compute the configuration of VPN systems. Both the allocation scheme of VPN systems in the network and their protection rules are computed automatically. This result is achieved through the formulation of a Maximum Satisfiability Modulo Theories problem, which provides both formal correctness-by-construction and optimization of the result. A framework implementing this approach has been developed, and its experimental validation showed that it is a valid alternative for replacing time-consuming and error-prone human operations for significant problem sizes.
@article{TDSC2025B,author={Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={Automating {VPN} Configuration in Computer Networks},journal={{IEEE} Trans. Dependable Secur. Comput.},volume={22},number={1},pages={561--578},year={2025},url={https://doi.org/10.1109/TDSC.2024.3409073},doi={10.1109/TDSC.2024.3409073}}
TDSC
Atomizing Firewall Policies for Anomaly Analysis and Resolution
Daniele
Bringhenti, Simone
Bussa, Riccardo
Sisto, and Fulvio
Valenza
Nowadays, the security management of packet filtering firewall policies got complicated due to the evolution of modern computer networks, characterized by growing size and heterogeneity of communications. The traditional manual approaches for configuring firewalls have become error-prone, unoptimized and time-consuming, leading to an increasing number of policy anomalies, including both sub-optimizations and conflicts. In literature, the techniques proposed for anomaly management have several shortcomings, as their anomaly analysis is usually excessively complex, while their anomaly resolution cannot solve all anomalies. In order to overcome these shortcomings, this paper proposes a comprehensive approach for firewall policy anomaly analysis and resolution, based on the formal concept of atomic predicates. This approach has the aim to simplify the anomaly management operations, make them efficient and solve all configuration anomalies. The achievement of these objectives has been experimentally proved through the validation of a framework which implements the proposed approach, and whose time performance and anomaly management efficiency have been compared with the relevant alternative approaches.
@article{TDSC2025A,author={Bringhenti, Daniele and Bussa, Simone and Sisto, Riccardo and Valenza, Fulvio},title={Atomizing Firewall Policies for Anomaly Analysis and Resolution},journal={{IEEE} Trans. Dependable Secur. Comput.},volume={22},number={3},pages={2308--2325},year={2025},url={https://doi.org/10.1109/TDSC.2024.3495230},doi={10.1109/TDSC.2024.3495230}}
IJNM
Autonomous Attack Mitigation Through Firewall Reconfiguration
Daniele
Bringhenti, Francesco
Pizzato, Riccardo
Sisto, and Fulvio
Valenza
International Journal of Network Management , 2025
Packet filtering firewalls represent a main defense line against cyber attacks that target computer networks daily. However, the traditional manual approaches for their configuration are no longer applicable to next-generation networks, which have become much more complex after the introduction of virtualization paradigms. Some automatic strategies have been investigated in the literature to change that old-fashioned configuration approach, but they are not fully autonomous and still require several human interventions. In order to overcome these limitations, this paper proposes an autonomous approach for firewall reconfiguration where all steps are automated, from the derivation of the security requirements coming from the logs of IDSs to the deployment of the automatically computed configurations. A core component of this process is React-VEREFOO, which models the firewall reconfiguration problem as a Maximum Satisfiability Modulo Theories problem, allowing the combination of full automation, formal verification, and optimization in a single technique. An implementation of this proposal has undergone experimental validation to show its effectiveness and performance.
@article{IJNM2025,author={Bringhenti, Daniele and Pizzato, Francesco and Sisto, Riccardo and Valenza, Fulvio},title={Autonomous Attack Mitigation Through Firewall Reconfiguration},journal={International Journal of Network Management },volume={35.1},pages={e2307},year={2025},url={https://doi.org/10.1002/nem.2307},doi={10.1002/nem.2307}}
2024
TNSM
GreenShield: Optimizing Firewall Configuration for Sustainable Networks
Sustainability is an increasingly critical design feature for modern computer networks. However, green objectives related to energy savings are affected by the application of approximate cybersecurity management techniques. In particular, their impact is evident in distributed firewall configuration, where traditional manual approaches create redundant architectures, leading to avoidable power consumption. This issue has not been addressed by the approaches proposed in literature to automate firewall configuration so far, because their optimization is not focused on network sustainability. Therefore, this paper presents GreenShield as a possible solution that combines security and green-oriented optimization for firewall configuration. Specifically, GreenShield minimizes the power consumption related to firewalls activated in the network while ensuring that the security requested by the network administrator is guaranteed, and the one due to traffic processing by making firewalls to block undesired traffic as near as possible to the sources. The framework implementing GreenShield has undergone experimental tests to assess the provided optimization and its scalability performance.
@article{TNSM2024B,author={Bringhenti, Daniele and Valenza, Fulvio},title={GreenShield: Optimizing Firewall Configuration for Sustainable Networks},journal={{IEEE} Trans. Netw. Serv. Manag.},volume={21},number={6},pages={6909--6923},year={2024},url={https://doi.org/10.1109/TNSM.2024.3452150},doi={10.1109/TNSM.2024.3452150}}
TNSM
A Two-Fold Traffic Flow Model for Network Security Management
Daniele
Bringhenti, Simone
Bussa, Riccardo
Sisto, and Fulvio
Valenza
Introducing formal methods in the automatic resolution of network security management problems can guarantee solution correctness, so also boosting human confidence in using automatic techniques. A necessary step to achieve this feature is the definition of formal network models, representing network topology, traffic flows, etc. Each state-of-the-art formal network modeling approach has been proposed and validated only for a specific management problem (e.g., verification of configurations or refinement of policies into configurations). This paper analyzes a possible combination of the most promising state-of-the-art modeling approaches into a unified formal model that can be used by existing automatic resolution algorithms to solve both the verification and the refinement problems, without the need of major changes. The model is flexible enough to allow different aggregation levels of traffic into flows. The paper analyzes two opposite flow aggregation strategies, named Atomic Flows and Maximal Flows, and compares their performance when applied to the two identified security problems.
@article{TNSM2024A,author={Bringhenti, Daniele and Bussa, Simone and Sisto, Riccardo and Valenza, Fulvio},title={A Two-Fold Traffic Flow Model for Network Security Management},journal={{IEEE} Trans. Netw. Serv. Manag.},volume={21},number={4},pages={3740--3758},year={2024},url={https://doi.org/10.1109/TNSM.2024.3407159},doi={10.1109/TNSM.2024.3407159}}
CSR
A Looping Process for Cyberattack Mitigation
Daniele
Bringhenti, Francesco
Pizzato, Riccardo
Sisto, and Fulvio
Valenza
In IEEE International Conference on Cyber Security and Resilience,
CSR 2024, London, UK, September 2-4, 2024, 2024
Mitigating cyberattacks in fast times has become a strong requirement for the security management of modern virtual computer networks, where attacks are highly mutable and short-term. Firewalls would still represent an effective defense line, but the traditional manual approaches for their configuration are no longer applicable. Besides, even if automatic approaches for firewall configuration have been recently proposed in literature, they still require excessive interaction with human administrators, thus delaying the attack mitigation. Therefore, this paper proposes a looping autonomous process that mitigates ongoing attacks by reconfiguring distributed firewalls in a provably correct and optimized way. This continuously active process includes a policy extraction engine to extract information from the alerts produced by monitoring agents and to produce security policies whose enforcement would stop the detected attack. An implementation of this multi-step process has been validated in realistic use cases to assess its efficacy and efficiency in stopping cyberattacks.
@inproceedings{CSR2024,author={Bringhenti, Daniele and Pizzato, Francesco and Sisto, Riccardo and Valenza, Fulvio},title={A Looping Process for Cyberattack Mitigation},booktitle={{IEEE} International Conference on Cyber Security and Resilience,
{CSR} 2024, London, UK, September 2-4, 2024},pages={276--281},publisher={{IEEE}},year={2024},url={https://doi.org/10.1109/CSR61664.2024.10679501},doi={10.1109/CSR61664.2024.10679501}}
NetSoft
An intent-based solution for network isolation in Kubernetes
Francesco
Pizzato, Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
In 10th IEEE International Conference on Network Softwarization, NetSoft
2024, Saint Louis, MO, USA, June 24-28, 2024, 2024
Cloud computing has transformed the landscape of application delivery, offering an enormous pool of devices with a wide-spread geographical distribution. In this context, liquid computing is a novel paradigm that aims to avoid that available resources are underutilized, by facilitating their seamless sharing among different tenants and administrative domains. Nevertheless, liquid computing introduces new security challenges, particularly related to network isolation, which traditional approaches are inadequate to address. Therefore, this paper proposes a security orchestrator to automate the configuration of network isolation primitives across a multi-domain and multi-tenant cloud environment, simplifying the implementation of security patterns like zero trust and least privilege. The proposed solution is intent-driven, because users define their requirements in terms of desired and prohibited network communications through a user-friendly language. In our implemented proposal, intents expressed by different users are harmonized to avoid discordances among them, and then they are translated into Kubernetes Network Policies as isolation primitives.
@inproceedings{NetSoft2024,author={Pizzato, Francesco and Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={An intent-based solution for network isolation in Kubernetes},booktitle={10th {IEEE} International Conference on Network Softwarization, NetSoft
2024, Saint Louis, MO, USA, June 24-28, 2024},pages={381--386},publisher={{IEEE}},year={2024},url={https://doi.org/10.1109/NetSoft60951.2024.10588939},doi={10.1109/NETSOFT60951.2024.10588939}}
NOMS
Security Automation in next-generation Networks and Cloud environments
Francesco
Pizzato, Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
In NOMS 2024 IEEE Network Operations and Management Symposium, Seoul,
Republic of Korea, May 6-10, 2024, 2024
In the next generation networks and cloud systems, administrators should only need to define their intentions through simple high-level intents, leaving the system to autonomously implement them in the best way possible. The adoption of automation enables the possibility to create reactive systems that can reconfigure themselves in response to unpredictable events, such as network attacks. Nowadays, such solutions are far from being achieved. The enforcement of security requirements continues to heavily rely on manual efforts and tools requiring non-negligible expertise to be used. This results in frequent misconfiguration errors or the complete absence of default security measures due to their high implementation complexity. This paper introduces the research that will be carried out within my Ph.D. program, focusing on network security automation. The objective is to bridge existing gaps in the literature, on one side developing novel automated and intent-based approaches for security enforcement in cloud environments, ensuring formal correctness and optimization, and on the other side researching new solutions for the design of security reaction mechanisms for modern networks in response to network attacks.
@inproceedings{NOMS2024B,author={Pizzato, Francesco and Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={Security Automation in next-generation Networks and Cloud environments},booktitle={{NOMS} 2024 {IEEE} Network Operations and Management Symposium, Seoul,
Republic of Korea, May 6-10, 2024},pages={1--4},publisher={{IEEE}},year={2024},url={https://doi.org/10.1109/NOMS59830.2024.10575650},doi={10.1109/NOMS59830.2024.10575650}}
NOMS
Automatic and optimized firewall reconfiguration
Francesco
Pizzato, Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
In NOMS 2024 IEEE Network Operations and Management Symposium, Seoul,
Republic of Korea, May 6-10, 2024, 2024
The continuous innovation in network softwarization has enabled higher dynamism and responsiveness in creating and deploying complex network configurations. Following this trend, several approaches have been proposed to automate the allocation and configuration of network security functions to satisfy a set of network security policies, describing the security requirements to be fulfilled in the network. In particular, many studies focused on addressing this problem for the packet filtering firewall, as it is the most common firewall technology used in computer networks. However, those proposed techniques for automatic firewall configuration are not optimized for reconfiguring an already deployed network. This results in a computation delay that is incompatible with the needs of modern networks and the timing of current network attacks. In order to overcome these limitations, this paper proposes an efficient method to reduce the computation time for reconfiguration while providing an automated, formally correct, and optimal placement and configuration of the required network security functions. The proposal has undergone validation and evaluation tests, to show the improvements in comparison to non-optimized approaches.
@inproceedings{NOMS2024A,author={Pizzato, Francesco and Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={Automatic and optimized firewall reconfiguration},booktitle={{NOMS} 2024 {IEEE} Network Operations and Management Symposium, Seoul,
Republic of Korea, May 6-10, 2024},pages={1--9},publisher={{IEEE}},year={2024},url={https://doi.org/10.1109/NOMS59830.2024.10575212},doi={10.1109/NOMS59830.2024.10575212}}
Comput. Surv.
Automation for Network Security Configuration: State of the Art and
Research Trends
Daniele
Bringhenti, Guido
Marchetto, Riccardo
Sisto, and Fulvio
Valenza
The size and complexity of modern computer networks are progressively increasing, as a consequence of novel architectural paradigms such as the Internet of Things and network virtualization. Consequently, a manual orchestration and configuration of network security functions is no more feasible in an environment where cyber attacks can dramatically exploit breaches related to any minimum configuration error. A new frontier is then the introduction of automation in network security configuration, i.e., automatically designing the architecture of security services and the configurations of network security functions, such as firewalls, Virtual Private Networks gateways, and so on. This opportunity has been enabled by modern computer networks technologies, such as virtualization. In view of these considerations, the motivations for the introduction of automation in network security configuration are first introduced, along with the key automation enablers. Then, the current state of the art in this context is surveyed, focusing on both the achieved improvements and the current limitations. Finally, possible future trends in the field are illustrated.
@article{COMSUR2024,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Valenza, Fulvio},title={Automation for Network Security Configuration: State of the Art and
Research Trends},journal={{ACM} Comput. Surv.},volume={56},number={3},pages={57:1--57:37},year={2024},url={https://doi.org/10.1145/3616401},doi={10.1145/3616401}}
2023
Access
An Optimized Approach for Assisted Firewall Anomaly Resolution
Daniele
Bringhenti, Lucia
Seno, and Fulvio
Valenza
The security configuration of firewalls is a complex task that is commonly performed manually by network administrators. As a consequence, among the rules composing firewall policies, they often introduce anomalies, which can be classified into sub-optimizations and conflicts, and which must be solved to allow the expected firewall behavior. The severity of this problem has been recently exacerbated by the increasing size and heterogeneity of next-generation computer networks. In this context, a main research challenge is the definition of approaches that may help the administrators in identifying and resolving the anomalies afflicting the policies they write. However, the strategies proposed in literature are fully automated, and thus potentially dangerous because the error-fixing process is not under human control. Therefore, this paper proposes an optimized approach to provide assisted firewall anomaly detection and resolution. This approach solves automatically only sub-optimizations, while it interacts with human users through explicit queries related to the resolution of conflicts, as their automatic resolution may lead to undesired configurations. The proposed approach also reduces the number of required interactions, with the aim to reduce the workload required to administrators, and employs satisfiability checking techniques to provide a correct-by-construction result. A framework implementing this methodology has been finally evaluated in use cases showcasing its applicability and optimization.
@article{Access2023,author={Bringhenti, Daniele and Seno, Lucia and Valenza, Fulvio},title={An Optimized Approach for Assisted Firewall Anomaly Resolution},journal={{IEEE} Access},volume={11},pages={119693--119710},year={2023},url={https://doi.org/10.1109/ACCESS.2023.3328194},doi={10.1109/ACCESS.2023.3328194}}
CRC Press
Introduction to Formal Methods for the Analysis and Design of Cryptographic
Protocols
Daniele
Bringhenti, Riccardo
Sisto, Fulvio
Valenza, and Jalolliddin
Yusupov
In Handbook of Formal Analysis and Verification in Cryptography, 2023
This chapter introduces formal methods, and how they are applied to cryptographic protocols to achieve high security assurance. Cryptographic protocols are communication protocols designed to guarantee security proprieties against the antagonistic actions of attackers. Formal methods are mathematical techniques used to model cryptographic protocols rigorously, and to support their development process in an automated way, so managing their high complexity and reducing the risk of human error. The most important techniques supporting this development process are overviewed, starting from how formal cryptographic protocol models can be built with increasing detail level (belief models, symbolic models, and computational models). Then, this chapter introduces the techniques to formally verify such models at design level, to link design-level abstract models to concrete implementations to reduce the risk of introducing errors in the implementation phase, and the techniques for run-time monitoring of implementations based on formal models. Finally, examples of frameworks combining such techniques are presented.
@incollection{CRC2023,author={Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio and Yusupov, Jalolliddin},editor={Akleylek, Sedat and Dundua, Besik},title={Introduction to Formal Methods for the Analysis and Design of Cryptographic
Protocols},booktitle={Handbook of Formal Analysis and Verification in Cryptography},pages={57--104},publisher={{CRC} Press},year={2023},url={https://doi.org/10.1201/9781003090052-2},doi={10.1201/9781003090052-2}}
Comput. Networks
A novel abstraction for security configuration in virtual networks
Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
The incessant growth of network virtualization determined the proliferation of Virtual Network Functions (VNFs), software programs that can run on general-purpose servers and that can also integrate security controls for protection from cyber-attacks. However, a high availability of VNFs may be counterproductive for the network administrators who have to select the most suitable ones to establish the security configuration of their network. On the one hand, the vendor-dependent technicalities of each VNF may cloud the security controls it can actually perform. On the other hand, VNF selection traditionally occurs before the synthesis of the virtual network graph, so it does not employ any network information and it may outcome unoptimized results. In light of these shortcomings, this paper proposes a novel security configuration workflow, based on new abstractions that we call projections. They represent the security-related operations that VNFs should perform to enforce a security policy. Thanks to these abstractions, the actual selection of the VNFs can be postponed to the moment their deployment in the physical network is actually required. In fact, projections are enough for the synthesis of the virtual security graph. This paper also proposes a two-step algorithm for computing projection chains as candidate solutions for graph synthesis. The proposed approach has been implemented as a Java framework and a set of tests have validated its applicability to real-world VNFs, correctness, scalability and optimization. These tests showed that the new security configuration workflow can achieve a significant reduction for the number of selected VNFs and their deployment cost. Specifically, in the analyzed scenario, the improvement percentages for these two parameters are 79% and 90% with respect to the worst-case strategy, while 68% and 77% with respect to a traditional more optimized configuration strategy.
@article{ComNet2023,author={Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={A novel abstraction for security configuration in virtual networks},journal={Comput. Networks},volume={228},pages={109745},year={2023},url={https://doi.org/10.1016/j.comnet.2023.109745},doi={10.1016/J.COMNET.2023.109745}}
NetSoft
A demonstration of VEREFOO: an automated framework for virtual firewall
configuration
Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
In 9th IEEE International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023, 2023
Nowadays, security automation exploits the agility characterizing network virtualization to replace the traditional error-prone human operations. This dynamism allows user-specified high-level intents to be rapidly refined into the concrete configuration rules which should be deployed on virtual security functions. In this revolutionary context, this paper proposes the demonstration of a novel security framework based on an optimized approach for the automatic orchestration of virtual distributed firewalls. The framework provides formal guarantees for the firewall configuration correctness and minimizes the size of the firewall allocation scheme and rule set. The framework produces rules that can be deployed on multiple types of real virtual function implementations, such as iptables, eBPF firewalls and Open vSwitch.
@inproceedings{NetSoft2023D,author={Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={A demonstration of {VEREFOO:} an automated framework for virtual firewall
configuration},booktitle={9th {IEEE} International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023},pages={293--295},publisher={{IEEE}},year={2023},url={https://doi.org/10.1109/NetSoft57336.2023.10175442},doi={10.1109/NETSOFT57336.2023.10175442}}
NetSoft
Towards Security Automation in Virtual Networks
Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
In 9th IEEE International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023, 2023
Nowadays virtual computer networks are characterized by high dynamism and complexity. However, these features made the traditional manual approaches for network security management error-prone, unoptimized and time-consuming. This paper discusses the research carried out during my Ph.D. program on network security automation. In particular, it presents an approach based on constraint programming that combines automation, formal verification, and optimization for network security management. This approach has been proved to be general enough by means of multiple applications that have been developed. In particular, this paper describes VEREFOO, a framework for the automatic configuration of security functions, and FATO, a framework for the automatic orchestration of security transients. This methodology is extensively evaluated using different metrics and tests, and it has been compared to state-of-the-art solutions and to the requirements of dynamic virtual networks.
@inproceedings{NetSoft2023C,author={Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={Towards Security Automation in Virtual Networks},booktitle={9th {IEEE} International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023},pages={326--331},publisher={{IEEE}},year={2023},url={https://doi.org/10.1109/NetSoft57336.2023.10175459},doi={10.1109/NETSOFT57336.2023.10175459}}
NetSoft
Automating the configuration of firewalls and channel protection systems
in virtual networks
Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
In 9th IEEE International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023, 2023
Network virtualization has revolutionized the traditional approaches for security configuration. If in the past error-prone and unoptimized manual operations were performed by human beings, nowadays automated methodologies are employed for establishing the configuration of virtual security functions that can enforce the requested security properties. However, these techniques can only perform the automatic configuration of a single function type at a time. This restriction may be excessively limiting, because the configuration of some functions may directly impact others, and they cannot be configured in sequence. In light of these considerations, the paper investigates the stated problem for the two most commonly used security functions, packet filtering firewalls and channel protection systems. It also proposes a preliminary approach to automatically perform their joint intent-based configuration, by defining the problem through a Maximum Satisfiability Modulo Theories formulation.
@inproceedings{NetSoft2023B,author={Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={Automating the configuration of firewalls and channel protection systems
in virtual networks},booktitle={9th {IEEE} International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023},pages={474--479},publisher={{IEEE}},year={2023},url={https://doi.org/10.1109/NetSoft57336.2023.10175466},doi={10.1109/NETSOFT57336.2023.10175466}}
NetSoft
Security automation for multi-cluster orchestration in Kubernetes
Daniele
Bringhenti, Riccardo
Sisto, and Fulvio
Valenza
In 9th IEEE International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023, 2023
In the latest years, multi-domain Kubernetes architectures composed of multiple clusters have been getting more frequent, so as to provide higher workload isolation, resource availability flexibility and scalability for application deployment. However, manually configuring their security may lead to inconsistencies among policies defined in different clusters, or it may require knowledge that the administrator of each domain cannot have. Therefore, this paper proposes an automatic approach for the automatic generation of the network security policies to be deployed in each cluster of a multi-domain Kubernetes deployment. The objectives of this approach are to reduce of configuration errors that human administrators commonly make, and to create transparent cross-cluster communications. This approach has been implemented as a framework named Multi-Cluster Orchestrator, which has been validated in realistic use cases to assess its benefits to Kubernetes orchestration.
@inproceedings{NetSoft2023A,author={Bringhenti, Daniele and Sisto, Riccardo and Valenza, Fulvio},title={Security automation for multi-cluster orchestration in Kubernetes},booktitle={9th {IEEE} International Conference on Network Softwarization, NetSoft
2023, Madrid, Spain, June 19-23, 2023},pages={480--485},publisher={{IEEE}},year={2023},url={https://doi.org/10.1109/NetSoft57336.2023.10175419},doi={10.1109/NETSOFT57336.2023.10175419}}
TDSC
Automated Firewall Configuration in Virtual Networks
The configuration of security functions in computer networks is still typically performed manually, which likely leads to security breaches and long re-configuration times. This problem is exacerbated for modern networks based on network virtualization, because their complexity and dynamics make a correct manual configuration practically unfeasible. This article focuses on packet filters, i.e., the most common firewall technology used in computer networks, and it proposes a new methodology to automatically define the allocation scheme and configuration of packet filters in the logical topology of a virtual network. The proposed method is based on solving a carefully designed partial weighted Maximum Satisfiability Modulo Theories problem by means of a state-of-the-art solver. This approach formally guarantees the correctness of the solution, i.e., that all security requirements are satisfied, and it minimizes the number of needed firewalls and firewall rules. This methodology is extensively evaluated using different metrics and tests on both synthetic and real use cases, and compared to the state-of-the-art solutions, showing its superiority.
@article{TDSC2023,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Valenza, Fulvio and Yusupov, Jalolliddin},title={Automated Firewall Configuration in Virtual Networks},journal={{IEEE} Trans. Dependable Secur. Comput.},volume={20},number={2},pages={1559--1576},year={2023},url={https://doi.org/10.1109/TDSC.2022.3160293},doi={10.1109/TDSC.2022.3160293}}
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.
@article{ComNet2022B,author={Bringhenti, Daniele and Valenza, Fulvio},title={Optimizing distributed firewall reconfiguration transients},journal={Comput. Networks},volume={215},pages={109183},year={2022},url={https://doi.org/10.1016/j.comnet.2022.109183},doi={10.1016/J.COMNET.2022.109183}}
Comput. Networks
Automatic, verifiable and optimized policy-based security enforcement
for SDN-aware IoT networks
Daniele
Bringhenti, Jalolliddin
Yusupov, Alejandro Molina
Zarca, Fulvio
Valenza, Riccardo
Sisto, Jorge Bernal
Bernabé, and Antonio F.
Skarmeta
The pervasiveness of Internet of Things (IoT) has made the management of computer networks more troublesome. The softwarized control provided by Software-Defined Networking (SDN) is not sufficient to overcome the problems raising in this context. An increasing number of attacks can, in fact, occur in SDN-aware IoT networks if the security configuration enforced on the SDN switches is manually computed and not formally verified. To mitigate this problem, this paper proposes a novel methodology which leverages Maximum Satisfiability Modulo Theories (MaxSMT) to automatically compute a formally correct and optimized allocation scheme and configuration of SDN switches by refining security policies, user-defined or derived from detected attacks. This mechanism is compliant with the main characteristics of virtualized IoT-based networks, such as the simultaneous presence of numerous interconnected devices and strict latency requirements. The feasibility and the performance of the framework developed to implement this methodology have been validated in a realistic use case.
@article{ComNet2022A,author={Bringhenti, Daniele and Yusupov, Jalolliddin and Zarca, Alejandro Molina and Valenza, Fulvio and Sisto, Riccardo and Bernab{\'{e}}, Jorge Bernal and Skarmeta, Antonio F.},title={Automatic, verifiable and optimized policy-based security enforcement
for SDN-aware IoT networks},journal={Comput. Networks},volume={213},pages={109123},year={2022},url={https://doi.org/10.1016/j.comnet.2022.109123},doi={10.1016/J.COMNET.2022.109123}}
Access
A Twofold Model for VNF Embedding and Time-Sensitive Network Flow
Scheduling
The revolution that Industrial Control Systems are undergoing is reshaping the traditional network management and it is introducing new challenges. After the advent of network virtualization, an enhanced level of automation has been required to cope with the safety-critical mission of industrial systems and strict requirements for end-to-end latency. In the literature, there have been attempts to automatically solve two strictly interconnected problems for the management of virtual industrial networks: the Virtual Network Function embedding and the time-sensitive flow scheduling problems. However, dealing with these problems separately can lead to unoptimized results, or in the worst case to situations where the latency requirements cannot be satisfied because of a poorly chosen function embedding. In light of these motivations, this paper proposes a formal approach to jointly solve the two problems through an Optimization Satisfiability Modulo Theories formulation. This choice also allows combining two vital features: a formal guarantee of the solution correctness and optimization targeting the minimization of the end-to-end delay for flow scheduling. The feasibility of the proposed approach has been validated by implementing a prototype framework and experimentally testing it on realistic use cases.
@article{Access2022,author={Bringhenti, Daniele and Valenza, Fulvio},title={A Twofold Model for {VNF} Embedding and Time-Sensitive Network Flow
Scheduling},journal={{IEEE} Access},volume={10},pages={44384--44399},year={2022},url={https://doi.org/10.1109/ACCESS.2022.3169863},doi={10.1109/ACCESS.2022.3169863}}
Secur. Priv.
Toward Cybersecurity Personalization in Smart Homes
Daniele
Bringhenti, Fulvio
Valenza, and Cataldo
Basile
Security personalization has become a critical need for smart homes in recent years. The current approaches cannot fully satisfy this requirement of user-centered security. We propose a user-friendly approach for the automatic configuration of home security solutions through policy-based management, minimizing human interventions, and improving security usability.
@article{SP2022,author={Bringhenti, Daniele and Valenza, Fulvio and Basile, Cataldo},title={Toward Cybersecurity Personalization in Smart Homes},journal={{IEEE} Secur. Priv.},volume={20},number={1},pages={45--53},year={2022},url={https://doi.org/10.1109/MSEC.2021.3117471},doi={10.1109/MSEC.2021.3117471}}
2021
NetSoft
A novel approach for security function graph configuration and deployment
Daniele
Bringhenti, Guido
Marchetto, Riccardo
Sisto, and Fulvio
Valenza
In 7th IEEE International Conference on Network Softwarization, NetSoft
2021, Tokyo, Japan, June 28 - July 2, 2021, 2021
Network virtualization increased the versatility in enforcing security protection, by easing the development of new security function implementations. However, the drawback of this opportunity is that a security provider, in charge of configuring and deploying a security function graph, has to choose the best virtual security functions among a pool so large that makes manual decisions unfeasible. In light of this problem, the paper proposes a novel approach for synthesizing virtual security services by introducing the functionality abstraction. This new level of abstraction allows to work in the virtual level without considering the different function implementations, with the objective to postpone the function selection jointly with the deployment, after the configuration of the virtual graph. This novelty enables to optimize the function selection when the pool of available functions is very large. A framework supporting this approach has been implemented and it showed adequate scalability for the requirements of modern virtual networks.
@inproceedings{NetSoft2021,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Valenza, Fulvio},title={A novel approach for security function graph configuration and deployment},booktitle={7th {IEEE} International Conference on Network Softwarization, NetSoft
2021, Tokyo, Japan, June 28 - July 2, 2021},pages={457--463},publisher={{IEEE}},year={2021},url={https://doi.org/10.1109/NetSoft51509.2021.9492654},doi={10.1109/NETSOFT51509.2021.9492654}}
TNSM
Improving the Formal Verification of Reachability Policies in Virtualized
Networks
Network Function Virtualization (NFV) and Software Defined Networking (SDN) are new emerging paradigms that changed the rules of networking, shifting the focus on dynamicity and programmability. In this new scenario, a very important and challenging task is to detect anomalies in the data plane, especially with the aid of suitable automated software tools. In particular, this operation must be performed within quite strict times, due to the high dynamism introduced by virtualization. In this article, we propose a new network modeling approach that enhances the performance of formal verification of reachability policies, checked by solving a Satisfiability Modulo Theories (SMT) problem. This performance improvement is motivated by the definition of function models that do not work on single packets, but on packet classes. Nonetheless, the modeling approach is comprehensive not only of stateless functions, but also stateful functions such as NATs and firewalls. The implementation of the proposed approach achieves high scalability in complex networked systems consisting of several heterogeneous functions.
@article{TNSM2021,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Spinoso, Serena and Valenza, Fulvio and Yusupov, Jalolliddin},title={Improving the Formal Verification of Reachability Policies in Virtualized
Networks},journal={{IEEE} Trans. Netw. Serv. Manag.},volume={18},number={1},pages={713--728},year={2021},url={https://doi.org/10.1109/TNSM.2020.3045781},doi={10.1109/TNSM.2020.3045781}}
2020
CYSARM@CCS
Short Paper: Automatic Configuration for an Optimal Channel Protection
in Virtualized Networks
Daniele
Bringhenti, Guido
Marchetto, Riccardo
Sisto, and Fulvio
Valenza
In CYSARM@CCS ’20: Proceedings of the 2nd Workshop on Cyber-Security
Arms Race, Virtual Event, USA, November, 2020, 2020
Data confidentiality, integrity and authentication are security properties which are often enforced with the generation of secure channels, such as Virtual Private Networks, over unreliable network infrastructures. Traditionally, the configuration of the systems responsible of encryption operations is performed manually. However, the advent of software-based paradigms, such as Software-Defined Networking and Network Functions Virtualization, has introduced new arms races. In particular, even though network management has become more flexible, the increased complexity of virtual networks is making manual operations unfeasible and leading to errors which open the path to a large number of cyber attacks. A possible solution consists in reaching a trade-off between flexibility and complexity, by automatizing the configuration of the channel protection systems through policy refinement. In view of these considerations, this paper proposes a preliminary study for an innovative methodology to automatically allocate and configure channel protection systems in virtualized networks. The proposed approach would be based on the formulation of a MaxSMT problem and it would be the first to combine automation, formal verification and optimality in a single technique.
@inproceedings{CYSARM2020,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Valenza, Fulvio},title={Short Paper: Automatic Configuration for an Optimal Channel Protection
in Virtualized Networks},booktitle={CYSARM@CCS '20: Proceedings of the 2nd Workshop on Cyber-Security
Arms Race, Virtual Event, USA, November, 2020},pages={25--30},publisher={{ACM}},year={2020},url={https://doi.org/10.1145/3411505.3418439},doi={10.1145/3411505.3418439}}
NetSoft
Introducing programmability and automation in the synthesis of virtual
firewall rules
The rise of new forms of cyber-threats is mostly due to the extensive use of virtualization paradigms and the increasing adoption of automation in the software life-cycle. To address these challenges we propose an innovative framework that leverages the intrinsic programmability of the cloud and software-defined infrastructures to improve the effectiveness and efficiency of reaction mechanisms. In this paper, we present our contributions with a demonstrative use case in the context of Kubernetes. By means of this framework, developers of cybersecurity appliances will not have any more to care about how to react to events or to struggle to define any possible security tasks at design time. In addition, automatic firewall ruleset generation provided by our framework will mostly avoid human intervention, hence decreasing the time to carry out them and the likelihood of errors. We focus our discussions on technical challenges: definition of common actions at the policy level and their translation into configurations for the heterogeneous set of security functions by means of a use case.
@inproceedings{NetSoft2020,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Valenza, Fulvio and Yusupov, Jalolliddin},title={Introducing programmability and automation in the synthesis of virtual
firewall rules},booktitle={6th {IEEE} Conference on Network Softwarization, NetSoft 2020, Ghent,
Belgium, June 29 - July 3, 2020},pages={473--478},publisher={{IEEE}},year={2020},url={https://doi.org/10.1109/NetSoft48620.2020.9165434},doi={10.1109/NETSOFT48620.2020.9165434}}
NOMS
Automated optimal firewall orchestration and configuration in virtualized
networks
Emerging technologies such as Software-Defined Networking and Network Functions Virtualization are making the definition and configuration of network services more dynamic, thus making automatic approaches that can replace manual and error-prone tasks more feasible. In view of these considerations, this paper proposes a novel methodology to automatically compute the optimal allocation scheme and configuration of virtual firewalls within a user-defined network service graph subject to a corresponding set of security requirements. The presented framework adopts a formal approach based on the solution of a weighted partial MaxSMT problem, which also provides good confidence about the solution correctness. A prototype implementation of the proposed approach based on the z3 solver has been used for validation, showing the feasibility of the approach for problem instances requiring tens of virtual firewalls and similar numbers of security requirements.
@inproceedings{NOMS2020,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Valenza, Fulvio and Yusupov, Jalolliddin},title={Automated optimal firewall orchestration and configuration in virtualized
networks},booktitle={{NOMS} 2020 - {IEEE/IFIP} Network Operations and Management Symposium,
Budapest, Hungary, April 20-24, 2020},pages={1--7},publisher={{IEEE}},year={2020},url={https://doi.org/10.1109/NOMS47738.2020.9110402},doi={10.1109/NOMS47738.2020.9110402}}
2019
ICCCS
Towards a fully automated and optimized network security functions
orchestration
Automated policy-based network security management tools represent a new research frontier to be fully explored, so as to reduce the number of human errors due to a manual and suboptimal configuration of security services. Moreover, the agility that an automated tool would require can be provided by the most recent networking technologies, Network Functions Virtualization and Software-Defined Networking, which move the network management from the hardware level to the software. However, even though a Security Automation approach is nowadays feasible and would bring several benefits in facing cybersecurity attacks, pending problems are that currently only a limited number of automatic management tools have been developed and that they do not have a direct integration with cloud orchestrators, consequently requiring human interaction. Given these considerations, in this paper we propose a novel framework, whose goal is to automatically and optimally allocate and conFigure security functions in a virtualized network service in a formal and verified way, directly integrated in cloud orchestrators. We validated this contribution through an implementation that is able to cooperate with two well-known orchestrators, that are Open Baton and Kubernetes.
@inproceedings{ICCCS2019,author={Bringhenti, Daniele and Marchetto, Guido and Sisto, Riccardo and Valenza, Fulvio and Yusupov, Jalolliddin},title={Towards a fully automated and optimized network security functions
orchestration},booktitle={2019 4th International Conference on Computing, Communications and
Security (ICCCS), Rome, Italy, October 10-12, 2019},pages={1--7},publisher={{IEEE}},year={2019},url={https://doi.org/10.1109/CCCS.2019.8888130},doi={10.1109/CCCS.2019.8888130}}