Analysis and characterization of the VPN configuration problem

The automated and optimized configuration of secure communications inside networks is an indispensable necessity. The transmitted data must be protected to guarantee confidentiality, integrity, and availability. From this point of view, VPNs allow the configuration of secure channels between hosts, even over untrusted networks such as the Internet. However, the introduction of virtual systems based on virtualization significantly changes networks, which have become more dynamic and flexible, but also more complex to configure. Therefore, operations require specialized skills and knowledge of the network and the functions to be implemented, which cannot be managed entirely by humans. One possible solution is to make such operations automatic through a policy-based model. This thesis contributes to the development of one of these automated approaches, called VEREFOO (VErified REFinement and Optimized Orchestration). This framework can automatically generate an optimal network configuration from user-defined security requirements. Full automation, formal correctness, and optimization are the main principles that need to be fulfilled. Full automation is achieved because the final network configuration, except for input specification, can be obtained without human intervention. Formal correctness is ensured by solving the MaxSMT problem, which generates a correct solution through hard constraints without requiring a-posteriori verification. Optimization can be reached by solving soft constraints. This thesis is based on this approach to evaluate the performance of the framework for configuring secure communications using VPNs. In particular, a generator is proposed that can create a complex and branched network structure, in which different types of nodes can be inserted. This generator allows the evaluation of the framework's performance in the optimal allocation and configuration of a minimum number of VPN gateways to enable secure communications and traffic protection. Tests are conducted by increasing the size and considering different scenarios to assess the impact of different parameters. The results demonstrate the framework's ability to correctly configure and allocate security functions, even in the presence of a large number of input security requirements. Performance is evaluated according to the execution time taken to find the optimal and correct solution. To achieve the results, two different models, Atomic Flows and Maximal Flows, are used to evaluate which one offered greater advantages when subject to the same conditions.