A holistic approach for formal adaptive firewall rule management

Modern network infrastructures require high speeds for multiple services at once and a robust defence against cyber threats. Among these, Denial-of-Service (DoS) attack is a major risk because it consists of flooding systems to make them unavailable. The security provided by conventional firewalls using static rules becomes insufficient when networks experience this type of attack. To address this limitation, this thesis develops a framework that combines verified static configurations with flexible runtime rule distribution. The system integrates VEREFOO (Verified Refinement and Optimized Orchestrator) which generates optimized and formally verified firewall policies at design time with REDIAL (RulE DIstribution ALgorithm) which operates at runtime to distribute rules between cascaded firewalls. This system is evaluated through testing on various hardware systems and in simulated attack environments with the aim to demonstrate the effectiveness of the framework. The test-bed replicated an enterprise border network using heterogeneous hardware. Network namespaces were used to separate the functions of routing and filtering. The control-plane automation used SSH-based scripts while experimental data collection occurred on RAM disks to mitigate packet drops when rates reached high levels. The system handled network traffic by running tests that emulated real-world network operations. Attack traffic consisted of ICMP floods of different payload sizes. The experiments included baseline measurements without a firewall and static configuration followed by deployment of VEREFOO–REDIAL in an integrated system to track throughput, packet loss and retransmission. The baseline measurements showed that unprotected networks became unstable when ICMP floods occurred: small-packet floods broke TCP flows but UDP flows operated at a reduced level. In the final demo, the system integrating the VEREFOO-REDIAL framework proved to be more resistant to attacks. The results show that design-time optimization provides effective configurations when combined with runtime adaptation. There are three primary limitations: (i) hardware differences that make performance evaluation challenging; (ii) the thesis focuses only on ICMP floods; (iii) the use of iptables-legacy instead of modern packet filtering systems. Future work should evaluate the framework against various attack methods and use contemporary packet filtering systems and assess the automated policy update capabilities of the REACT-VEREFOO framework. Furthermore, experiments should be conducted on more homogeneous and powerful hardware.