Verification and Configuration of Software-based Networks

The innovative trends of Network Function Virtualization (NFV) and Software Defined Networking (SDN) have posed never experienced opportunities in productive environments, like data centers. While NFV decouples software implementation of the network functions (e.g., DPI and NAT) from their physical counterparts, SDN is in charge of dynamically changing those functions to create network paths. One new opportunity of such Software-based networks is to make the network service-provisioning models more flexible, by enabling users to build their own service graphs: users can select the Virtual Network Functions (VNFs) to use and can specify how packets have to be processed and forwarded in their networks. In particular, this PhD thesis spans mostly topics related to the verification and configuration of service graphs. For what concerns the challenges of network verification, our aim is to explore strategies that overcome the limitations of traditional techniques, which generally exploit complex modelling approaches and takes considerable verification times. Thus we envision for verification techniques that are based on non-complex modelling approaches in order to be much more efficient than existing proposals. Under these conditions, such novel approaches may work at run-time and, in particular, may be performed before deploying the service graphs, in order to avoid unexpected network behaviours and detect errors as early as possible. Another requirement is that verification should take a reasonable amount of time from a VNF Orchestrator point of view, with fair processing resources (e.g. CPU, memory and so on). This is because we are in the context of flexible services, where the reconfiguration of network functions can be frequently triggered, both in case of user request and in case of management events. The first contribution of this thesis lays on the service graphs specification by means of forwarding policies (i.e, a high-level specification of how packet flows are forwarded). While the majority of the SDN verification tools operate on OpenFlow configurations, we have defined a formal model to detect a set of anomalies in forwarding policies (i.e., erroneous specifications that may cause misleading network conditions and states). The key factors that distinguish our work from existing approaches are both an early detection of policies anomalies (i.e., before translating such policies into OpenFlow entries), in order to speed up the fixing phase, without even starting service deployment, and a scalable approach that achieves verification times in the order of milliseconds for medium- large- sized networks. Another advancement in network verification has been the possibility to verify networks including stateful VNFs, which are functions that may dynamically change the forwarding path of a traffic flow according to their local algorithms and states (e.g., IDSs). Our second contribution is thus a verification approach that models the network and the involved (possibly stateful) VNFs as a set of FOL formulas. Those formulas are passed to the off-the-shelf SMT (Satisfiability Modulo Theory) solver Z3 in order to verify some reachability-based properties. In particular, the proposed solution has been implemented in a tool released under the AGPLv3 license, named VeriGraph, which takes the functional configurations of all deployed VNFs (e.g., filtering rules on firewalls) into account to check the network. The adopted approach achieves verification times in the order of milliseconds, which is compliant with the timing limitations needed by a VNF Orchestrator. Finally, for what concerns the configuration of VNFs, service graph deployment should include a strategy to deploy VNF configurations in order to fix bugs in case of verification failures. Here, we have to face several challenges like the different ways a network function may require for being configured (REST API, CLI, etc...) and the configuration semantic that depends on the function itself (e.g., router parameters are clearly different from firewall ones). We conclude this thesis by proposing a model-based configuration approach, which means defining a representation of the main configuration parameters of a VNF. This VNF model is then automatically processed by further software modules in the VNF architecture to translate the configuration parameters into a particular format required by a VNF and to deliver the produced configuration into the VNF following one of the configuration strategies (e.g., REST, configuration file, etc.) already supported by the function. The achieved results of this last work, w.r.t. the current state of the art, are the exploitation of a model-driven approach that achieves a higher flexibility and the insertion of non-VNF-specific software modules to avoid changes in the VNF implementation.