Fulvio Valenza

dblp:161/8059 · DBLP profile ↗
← Back
43ranked-venue papers
4as first author
31since 2021 · last 2026
0000-0002-8471-3029ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 14 · 11 since 2021Computer networks · 12 · 3 first-author · 9 since 2021Security and privacy · 10 · 1 first-author · 7 since 2021Applied, interdisciplinary, general and emerging computing · 2 · 1 since 2021Systems, architecture and hardware · 1
YearPublicationVenuePosition
2026 Improving Web Protection in Virtual Networks with Automatic WAF Configuration
Daniele Bringhenti, Francesco Pizzato, Fulvio Valenza
NetSoft3
2026 Toward Risk-Driven Cybersecurity Management for Virtual Networks
Francesca Coriale, Daniele Bringhenti, Fulvio Valenza
NetSoft3
2026 GreenShield-E2C: A sustainable energy-aware firewall configuration mechanism for edge-to-cloud continuum
abstract
The advent of the edge-to-cloud continuum paradigm has enabled a seamless integration of resources across different architectural layers, offering significant benefits in terms of scalability and flexibility. Due to the complexity of this environment, a key operation is to enforce adequate network security mechanisms to protect the continuum in an effective, efficient, and correct way. In this regard, a critical task is the configuration of distributed packet-filtering firewalls, because they are essential to protect the boundaries between the different layers. Unfortunately, their configuration is commonly performed manually and in an unoptimized way, raising pressing challenges from a sustainability perspective, due to the increasing power consumption related to the activation and operation of each firewall instance in the continuum. In order to address this problem, this paper proposes an approach, named GreenShield-E2C, which integrates automation, formal verification, and sustainability optimization for distributed firewall configuration into a unified methodology tailored explicitly for the continuum’s heterogeneous and multi-layer nature. These achievements were reached by formulating the configuration problem as a Maximum Satisfiability Modulo Theories problem, ensuring security policy compliance while minimizing the firewall power consumption. The implementation of the proposed approach has been experimentally evaluated on scenarios derived from a realistic smart city use case, so as to showcase its energy efficiency effectiveness and performance.
Daniele Bringhenti, Fulvio Valenza
Comput. Networks2
2026 FDO Protocol: A Possible Solution to Protect the Ownership Voucher Against Untrusted Supply Chain
abstract
The FDO protocol is the leading candidate to become the reference standard for automatic device onboarding. However, as documented in the literature, it may suffer from a security issue exploiting its Ownership Voucher when the supply chain of the device cannot be considered trusted. In a previous work, we showed a possible attack of this type, found by performing a formal analysis on a symbolic model of the protocol. The first contribution of this paper is to present the analysis done in the previous work in a more comprehensive way, to extend it, and to show that the attack found is also possible on a real implementation of the protocol. We then analyse some possible solutions proposed in the literature as countermeasures to try to mitigate the attack. After demonstrating that they may not completely solve the mentioned issue, we propose our own solution, which could be taken into consideration by the FIDO Working Group to further improve the protocol specification. Again, as a demonstration of the logical correctness of our solution, we formally analyse its symbolic model.
Simone Bussa, Riccardo Sisto, Fulvio Valenza
IEEE Trans. Dependable Secur. Comput.3
2025 A Demonstration of an Autonomous Approach for Cyberattack Mitigation
abstract
The increasing complexity and size of virtual networks, jointly with the fast-evolving nature of modern threats, have significantly amplified the challenge of mitigating cyberattacks in real time. In particular, these factors have made the traditional approaches for network security reconfiguration unfeasible, as they rely heavily on manual operations. To address these issues, this demo presents a looping process that autonomously mitigates ongoing attacks by extracting security policies from intrusion detection system alerts and automatically reconfiguring distributed firewalls via a provably correct and optimized approach. The proposed system architecture is composed of several interconnected components responsible for the full lifecycle from the detection of an attack to the deployment of the updated and secure configuration, operating in a fully automated and self-triggering way, aiming to reduce human involvement while improving mitigation speed and correctness.
Francesco Pizzato, Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
CNSM4
2025 Analysis of the eBPF Vulnerabilities in the Linux Kernel
Rosario Rizza, Riccardo Sisto, Fulvio Valenza
CRiSIS3
2025 Adaptive, Agile and Automated Cybersecurity Management
abstract
In recent years, the network paradigms of Software Defined Networking and Network Function Virtualization have gained significant traction, leading to the emergence of new network architectures that emphasize flexibility and adaptability. However, the rapid evolution of these paradigms has outpaced the development of effective cybersecurity management solutions, which remain largely reliant on traditional, manual processes. In this context, my doctoral research aims to advance network security automation by integrating Artificial Intelligence and formal methods into hybrid approaches for automating the configuration of network security functions. These approaches seek to combine the strengths of both fields, which are formal correctness, optimization, and computational efficiency. In this paper, I present the research questions and directions that will guide my PhD activity in developing such hybrid approaches.
Gianmarco Bachiorrini, Daniele Bringhenti, Fulvio Valenza
NetSoft3
2025 Toward the Optimization of Automated VPN Configuration
abstract
In recent years, VPNs have become one of the most essential security mechanisms, allowing the users to safely communicate over untrusted networks. As research in security automation advances, the literature has introduced various approaches for automating the configuration of security functions and addressing the growing challenges faced by security administrators, though only a limited number specifically address VPNs. An effective constraint programming-based approach in this field is VEREFOO, which leverages formal methods to automatically and optimally configure VPNs while ensuring formal correctness by construction. However, VEREFOO was not designed to minimize memory consumption and performance overhead, despite their relevance in both enterprise and commercial modern virtual networks. In this paper, the optimization aspect of the VEREFOO approach is enhanced and expanded on both of these new fronts. Specifically, new optimization strategies are designed to provide minimization of the configured rules and maximization of constraints generation efficiency. This optimized approach has been implemented as a framework and validated on a realistic use case to assess optimization improvements across multiple aspects.
Gianmarco Bachiorrini, Daniele Bringhenti, Fulvio Valenza
NetSoft3
2025 Formal verification of a V2X scheme mixing traditional PKI and group signatures
abstract
Vehicle-to-Everything (V2X) communications are expected to reshape road mobility in the increasingly near future. This type of communication allows a vehicle to transmit information, such as its position and speed, which can be used for different applications. However, despite the benefits, the increased connectivity and data sent over the network may expose the vehicle to a significant number of cyber attacks. This paper takes one of the schemes proposed in the literature to protect the security and privacy of the vehicles, and analyses it from a security and privacy perspective using Proverif. Specifically, this scheme is unique in combining asymmetric encryption with digital certificates and group signatures used by vehicles to self-certify those certificates. We present a formal model able to capture all the main aspects of the protocol and the context in which it works, and show how security and privacy properties can be expressed for formal verification in Proverif. Our analysis conducted on the model of the protocol revealed some weaknesses for which we tried to provide a solution.
Simone Bussa, Riccardo Sisto, Fulvio Valenza
J. Inf. Secur. Appl.3
2025 Atomizing Firewall Policies for Anomaly Analysis and Resolution
abstract
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 article 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.
Daniele Bringhenti, Simone Bussa, Riccardo Sisto, Fulvio Valenza
IEEE Trans. Dependable Secur. Comput.4
2025 Automating VPN Configuration in Computer Networks
abstract
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.
Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
IEEE Trans. Dependable Secur. Comput.3
2024 An intent-based solution for network isolation in Kubernetes
abstract
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.
Francesco Pizzato, Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
NetSoft4
2024 Automatic and optimized firewall reconfiguration
abstract
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.
Francesco Pizzato, Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
NOMS4
2024 Security Automation in next-generation Networks and Cloud environments
abstract
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.
Francesco Pizzato, Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
NOMS4
2024 A Two-Fold Traffic Flow Model for Network Security Management
abstract
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.
Daniele Bringhenti, Simone Bussa, Riccardo Sisto, Fulvio Valenza
IEEE Trans. Netw. Serv. Manag.4
2024 GreenShield: Optimizing Firewall Configuration for Sustainable Networks
abstract
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.
Daniele Bringhenti, Fulvio Valenza
IEEE Trans. Netw. Serv. Manag.2
2023 A demonstration of VEREFOO: an automated framework for virtual firewall configuration
abstract
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.
Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
NetSoft3
2023 Towards Security Automation in Virtual Networks
abstract
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.
Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
NetSoft3
2023 Automating the configuration of firewalls and channel protection systems in virtual networks
abstract
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.
Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
NetSoft3
2023 Security automation for multi-cluster orchestration in Kubernetes
abstract
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.
Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
NetSoft3
2023 A novel abstraction for security configuration in virtual networks
abstract
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.
Daniele Bringhenti, Riccardo Sisto, Fulvio Valenza
Comput. Networks3
2023 Automated Firewall Configuration in Virtual Networks
abstract
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.
Daniele Bringhenti, Guido Marchetto, Riccardo Sisto, Fulvio Valenza, Jalolliddin Yusupov
IEEE Trans. Dependable Secur. Comput.4
2023 A Hybrid Threat Model for Smart Systems
abstract
Cyber-physical systems and their smart components have a pervasive presence in all our daily activities. Unfortunately, identifying the potential threats and issues in these systems and selecting enough protection is challenging given that such environments combine human, physical and cyber aspects to the system design and implementation. Current threat models and analysis do not take into consideration all three aspects of the analyzed system, how they can introduce new vulnerabilities or protection measures to each other. In this work, we introduce a novel threat model for cyber-physical systems that combines the cyber, physical, and human aspects. Our model represents the system's components relations and security properties by taking into consideration these three aspects. Together with the threat model we also propose a threat analysis method that allows understanding the security state of the system's components. The threat model and the threat analysis have been implemented into an automatic tool, called TAMELESS, that automatically analyzes threats to the system, verifies its security properties, and generates a graphical representation, useful for security architects to identify the proper prevention/mitigation solutions. We show and prove the use of our threat model and analysis with three cases studies from different sectors.
Fulvio Valenza, Erisa Karafili, Rodrigo Vieira Steiner, Emil C. Lupu
IEEE Trans. Dependable Secur. Comput.1
2022 Security Automation using Traffic Flow Modeling
abstract
he growing trend towards network “softwarization” allows the creation and deployment of even complex network environments in a few minutes or seconds, rather than days or weeks as required by traditional methods. This revolutionary approach made it necessary to seek automatic processes to solve network security problems. One of the main issues in the automation of network security concerns the proper and efficient modeling of network traffic. In this paper, we describe two optimized Traffic Flows representation models, called Atomic Flows and Maximal Flows. In addition to the description, we have validated and evaluated the proposed models to solve two key network security problems - security verification and automatic configuration - showing the advantages and limitations of each solution.
Simone Bussa, Riccardo Sisto, Fulvio Valenza
NetSoft3
2022 Optimizing distributed firewall reconfiguration transients
Daniele Bringhenti, Fulvio Valenza
Comput. Networks2
2022 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é, Antonio F. Skarmeta
Comput. Networks4
2022 Guest Editors Introduction: Special Section on Recent Advances in Network Security Management
abstract
As the backbone of communications amongst objects, humans, companies, and administrations, the Internet has become a great integration platform capable of efficiently interconnecting billions of entities, from RFID chips to data centers. This platform provides access to multiple hardware and virtualized resources (servers, networking, storage, applications, connected objects) coming from cloud computing and Internet-of-Things (IoT) infrastructures. From these resources that may be hosted and distributed amongst different providers and tenants, the building and operation of complex and value-added networked systems is enabled.
Rémi Badonnel, Carol J. Fung, Sandra Scott-Hayward, Qi Li 0002, Fulvio Valenza, Cristian Hesselman
IEEE Trans. Netw. Serv. Manag.5
2021 A novel approach for security function graph configuration and deployment
abstract
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.
Daniele Bringhenti, Guido Marchetto, Riccardo Sisto, Fulvio Valenza
NetSoft4
2021 Guest editorial: Special issue on novel cyber-security paradigms for software-defined and virtualized systems
Fulvio Valenza, Matteo Repetto, Stavros Shiaeles
Comput. Networks1
2021 A Formal Approach to Verify Connectivity and Optimize VNF Placement in Industrial Networks
abstract
The increased flexibility and interconnectivity of modern industrial communication networks, obtained through the use of innovative technologies like network function virtualization and software-defined networking, require a secure and manageable framework to support the new communication and computing needs. To focus on these requirements, this article proposes a framework for reliable placement of services across physically separated locations, which offers both system optimization, in terms of latency and resource utilization, and connectivity policy enforcement to guarantee service reliability, safety, and security. This is achieved by exploiting a new approach to solve the virtual network embedding problem, using optimization modulo theories (MaxSMT), which allows the use of very expressive constraints.
Guido Marchetto, Riccardo Sisto, Fulvio Valenza, Jalolliddin Yusupov, Adlen Ksentini
IEEE Trans. Ind. Informatics3
2021 Improving the Formal Verification of Reachability Policies in Virtualized Networks
abstract
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.
Daniele Bringhenti, Guido Marchetto, Riccardo Sisto, Serena Spinoso, Fulvio Valenza, Jalolliddin Yusupov
IEEE Trans. Netw. Serv. Manag.5
2020 Introducing programmability and automation in the synthesis of virtual firewall rules
abstract
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.
Daniele Bringhenti, Guido Marchetto, Riccardo Sisto, Fulvio Valenza, Jalolliddin Yusupov
NetSoft4
2020 Automated optimal firewall orchestration and configuration in virtualized networks
abstract
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.
Daniele Bringhenti, Guido Marchetto, Riccardo Sisto, Fulvio Valenza, Jalolliddin Yusupov
NOMS4
2020 Towards a Framework for Automatic Firewalls Configuration via Argumentation Reasoning
abstract
Firewalls have been widely used to protect not only small and local networks but also large enterprise networks. The configuration of firewalls is mainly done by network administrators, thus, it suffers from human errors. This paper aims to solve the network administrators’ problem by introducing a formal approach that helps to configure centralized and distributed firewalls and automatically generate conflict-free firewall rules. We propose a novel framework, called ArgoFiCo, which is based on argumentation reasoning. Our framework automatically populates the firewalls of a network, given the network topology and the high-level requirements that represent how the network should behave. ArgoFiCo provides two strategies for firewall rules distribution.
Erisa Karafili, Fulvio Valenza, Emil C. Lupu
NOMS2
2020 Work-in-Progress: A Formal Approach to Verify Fault Tolerance in Industrial Network Systems
abstract
Distributed systems are extremely difficult to design and implement correctly because they must handle both system correctness and device failures. Most of the work focuses on the first aspect, and in particular, on the correctness of security and network configuration. The large demand for availability and reliability for critical services is actually pushing new architectures that tolerate faults, but a-priori analysis of redundancy and recovery features is still limited. To this end, we present a framework to design and formally verify the persistence of network properties, even in case of failures. The solution considers both nodes and links failure, and it is based on a formal model that takes both network topology and network device configurations into account. In contrast, most of the existing approaches only consider network topology. By analyzing the formal model, the framework can check whether the specified network services are still available after failures, and in case of success, it outputs a possible configuration of the devices to be used for automatic recovery.
Alessio Sacco, Guido Marchetto, Riccardo Sisto, Fulvio Valenza
WFCS4
2019 A comprehensive approach to the automatic refinement and verification of access control policies
Manuel Cheminod, Luca Durante, Lucia Seno, Fulvio Valenza, Adriano Valenzano
Comput. Secur.4
2019 Formally specifying and checking policies and anomalies in service function chaining
Fulvio Valenza, Serena Spinoso, Riccardo Sisto
J. Netw. Comput. Appl.1
2019 Towards an Efficient Management and Orchestration Framework for Virtual Network Security Functions
abstract
The recent years have witnessed a growth in the number of users connected to computer networks, due mainly to megatrends such as Internet of Things (IoT), Industry 4.0, and Smart Grids. Simultaneously, service providers started offering vertical services related to a specific business case (e.g., automotive, banking, and e-health) requiring more and more scalability and flexibility for the infrastructures and their management. NFV and SDN technologies are a clear way forward to address these challenges even though they are still in their early stages. Security plays a central role in this scenario, mainly because it must follow the rapid evolution of computer networks and the growing number of devices. The main issue is to protect the end-user from the increasing threats, and for this reason, we propose in this paper a security framework compliant to the Security-as-a-Service paradigm. In order to implement this framework, we leverage NFV and SDN technologies, using a user-centered approach. This allows to customize the security service starting from user preferences. Another goal of our work is to highlight the main relevant challenges encountered in the design and implementation of our solution. In particular, we demonstrate how significant is to choose an efficient way to configure the Virtual Network Security Functions in terms of performance. Furthermore, we also address the nontrivial problem of Service Function Chaining in an NFV MANO platform and we show what are the main challenges with respect to this problem.
Ignazio Pedone, Antonio Lioy, Fulvio Valenza
Secur. Commun. Networks3
2019 Adding Support for Automatic Enforcement of Security Policies in NFV Networks
abstract
This paper introduces an approach toward the automatic enforcement of security policies in network functions virtualization (NFV) networks and dynamic adaptation to network changes. The approach relies on a refinement model that allows the dynamic transformation of high-level security requirements into configuration settings for the network security functions (NSFs), and optimization models that allow the optimal selection of the NSFs to use. These models are built on a formalization of the NSF capabilities, which serves to unequivocally describe what NSFs are able to do for security policy enforcement purposes. The approach proposed is the first step toward a security policy aware NFV management, orchestration, and resource allocation system-a paradigm shift for the management of virtualized networks-and it requires minor changes to the current NFV architecture. We prove that our approach is feasible, as it has been implemented by extending the OpenMANO framework and validated on several network scenarios. Furthermore, we prove with performance tests that policy refinement scales well enough to support current and future virtualized networks.
Cataldo Basile, Fulvio Valenza, Antonio Lioy, Diego R. López, Antonio Pastor 0001
IEEE/ACM Trans. Netw.2
2017 A model for the analysis of security policies in service function chains
abstract
Two emerging architectural paradigms, i.e., Software Defined Networking (SDN) and Network Function Virtualization (NFV), enable the deployment and management of Service Function Chains (SFCs). A SFC is an ordered sequence of abstract Service Functions (SFs), e.g., firewalls, VPN-gateways, traffic monitors, that packets have to traverse in the route from source to destination. While this appealing solution offers significant advantages in terms of flexibility, it also introduces new challenges such as the correct configuration and ordering of SFs in the chain to satisfy overall security requirements. This paper presents a formal model conceived to enable the verification of correct policy enforcements in SFCs. Software tools based on the model can then be designed to cope with unwanted network behaviors (e.g., security flaws) deriving from incorrect interactions of SFs in the same SFC.
Luca Durante, Lucia Seno, Fulvio Valenza, Adriano Valenzano
NetSoft3
2017 Classification and Analysis of Communication Protection Policy Anomalies
abstract
This paper presents a classification of the anomalies that can appear when designing or implementing communication protection policies. Together with the already known intra- and inter-policy anomaly types, we introduce a novel category, the inter-technology anomalies, related to security controls implementing different technologies, both within the same network node and among different network nodes. Through an empirical assessment, we prove the practical significance of detecting this new anomaly class. Furthermore, this paper introduces a formal model, based on first-order logic rules that analyses the network topology and the security controls at each node to identify the detected anomalies and suggest the strategies to resolve them. This formal model has manageable computational complexity and its implementation has shown excellent performance and good scalability.
Fulvio Valenza, Cataldo Basile, Daniele Canavese, Antonio Lioy
IEEE/ACM Trans. Netw.1
2015 A novel approach for integrating security policy enforcement with dynamic network virtualization
abstract
Network function virtualization (NFV) is a new networking paradigm that virtualizes single network functions. NFV introduces several advantages compared to classical approaches, such as the dynamic provisioning of functionality or the implementation of scalable and reliable services (e.g., adding a new instance to support demands). NFV also allows the deployment of security controls, like firewalls or VPN gateways, as virtualized network functions. However, currently there is not an automatic way to select the security functions to enable and to configure the selected ones according to a set of user's security requirements. This paper presents a first approach towards the integration of network and security policy management into the NFV framework. By adding to the NFV architecture a new software component, the Policy Manager, we provide NFV with an easy and effective way for users to specify their security requirements and a process that hides all the details of the correct deployment and configuration of security functions. To perform its tasks, the Policy Manager uses policy refinement techniques.
Cataldo Basile, Antonio Lioy, Christian Pitscheider, Fulvio Valenza, Marco Vallini
NetSoft4
2014 Inter-technology Conflict Analysis for Communication Protection Policies
Cataldo Basile, Daniele Canavese, Antonio Lioy, Fulvio Valenza
CRiSIS4