Automatic Optimized Firewalls Orchestration and Configuration in NFV environment

The Network Functions Virtualization (NFV) paradigm is a novel networking technology which, by means of a decoupling between the network functions and the hardware appliances, allows software processes to be installed as service functions on general-purpose servers. Among the consequent benefits, this principle entails further agility and flexibility in the creation of a Service Graph, which is a generalization of the Service Function Chain (SFC) concept, describing how the single network functions must be organized and connected. A problem which, however, arises in the creation of a Service Graph in this scenario is that this task is typically performed by a service designer; instead, the security manager is separately in charge of the allocation and configuration of the Network Security Functions (NSFs) - such as firewalls and anti-spam filters - needed to protect the network from cybersecurity attacks. Moreover, these operations are usually performed manually, so they are prone to human errors and the reaction latency is not negligible whenever the security defences should be updated according to different or additional security requirements. In view of these considerations, this thesis contributed to the development of VEREFOO (VErified REFinement and Optimized Orchestration), a framework which aims to provide a Security Automation approach as a solution to these open problems. The main purpose is to perform, on a provided Service Graph, an automatic optimized allocation and configuration of the NSFs that are necessary tu fulfil an input set of Network Security Requirements (NSRs), which can be expressed by the service designer by exploiting a high-level language. The VEREFOO approach involves the formulation of a MaxSMT problem: its targets are on one side the allocation of the minimum number of NSFs instances to reduce the resource consumption due to the allocation of the corresponding virtual functions, on the other side the reduction of the rules describing their configuration to simplify their management. The MaxSMT problem is formulated so as to provide also a formal verification that the achieved solution is formally correct. The major contributions provided by this thesis work have been the formal definition of the optimization and verification problem and its implementation by means of z3, a state-of-the-art MaxSMT solver, inside the framework. Among all the possible NSFs, the focus has been on packet filter, the most common firewall technology which can filter the received packets according to the values of the IP quintuple. An automatic generation of both the allocation schema and the filtering policies of the firewalls is, currently, an open problem not well addressed in literature by itself. Hence, the solution developed in this thesis advances the state of the art. In order to make this solution really effective, it has been necessary to develop a number of pruning strategies to minimize the number and the complexity of the MaxSMT clauses. The implementation has been finally tested extensively in common network scenarios and it showed good scalability against the dimension of the Service Graph and the number of input NSRs; consequently, this thesis demonstrates that the proposed approach is feasible and that it can provide a valid alternative in enforcing security functions to manual allocation and configuration of packet filtering firewalls, enabling low latency reaction to changes in the NSRs.