A Parallelization Approach Via Clusterization for Firewall Configuration

The growing complexity and dynamic nature of modern computer networks pose significant challenges for ensuring their security and correctness. Network misconfigurations are the most common reason for vulnerabilities, most times resulting in security breaches, disruptions of service, as well as non-compliance. Formal verification, a rigorous methodology rooted in mathematical logic, offers the systematic method to understand network configurations and give robust guarantees for their actions and adherence to the security policies. Of the most visible tools in this area is VEREFOO, designed at the Politecnico di Torino, excels for its capacity to efficiently fulfill network needs by allocating firewalls to avoid subtle configuration errors. While VEREFOO has proven highly successful in evading critical bugs, its use on large-scale, enterprise-level networks frequently incur severe performance bottlenecks. Computational cost needed to exhaustively search the entire state space of complex network topologies grows exponentially, leading to unfeasibly long analysis times and memory consumption. This inherent scalability limitation restricts VEREFOO’s practical deployability for eventual real-world deployments where quick verification loops are repeatedly iterated frequently essential for maintaining a strong security posture. This master’s thesis addresses the crucial problem of VEREFOO’s scalability by proposing and assessing a parallelization strategy using network decomposition. The key idea involves intelligently partitioning a large, monolithic network into a set of smaller, more tractable subnetworks. These subnetworks may then be analyzed concurrently by separate instances of VEREFOO. This concurrent processing paradigm leverages modern multi-core architectures, promising a substantial reductions in aggregate verification time. After this phase, an aggregation algorithm is used to collect the individual outputs of verification and aggregate them in a final integral solution. The key benefit of this approach is its high capability to increase the verification speed significantly and to let VEREFOO process high scale networks, thus allowing formal verification becoming increasingly accessible and embedded feature of regular security assurance processes. However, this performance enhancement comes with an acknowledged trade-off: the potential loss of global optimality in the verification solution. By analyzing subnetworks in isolation, certain inter-subnetwork dependencies or global properties that span across partition boundaries might not be fully captured or optimized, leading to a ”good enough” rather than a perfectly optimal solution. Despite this trade-off, the cybersecurity implications are profound. In dynamic environments where frequent integration and quick deployment are essential, a faster, larger scale verification procedure with highly accurate, potentially non-optimum, results are frequently more beneficial than an optimum solution delivered too late. This thesis fills the gap between theoretical rigor and usability for practical network security verification, opening the door to wider and better use of formal methods when securing the critical network infrastructures against evolving cyber threats.