Modeling and verification of firewall configurations using domain restriction method

Firewalls play an important role in the security of communication systems. They are widely adopted for protecting private networks by filtering out undesired network traffic in and out of the secured network. The verification of firewalls is a great challenge because of the dynamic characteristics of their operation, their configuration is highly error prone, and finally, they are considered the first defense to secure networks against attacks and unauthorized access. In this paper, we propose a new approach for modeling and verification of firewall configuration rules using domain restriction method. Our approach is implemented in Event-B formal techniques, where we model firewall configuration rules, and then use invariant checking to verify the consistency of firewall configurations in Event-B theorem proving framework.