Security Infrastructures

Security infrastructures are a particularly interesting line of application of testing techniques. Security infrastuctures can be

  • access-control mechanisms on the level of operating systems,
  • network-infrastructure (firewalls and network-adress-translators),
  • complex data-base systems (such as the patient record in the British-Telecom-Spine) or
  • usage control mechanisms that prevent at the operating system level, for example, copying audio-files and its streaming-derivatives to other files due to unsufficient copyrights. 

Security infrastructures are ideal targets for blackbox-testing approaches.

In the HOL-TestGen library,  a particular infrastructure for the specification and test-case generation of security policies have been devceloped: the unified policy framework UPF. UPF is defined directly in Higher-order Logic and provides a number of fundamental operators for the construction of (higher-order) policies and their composition. These operators enjoy a large number of (formally proven) algebraic properties that can be used for (formally proven) pre-normalisation processes, that transform large policy rule-sets into equivalent ones for which test-case-generation is structurally simpler.

These techniques have been used to test individual firewalls, properties networks comprising firewalls and NAT's, access-control-policies in the area of health-record-management systems and are currently adapted to access control policies occurring in personal information management systems (PIMS).



[] Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff. An Approach to Modular and Testable Security Models of real-world health-care Applications. Proceedings of the ACM Symposium on Access control models and technologies, pages 133-142. ACM, 2011. SACMAT 2011. [ bib | .pdf]
[] Achim D. Brucker and Burkhart Wolff. HOL-TestGen: An Interactive Test-case Generation Framework. In Marsha Chechik and Martin Wirsing, editors, Fundamental Approaches to Software Engineering (FASE09), number 5503 in Lecture Notes in Computer Science, pages 417-420. Springer-Verlag, Heidelberg, 2009. [ bib | DOI | http | .ps.gz | .pdf ]
[] Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Model-based Firewall Conformance Testing. In Kenji Suzuki and Teruo Higashino, editors, Testcom/FATES 2008, LNCS 5047, pages 103-118. Springer-Verlag, Tokyo, Japan, 2008. [ bib | DOI | http | .pdf ]
[] Achim D. Brucker and Burkhart Wolff. Test-sequence Generation with HOL-Testgen - with an application to firewall testing. In Bertrand Meyer and Yuri Gurevich, editors, TAP 2007: Tests And Proofs, number 4454 in Lecture Notes in Computer Science, pages 149-168. Springer-Verlag, Zurich, 2007. [ bib | DOI | http | .ps.gz | .pdf ]
[] Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Jens Grabowski and Brian Nielsen, editors, Formal Approaches to Testing of Software (FATES 04), LNCS 3395, pages 16-32. Springer-Verlag, Linz 04, 2005. [ bib | DOI | http ]

Related Research Activities

Related Projects


You are here Application Domains Security Infrastructures