Analysis and Enhancement of the Automatic VPNs Configuration

In today's rapidly evolving Information Technology landscape, automation is a key objective across all sectors, including cybersecurity. The security of a system can be completely compromised by even the minor of configuration errors, highlighting the importance of minimizing human intervention in security configurations. Manual configuration of security systems, such as VPNs and packet filters, is not only prone to errors but also likely to result in suboptimal solutions: studies have shown that even seasoned security experts can introduce anomalies and errors when configuring complex systems manually. Therefore, automating such crucial tasks would greatly improve the overall quality and effectiveness of a network's security, while minimizing the attack surface exploitable by potential attackers. The VEREFOO (VErified REFinement and Optimized Orchestrator) framework perfectly fits the role of a tool capable of automating the allocation and configuration of security systems, producing as output network configurations that are both correct and optimal. VEREFOO is a framework developed at Politecnico di Torino which lays its foundation on the formal methods approach, whose core design allows the achievement of three important goals: firstly, ensuring formal correctnes of the produced solution by construction; secondly, optimization by selecting the most efficient option in the solution space; finally, as a consequence of the first two, eliminating the need for post-verification. This thesis aims to analyze the problem of automating the allocation and configuration of VPNs from both conceptual and practical perspectives, and enhance the implementation of the approach in VEREFOO. In particular, the thesis focuses on the analysis of how VEREFOO manages the formulation of the VPNs' configuration process as a Maximum Satisfiability Modulo Theories (MaxSMT) problem: starting from the generation of the network flows and constraints applied to the Network Security Functions (NSF) allocated on the graph, the analysis examines every computational step that ultimately leads to the production of the final outcome. Through careful code reviews and debugging, the objective is to detect and fix the issues affecting the current version of the framework, while also studying new optimization strategies to enhance the tool's performance. The analysis revealed several defects in the framework's code, such as inefficient generation of constraints, an incorrect assignment of weights and grouping of constraints, imprecise generation of the various flow path and a redundancy issue affecting the quality of the output solution. Additionally, for not-yet resolved challenges like the achievement of feasible performances when managing large-sized networks, various strategies and approaches are proposed. The intrinsic complexity of the VPNs auto-configuration problem leaves very little room for sub-optimizations, especially related to the generation of constraints, as they can lead to unexpected and ambiguous output scenarios. Finally, an evaluation of the current framework's implementation is presented, in order to assess its strengths and weaknesses. The evaluation offers insights into areas where VEREFOO, and more broadly, the state of the art of VPNs automatic configuration, can advance in the future.