@InCollection{	  brucker.ea:firewall:2010,
  author	= {Achim D. Brucker and Lukas Br{\"u}gger and Paul Kearney
		  and Burkhart Wolff},
  booktitle	= {Third International Conference on Software Testing,
		  Verification, and Validation (ICST)},
  language	= {USenglish},
  title		= {Verified Firewall Policy Transformations for Test-Case
		  Generation},
  year		= {2010},
  publisher	= {IEEE Computer Society},
  address	= {Los Alamitos, CA, USA},
  categories	= {holtestgen},
  classification= {conference},
  areas		= {security, formal methods},
  public	= {yes},
  isbn		= {978-0-7695-3990-4},
  location	= {Paris, France},
  pages		= {345--354},
  doi		= {10.1109/ICST.2010.50},
  abstract	= {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},
  pdf		= {http://www.brucker.ch/bibliography/download/2010/brucker.ea-firewall-2010.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-firewall-2010}
		  
}