Docker-based deployment for an optimized security mitigation mechanism

In complex network environments, key roles such as network designers and security managers must collaborate to ensure both functionality and protection. However, miscommunication and human error are common and can result in unintended security vulnerabilities which are potential entry points for cyberattacks, in fact according to the 2022 Data Breach Investigations Report (DBIR), approximately 82% of security breaches involved a human element. To mitigate these issues, automated systems that leverage formal models and ensure formal correctness of results are essential; furthermore, such systems may also improve the reliability of network configurations while optimizing time and resource utilization. This is the context in which VEREFOO (VErified REFinement and Optimized Orchestrator) operates. The framework is specifically designed to automate the complex task of configuring packet filtering firewalls in virtualized networks by transforming high-level Network Security Requirements (NSRs) into optimized and formally verified firewall configurations. It does so by modeling the configuration as a MaxSMT problem instance, combining constraint solving techniques with formal verification to ensure correctness and efficiency. Additionally, in VEREFOO it is possible to integrate Intrusion Detection Systems (IDSs) to detect malicious activity and dynamically react to cyberattacks. Upon detection, the framework triggers an automatic reconfiguration process that updates only the necessary elements of the network topology to contain the threat, thereby minimizing disruption and avoiding full redeployment which is a time-consuming task. This thesis focuses on the design and implementation of a demonstrator aimed at highlighting the efficiency and responsiveness of the VEREFOO framework within a realistic network context. To this end, a custom network topology was developed to closely resemble an enterprise environment, consisting of multiple subnets representing, on the one hand, a data center and, on the other, departmental networks of a generic company. On this topology, a Denial-of-Service attack, specifically an ICMP flooding, was simulated in order to evaluate the framework’s capacity to promptly react to malicious activities. To enable the demonstrator, several modifications and extensions to the framework were carried out. A custom intrusion detection rule for Snort was designed, configured to generate alerts whenever more than ten ICMP echo requests per second are sent by the same source. This ensured that normal administrative operations such as simple pinging remain unaffected, while preventing their misuse for flooding attacks. Moreover, a graphical interface was developed for the demonstrator to guide the user through each step of the process, displaying explanatory messages and offering insights into both its functionality and customization possibilities. Finally, an additional supporting Python script was created to compare the virtual topology before and after the attack, thereby illustrating the automatic reconfigurations applied by the framework and assessing their effectiveness.