An Approach to Modular and Testable Security Models of Real-world Health-care Applications

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

We present a generic modular policy modelling framework and instantiate it with a substantial case study for model-based testing of some key security mechanisms of applications and services of the NPfIT. NPfIT, the National Programme for IT, is a very large-scale development project aiming to modernise the IT infrastructure of the NHS in England. Consisting of heterogeneous and distributed applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features.

We model the four information governance principles, comprising a role-based access control model, as well as policy rules governing the concepts of patient consent, sealed envelopes and legitimate relationship. The model is given in HOL and processed together with suitable test specifications in the HOL-TestGen system, that generates test sequences according to them. Particular emphasis is put on the modular description of security policies and their generic combination and its consequences for model-based testing.

Supplementary material:
[  Formalization  ]

Please cite this work as follows:
A. D. Brucker, L. Brügger, P. Kearney, and B. 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), 2011, pp. 133–142. doi: 10.1145/1998441.1998461. Author copy: https://logicalhacking.com/publications/brucker.ea-model-based-2011/

BibTeX
@InProceedings{ brucker.ea:model-based:2011,
  title           = {An Approach to Modular and Testable Security Models of
                     Real-world Health-care Applications},
  author          = {Achim D. Brucker and Lukas Br{\"u}gger and Paul Kearney and
                     Burkhart Wolff},
  booktitle       = {ACM symposium on access control models and technologies
                     (SACMAT) },
  language        = {USenglish},
  publisher       = {ACM Press },
  address         = {New York, NY, USA },
  location        = {Innsbruck, Austria},
  areas           = {security, formal methods},
  year            = {2011},
  copyright       = {ACM},
  copyrighturl    = {https://dl.acm.org/authorize?431936},
  pages           = {133--142},
  abstract        = {We present a generic modular policy modelling framework and
                     instantiate it with a substantial case study for model-based
                     testing of some key security mechanisms of applications and
                     services of the NPfIT. NPfIT, the National Programme for IT,
                     is a very large-scale development project aiming to modernise
                     the IT infrastructure of the NHS in England. Consisting of
                     heterogeneous and distributed applications, it is an ideal
                     target for model-based testing techniques of a large system
                     exhibiting critical security features.
                     
                     We model the four information governance principles,
                     comprising a role-based access control model, as well as
                     policy rules governing the concepts of patient consent, sealed
                     envelopes and legitimate relationship. The model is given in
                     HOL and processed together with suitable test specifications
                     in the HOL-TestGen system, that generates test sequences
                     according to them. Particular emphasis is put on the modular
                     description of security policies and their generic combination
                     and its consequences for model-based testing.},
  doi             = {10.1145/1998441.1998461},
  isbn            = {978-1-4503-0688-1},
  supplementary01 = {https://www.isa-afp.org/entries/UPF.html},
  supplabel01     = {Formalization},
  note            = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-model-based-2011/}},
  pdf             = {https://logicalhacking.com/publications/brucker.ea-model-based-2011/brucker.ea-model-based-2011.pdf},
}