Model checking a firewall for anomalies

Firewall is the primary network security specified in form of rules that dictate what would and would not be passed to a secured network. Network administrators need to undertake a lot of manual task to get the correct configuration for securing the organization´s network resources. Therefore filter properties called anomalies that hint at possible misconfigurations have been introduced. Verification of firewalls for identification of anomalies is a challenging task. We propose to do this within a formal framework using a custom built model checker.