pdfreaders.org

Verified Firewall Policy Transformations for Test-Case Generation

Achim D. Brucker, Lukas Brügger, Paul Kearney und Burkhart Wolff

Cover for brucker.ea:firewall:2010.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.

Schlüsselwörter: security testing, model-based testing
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:firewall:2010.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker, Lukas Brügger, Paul Kearney und Burkhart Wolff. Verified Firewall Policy Transformations for Test-Case Generation. In Third International Conference on Software Testing, Verification, and Validation (ICST), pages 345-354, IEEE Computer Society, 2010.
Schlüsselwörter: security testing, model-based testing
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1109/ICST.2010.50) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ brucker.ea:firewall:2010,
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.},
address = {Los Alamitos, CA, USA},
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)},
doi = {10.1109/ICST.2010.50},
isbn = {978-0-7695-3990-4},
keywords = {security testing, model-based testing},
language = {USenglish},
location = {Paris, France},
pages = {345--354},
pdf = {https://www.brucker.ch/bibliography/download/2010/brucker.ea-firewall-2010.pdf},
publisher = {IEEE Computer Society},
title = {Verified Firewall Policy Transformations for Test-Case Generation},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-firewall-2010},
year = {2010},
}