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.