Optimizing distributed firewall reconfiguration transients

The flexibility and dynamism brought over by softwarization for network management have increased the frequency of configuration changes. In this context, when a distributed security function is subject to a series of configuration changes, a problem that arises is the preservation of the security. The transient from the application of the first change to the last one may present unsecure temporary states, where the required security protection is missing. Establishing a safe scheduling of the configuration changes can significantly limit the number of unsecure states and decrease the time period where the network may be at risk. However, the literature challenged this problem only for centralized firewalls or SDN switches, and without applying formal methods to ensure the correctness of the computed scheduling. In order to overcome these limitations, this paper addresses the problem for distributed firewalls, aiming to satisfy the largest number of user-specified network security policies in each transient state. To this end, it proposes a formal methodology relying on the combination of three main features: automation, formal verification and optimization. This combination is achieved by pursuing a correctness-by-construction approach, based on the formulation of a Maximum Satisfiability Modulo Theories problem. A framework has been developed on the basis of this methodology, so that validation tests have been experimentally executed to assess the feasibility, efficacy and scalability of the approach.