Automatic Verification of Security Policies in Firewalls with Dynamic Rule Sequence

Security policies play an important role in the security of communication networks. They are normally defined at a high level of abstraction and implemented in firewalls, which are the first defense to secure networks against attacks and unauthorized access. When security policies are implemented in firewalls, anomalities and conflicts that may arise from different policies should be taken into consideration. On the other hand, Firewalls conduct random sequence order shuffling during their operation to prevent certain security attacks. This may result in an incorrect implementation of high level policies that depend on the order of rules inspection in the firewall. This paper presents a formal model of firewall rules sequence and a novel method that verifies the set of security policies when rules sequence changes. The method is tested on synthetic firewall of practical size, where the obtained results demonstrate the ability of firewalls to maintain the functional behavior of security policies during their runtime operation. The detailed analysis shows that the proposed method can be applied on firewalls with dynamic rule sequence in real time.