Model-based Firewall Conformance Testing

By Achim D. Brucker, Lukas Brügger, and Burkhart Wolff.

Firewalls are a cornerstone of todays security infrastructure for networks. Their configuration, implementing a firewall policy, is inherently complex, hard to understand, and difficult to validate.

We present a substantial case study performed with the model-based testing tool HOL-TestGen. Based on a formal model of firewalls and their policies in HOL, we first present a derived theory for simplifying policies. We discuss different test plans for test specifications. Finally, we show how to integrate these issues to a domain-specific firewall testing tool HOL-TestGen/FW.

Keywords:
Security Testing, Model-based Testing, Firewall, Conformance 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: http://logicalhacking.com/publications/brucker.ea-formal-fw-testing-2014/

Please cite this work as follows:
A. D. Brucker, L. Brügger, and B. Wolff, “Model-based firewall conformance testing,” in Testcom/FATES 2008, K. Suzuki and T. Higashino, Eds. Heidelberg: Springer-Verlag, 2008, pp. 103–118. doi: 10.1007/978-3-540-68524-1_9. Author copy: http://logicalhacking.com/publications/brucker.ea-model-based-2008/

BibTeX
@InCollection{ brucker.ea:model-based:2008,
  abstract    = {Firewalls are a cornerstone of todays security infrastructure
                 for networks. Their configuration, implementing a firewall
                 policy, is inherently complex, hard to understand, and
                 difficult to validate.
                 
                 We present a substantial case study performed with the
                 model-based testing tool HOL-TestGen. Based on a formal model
                 of firewalls and their policies in HOL, we first present a
                 derived theory for simplifying policies. We discuss different
                 test plans for test specifications. Finally, we show how to
                 integrate these issues to a domain-specific firewall testing
                 tool HOL-TestGen/FW.},
  editor      = {Kenji Suzuki and Teruo Higashino},
  location    = {Tokyo, Japan},
  author      = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  booktitle   = {Testcom/FATES 2008},
  language    = {USenglish},
  publisher   = {Springer-Verlag },
  address     = {Heidelberg },
  series      = {Lecture Notes in Computer Science },
  number      = {5047},
  doi         = {10.1007/978-3-540-68524-1_9},
  pages       = {103--118},
  title       = {Model-based Firewall Conformance Testing},
  areas       = {security, formal methods},
  keywords    = {Security Testing, Model-based Testing, Firewall, Conformance
                 Testing},
  year        = {2008},
  obsoletedby = {brucker.ea:formal-fw-testing:2014},
  note        = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-model-based-2008/}},
}