Français Anglais
Accueil Annuaire Plan du site
Home > Collaborations > Collaborations
Collaboration with MBTSEC
project collaboration (since Sep 2007)
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.

Research activities:                                                    > Publications
  ° Formalisation of (Specification and Programming) Languages in Proof Assistants
  ° Formal Model-Based Testing

  ° Verification of Algorithms, Languages and Systems

  WOLFF Burkhart

More information: