HOL-TestGen/FW: An Environment for Specification-based Firewall Conformance Testing

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

The HOL-TestGen environment is conceived as a system for modeling and semi-automated test generation with an emphasis on expressive power and generality. However, its underlying technical framework Isabelle/HOL supports the customization as well as the development of highly automated add-ons working in specific application domains.

In this paper, we present HOL-TestGen/FW, an add-on for the test framework HOL-TestGen, that allows for testing the conformance of firewall implementations to high-level security policies. Based on generic theories specifying a security-policy language, we developed specific theories for network data and firewall policies. On top of these firewall specific theories, we provide mechanisms for policy transformations based on derived rules and adapted code-generators producing test drivers. Our empirical evaluations shows that HOL-TestGen/FW is a competitive environment for testing firewalls or high-level policies of local networks.

Keywords:
Symbolic Test Case Generations, Black Box Testing, Theorem Proving, Network Security, Firewall Testing, Conformance Testing

Please cite this work as follows:
A. D. Brucker, L. Brügger, and B. Wolff, “HOL-TestGen/FW: An environment for specification-based firewall conformance testing,” in International colloquium on theoretical aspects of computing (ICTAC), Z. Liu, J. Woodcock, and H. Zhu, Eds. Heidelberg: Springer-Verlag, 2013, pp. 112–121. doi: 10.1007/978-3-642-39718-9_7. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-testgen-fw-2013/

BibTeX
@InCollection{ brucker.ea:hol-testgen-fw:2013,
  abstract  = {The HOL-TestGen environment is conceived as a system for
               modeling and semi-automated test generation with an emphasis
               on expressive power and generality. However, its underlying
               technical framework Isabelle/HOL supports the customization as
               well as the development of highly automated add-ons working in
               specific application domains.
               
               In this paper, we present HOL-TestGen/FW, an add-on for the
               test framework HOL-TestGen, that allows for testing the
               conformance of firewall implementations to high-level security
               policies. Based on generic theories specifying a
               security-policy language, we developed specific theories for
               network data and firewall policies. On top of these firewall
               specific theories, we provide mechanisms for policy
               transformations based on derived rules and adapted
               code-generators producing test drivers. Our empirical
               evaluations shows that HOL-TestGen/FW is a competitive
               environment for testing firewalls or high-level policies of
               local networks.},
  keywords  = {Symbolic Test Case Generations, Black Box Testing, Theorem
               Proving, Network Security, Firewall Testing, Conformance
               Testing},
  location  = {Shanghai},
  author    = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  booktitle = {International Colloquium on Theoretical Aspects of Computing
               (ICTAC)},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {8049},
  doi       = {10.1007/978-3-642-39718-9_7},
  editor    = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
  title     = {{HOL-TestGen}/{FW}: An Environment for Specification-based
               Firewall Conformance Testing},
  areas     = {security, formal methods},
  year      = {2013},
  pages     = {112--121},
  isbn      = {978-3-642-39717-2},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-hol-testgen-fw-2013/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-hol-testgen-fw-2013/brucker.ea-hol-testgen-fw-2013.pdf},
}