TY - CHAP AU - Brucker, Achim D. AU - Brügger, Lukas AU - Wolff, Burkhart ED - Liu, Zhiming ED - Woodcock, Jim ED - Zhu, Huibiao PY - 2013 DA - 2013// TI - HOL-TestGen/FW: An Environment for Specification-based Firewall Conformance Testing BT - International Colloquium on Theoretical Aspects of Computing (ICTAC) T3 - Lecture Notes in Computer Science SP - 112 EP - 121 IS - 8049 PB - Springer-Verlag CY - Heidelberg KW - symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing AB - 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. SN - 978-3-642-39717-2 L1 - https://www.brucker.ch/bibliography/download/2013/brucker.ea-hol-testgen-fw-2013.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-fw-2013 UR - https://doi.org/10.1007/978-3-642-39718-9_7 DO - 10.1007/978-3-642-39718-9_7 LA - USenglish ID - brucker.ea:hol-testgen-fw:2013 ER -