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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.