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
Due to copyright restrictions, this file is not available for public download
Click here to request a copy from the OU Author.
DOI (Digital Object Identifier) Link: http://dx.doi.org/10.1007/s10462-009-9147-0
Google Scholar: Look up in Google Scholar

Abstract

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 Article
Copyright Holders: 2009 Springer
ISSN: 0269-2821
Keywords: T802C
Academic Unit/Department: Mathematics, Computing and Technology > Computing & Communications
Interdisciplinary Research Centre: Centre for Research in Computing (CRC)
Item ID: 18801
Depositing User: Arosha Bandara
Date Deposited: 09 Nov 2009 11:57
Last Modified: 12 Dec 2012 19:45
URI: http://oro.open.ac.uk/id/eprint/18801
Share this page:

Actions (login may be required)

View Item
Report issue / request change

Policies | Disclaimer

© The Open University   + 44 (0)870 333 4340   general-enquiries@open.ac.uk