Specification and Verification of Security Policies in Firewalls

Abstract

Rules are used as a way of managing and configuring firewalls to fulfill security requirements in most cases. Managers have to specify their organizational security policies using low level and order-dependent rules. Furthermore, dependency of firewalls to the network topology, frequent changes in network topology (specially in dynamic networks), and lack of a method for analysis and verification of specified security policy may reduce to inconsistencies and security holes. Existence of a higher level environment for security policy specification can rectify part of the problems. In this paper we present a language for high level and formal specification of security policy in firewalls. Using the language, a security manager can configure its firewall based on his required security policy independent of the network topology. The language is used as a framework for analysis and verification of security policies. We designed and implemented a tool based on theorem proving for detecting inconsistencies, coverage, as well as applying a query on the specified policy. Results of analysis can be used to detect security vulnerabilities.