Abstract:


Verified Firewall Policy Transformations for 
Test Case Generation

Achim D. Brucker and Lukas Brügger and 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-TestGenFW. 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.