Verified Firewall Policy Transformations for Test-Case Generation

by Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff

We present an optimization technique for model-based generation of test cases for firewalls. Based on a formal model for firewall policies in higher-order logic, we derive a collection of semantics-preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage. The correctness of the rules and the algorithm is established by formal proofs in Isabelle/HOL. Finally, we use the normalized policies to generate test cases with the domain-specific firewall testing tool HOL-TestGen/FW.

The resulting procedure is characterized by a gain in efficiency of two orders of magnitude and can handle configurations with hundreds of rules as occur in practice.

Our approach can be seen as an instance of a methodology to tame inherent state-space explosions in test case generation for security policies.

Keywords: security testing, model-based testing
Categories: ,
Documents: (full text as PDF file)

Please cite this article as follows:
Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff. Verified Firewall Policy Transformations for Test-Case Generation. In Third International Conference on Software Testing, Verification, and Validation (ICST), pages 345-354, IEEE Computer Society, 2010.
Keywords: security testing, model-based testing
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1109/ICST.2010.50) ( )