Model-based Testing of Security Policies

The goal of this project is to use security policies as model-based specifications and to derive test-cases for them. The policies are specified in Higher-order logic and we use HOL-TestGen, a test-case generator based on the theorem prover Isabelle/HOL to generate the test cases. This approach has already been applied to automatically generate test-cases for firewall policies - for both stateless and stateful firewalls.

Currently, we are investigating the security policies for a large-scale patient data-management system: the access framework for the National Program for IT in the NHS England (NPfIT). We focus on the policies governing access to the Summary Care Records held in the SPINE. Access to patient data in this system is governed by several concepts:

• Role-based Access Control
• Legitimate Relationships
• Patient's Consent
• Sealed Envelopes

The combination of these different concepts serves as a challenging scenario for model-based policy specification, policy analysis, and policy testing.

• Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. An Approach to Modular and Testable Security Models of Real-world Health-Care Applications. In ACM symposium on access control models and technologies (SACMAT), ACM Press, 2011.
  [PDF][Presentation]
• Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. Verified firewall policy transformations for test case generation. In Ana Cavalli and Sudipto Ghosh, editors, International Conference on Software Testing (ICST10). Springer-Verlag, 2010. [PDF] [Presentation]
• Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Model-based Firewall Conformance Testing. In Testcom/FATES 2008. Lecture Notes in Computer Science Springer-Verlag, 2008.
  (PDF), (© Springer-Verlag)
• Achim D. Brucker and Burkhart Wolff. Test-Sequence Generation with HOL-TestGen - With an Application to Firewall Testing. In TAP 2007: Tests And Proofs. Lecture Notes in Computer Science 4454, Springer-Verlag, 2007.
  (PDF), (© Springer-Verlag)
• Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Verifying Test-Hypotheses - An Experiment in Test and Proof. In Model-based Testing (MBT 2008). Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2008.
  (PDF)

• An Approach to Modular and Testable Security Models of Real-world Health-Care Applications. Talk given at Sacmat 2011, Innsbruck, Austria. 15/06/2011 [Slides]
• Model-based Security Testing of Real-world Health-Care System Applications CS-Department Colloquium, Univ. York, UK [Slides]
• Verified firewall policy transformations for test case generation Talk given at ICST 2010, Paris. 08/04/2010 [Slides]
• Model-driven Security applied to Firewalls and the NHS Talk given at BT, Adastral Park, Ipswich. 04/11/2008 [Slides]
• Sicherheit von Elektronischen Gesundheitsakten. Ein Vergleich.
  Talk given at the Nationales Centrum für Tumorerkrankungen (NCT) Heidelberg. 29/09/2008. In German. [Slides]

The project is funded by BT Group plc and carried out by a collaboration between the Information Security Group at ETH Zurich and the LRI of the University Paris-Sud (Orsay). The involved persons are:

• Lukas Brügger, Information Security, ETH Zurich
• Prof. David Basin, Information Security, ETH Zurich
• Dr. Paul Kearney, BT Group plc
• Prof. Burkhart Wolff, LRI, University Paris-Sud (Orsay)
• Dr. Achim D. Brucker, SAP Research, Germany

Lukas Brügger