Verification of security policy filtering rules by Model Checking

One of the very important tasks, a computer network (or security) administrator has to fulfill under constructing a (distributed) firewall security policy, is to guarantee the absence of inconsistencies (or anomalies) and possibility to implement the policy in the given network configuration. The paper outlines an approach to verification of filtering rules of firewalls. The approach is intended for detection and resolution of filtering anomalies in the specification of security policy of computer networks. It is based on Model Checking technique. The paper proposes the models of computer networks, the models of firewalls and filtering anomalies, as well as an algorithm of detection of such anomalies. We suggest also a method for verification of filtering rules based on the mentioned models. The main peculiarities of the approach consist in using Model Checking exactly to detect the anomalies of filtering rules and in ability to specify temporal parameters in filtering rules.