The Open UniversitySkip to content

A formal logic approach to firewall packet filtering analysis and generation

Govaerts, John; Bandara, Arosha and Curran, Kevin (2009). A formal logic approach to firewall packet filtering analysis and generation. Artificial Intelligence Review, 29(3-4) pp. 223–248.

Full text available as:
Full text not publicly available (Version of Record)
Due to publisher licensing restrictions, this file is not available for public download
DOI (Digital Object Identifier) Link:
Google Scholar: Look up in Google Scholar


Recent years have seen a significant increase in the usage of computers and their capabilities to communicate with each other.With this has come the need for more security and firewalls have proved themselves an important piece of the overall architecture, as the body of rules they implement actually realises the security policy of their owners. Unfortunately, there is little help for their administrators to understand the actual meaning of the firewall rules. This work shows that formal logic is an important tool in this respect, because it is particularly apt at modelling real-world situations and its formalism is conductive to reason about such a model. As a consequence, logic may be used to prove the properties of the models it represents and is a sensible way to go in order to create those models on computers to automate such activities. We describe here a prototype which includes a description of a network and the body of firewall rules applied to its components. We were able to detect a number of anomalies within the rule-set: inexistent elements (e.g. hosts or services on destination components), redundancies in rules defining the same action for a network and hosts belonging to it, irrelevance as rules would involve traffic that would not pass through a filtering device, and contradiction in actions applied to elements or to a network and its hosts. The prototype produces actual firewall rules as well, generated from the model and expressed in the syntax of IPChains and Cisco's PIX.

Item Type: Journal Item
Copyright Holders: 2009 Springer
ISSN: 1573-7462
Keywords: formal logic; Internet security; fire walls; logic programming; network modelling
Academic Unit/School: Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
Faculty of Science, Technology, Engineering and Mathematics (STEM)
Research Group: Centre for Research in Computing (CRC)
Item ID: 18801
Depositing User: Arosha Bandara
Date Deposited: 09 Nov 2009 11:57
Last Modified: 11 Dec 2018 20:55
Share this page:


Altmetrics from Altmetric

Citations from Dimensions

Actions (login may be required)

Policies | Disclaimer

© The Open University   contact the OU