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

Obsoleted by:
This publication has been obsoleted by the following publication:
A. D. Brucker, L. Brügger, and B. Wolff, “Formal firewall conformance testing: An application of test and proof techniques,” Software Testing, Verification & Reliability (STVR), vol. 25, no. 1, pp. 34–71, 2015, doi: 10.1002/stvr.1544. Author copy: https://logicalhacking.com/publications/brucker.ea-formal-fw-testing-2014/

Please cite this work as follows:
A. D. Brucker, L. Brügger, P. Kearney, and B. Wolff, “Verified firewall policy transformations for test-case generation,” in Third international conference on software testing, verification, and validation (ICST), Los Alamitos, CA, USA: IEEE Computer Society, 2010, pp. 345–354. doi: 10.1109/ICST.2010.50. Author copy: https://logicalhacking.com/publications/brucker.ea-firewall-2010/

BibTeX
@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 },
  areas       = {security, formal methods},
  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.},
  obsoletedby = {brucker.ea:formal-fw-testing:2014},
  keywords    = {Security Testing, Model-Based Testing},
  note        = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-firewall-2010/}},
  pdf         = {https://logicalhacking.com/publications/brucker.ea-firewall-2010/brucker.ea-firewall-2010.pdf},
}