Skip to main content
Article
Using model checking to test a firewall : A case study.
Information Technology papers
  • Padmanabhan Krishnan, Bond University
  • Danita Hartley, University of Canterbury, New Zealand
Date of this Version
7-1-2002
Document Type
Conference Proceeding
Publication Details
Padmanabhan Krishnan and Danita Hartley (2002) Using model checking to test a firewall : A case study. In: Proceedings of the Euromicro Conference: Software Process and Product Improvement, pp 284-293, Dortmund, Germany, 2002.
Copyright © IEEE 2002.

Published by the Institute of Electrical and Electronics Engineers (IEEE)
Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
Abstract

This paper summarises our experience in using model checking technology to test concurrent programs. We use the tool Verisoft to understand various aspects of a firewall tool kit by instrumenting three components of the firewall tool kit with hooks to test their behaviour. Some of the key changes include changing socket communication to message passing queues and adding appropriate synchronisations so that the behaviour of the system can be tracked. We aim to minimize the number of changes to the original source code so that its original behaviour is not affected. The main conclusion is that it is possible to inspect source code with a view towards verifying key behavioural properties without understanding the entire behaviour of the system.

Citation Information
Padmanabhan Krishnan and Danita Hartley. "Using model checking to test a firewall : A case study." (2002)
Available at: http://works.bepress.com/paddy_krishnan/8/