Software weaknesses and vulnerabilities are continuously discovered and rapidly evolving. Their direct and indirect interference with the business process workflow execution is neither fully understood nor addressed by the current literature. The strict control of the vulnerability footprint of the landing platform before cloud/web service workflow execution is nowadays largely used as a prevention measure in order to improve execution trustworthiness. The vulnerability footprint governance is exacerbated by the cloud, where a common execution platform hosting (vulnerable) services is shared between different tenants. The paper proposes a service workflow deployment solution tailored for Edge-Cloud Continuum, made of different landing platforms showing different peculiarities. The proposed solution is capable of finding a suitable deployment recipe for a given workflow by i) evaluating the vulnerability footprint of each platform, ii) computing the set of candidate deployment platforms, iii) finding the optimal deployment solution, and iv) migrating already deployed workflows in case the vulnerability requirement is no longer satisfied. Each workflow can be associated with a set of requirements to be satisfied by our deployment solution, like the maximum level of vulnerability footprint accepted. Each workflow deployment contributes to the vulnerability footprint of the landing platform involved.

Advancements in softwarization and service composition have contributed to the deployment of large-scale distributed cloud services across diverse infrastructures. The growing complexity of these services, combined with the continuous emergence of new vulnerabilities, constitutes a significant challenge in terms of security management. Moving target defense strategies, leveraged by artificial intelligence, offer new opportunities to protect them. At the meantime, the changes that are operated by these strategies may lead these services into vulnerable configurations. We propose in this paper a moving target defense strategy which bridges the gap between artificial intelligence and configuration verification techniques. The objective is to select the movements to be applied on the cloud composite service, in order to reduce the predictability of configuration changes, while minimizing the risk of critical vulnerable configurations. We formalize and design a framework exploiting reinforcement learning and SMT solving, to support this strategy. We also perform large series of experiments to evaluate the feasibility and performance of our solution based on OVAL vulnerability descriptions.

Effective scheduling of software updates is a significant challenge in network operations and management, particularly when considering specific performance and security requirements. This paper focuses on the synthesis of such software updates in the context of emerging virtualized and softwarized networks, such as 5G network infrastructures, with the objective of ensuring vulnerability avoidance and congestion freedom at any time during the updates. We formalize the update synthesis problem and propose an algorithmic solution, called Eagle, that exploits formal methods and mixed integer linear programming, to achieve optimal solutions. We then complement it with a greedy algorithm to support faster computation. We exemplify our framework considering an implementation of a 5G architecture, as the one described in the ETSI 5123 standard, and which relies on kubernetes. Finally, we evaluate our approach through a large range of realistic ISP topologies from the Topology Zoo dataset, and we also perform extensive experiments on our kubernetes cluster, where we execute the software update sequences generated by our tool. This allows us to discuss the scalability of our approach along with its practical applicability.

To meet their stringent requirements in terms of performance and dependability, communication networks should be "well connected". While classic connectivity measures typically revolve around topological properties, e.g., related to cuts, these measures may not reflect well the degree to which a network is actually dependable. We introduce a more refined measure for network connectivity, the hazard value, which is developed to meet the needs of a real network operator. It accounts for crucial aspects affecting the dependability experienced in practice, including actual traffic patterns, distribution of failure probabilities, routing constraints, and alternatives for services with preferences therein. We analytically show that the hazard value fulfills several fundamental desirable properties that make it suitable for comparing different network topologies with one another, and for reasoning about how to efficiently enhance the robustness of a given network. We also present an optimised algorithm to compute the hazard value and an experimental evaluation against networks from the Internet Topology Zoo and classical datacenter topologies, such as fat trees and BCubes. This evaluation shows that the algorithm computes the hazard value within minutes for realistic networks, making it practically usable for network designers.

Abstract To ensure a high availability, communication networks provide resilient routing mechanisms that quickly change routes upon failures. However, a fundamental algorithmic question underlying such mechanisms is hardly understood: how to verify whether a given network reroutes flows alongfeasiblepaths, without violating capacity constraints, for up toklink failures? We chart the algorithmic complexity landscape of resilient routing under link failures, considering shortest path routing based on link weights as e.g. deployed in the ECMP protocol. We study two models: apessimisticmodel where flows interfere in a worst-case manner along equal-cost shortest paths, and anoptimisticmodel where flows are routed in a best-case manner, and we present a complete picture of the algorithmic complexities. We further propose a strategic search algorithm that checks only the critical failure scenarios while still providing correctness guarantees. Our experimental evaluation on a benchmark of Internet and datacenter topologies confirms an improved performance of our strategic search by several orders of magnitude.

Software-defined networking offers new opportunities for protecting end users by designing dynamic security policies. In particular, security chains can be built by combining security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. The configuration of these security functions and their associated policies is based on behavioural models of end-user applications when accessing the network. In this demo, we present our tool Synaptic, a SDN-based framework intended for the formal verification of security policies as well as for automatically generating such policies based on automata learning methods applied on NetFlow records of end-user applications collected at the device level.

Software-defined networking offers new opportu-nities for protecting end users and their applications. In that context, dedicated chains can be built to combine different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. To configure these security chains, it is important to have an adequate model of the patterns that end user applications exhibit when accessing the network. We propose an automated strategy for learning the networking behavior of end applications using algorithms for generating finite state models. These models can be exploited for inferring SDN policies ensuring that applications respect the observed behavior: such policies can be formally verified and deployed on SDN infrastructures in a dynamic and flexible manner. Our solution is prototypically implemented as a collection of Python scripts that extend our Synaptic verification package. The performance of our strategy is evaluated through extensive experimentations and is compared to the Synoptic and Invarimint automata learning algorithms.

Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.