|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Euris Cloud Santé (Paris, FRANCE)
and
INRIA Grenoble / CONVECS team (FRANCE)
|
|---|---|
| Method: |
LNT
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Cloud Computing.
|
| Period: |
2023
|
| Size: |
2000 lines of LNT
|
| Description: |
The digitisation of healthcare has revolutionised the efficiency of the
industry in terms of storage, transmission, and processing capabilities
as well as in terms of quality, cost, and time effectiveness of patient
care. Each institution hosting an environment (infrastructure,
application, services, solutions) that manipulates PHI (Personal Health
Information) via EHR (Electronic Health Record) needs to comply to the
security regulations enforced by the local regulating authorities.
To this end, all activities (system logs, application logs, user
activities, operations performed, etc.) must be logged and stored in
a secure manner.
φ-comp is a security compliance monitoring and management solution for sensitive health data environments, which respects existing security regulations. The monitored data are reported and classified with respect to four security areas (confidentiality, integrity, availability, traceability). These data are analysed by security area and further evaluated into three levels of risk, namely nominal behaviour, potential threat, and non-compliant behaviour. In the last case, risk mitigation actions are automatically performed so as to reduce the level of risk and restore a compliant behaviour. Monitored data and performed mitigation actions are stored in logs for subsequent auditing and for generating compliance reports for the hosting institution and (upon request) for supervising authorities. Since the security of health data is crucial, there is a need of guarantees in terms of correctness of the φ-comp approach. This work consisted in building a formal model in LNT of φ-comp representing all the components of the solution's architecture, as well as the behaviour of all components including the way they interact together. Then, several important properties of interest were formalised in MCL and verified using CADP on the LNT models of φ-comp in conjunction with several realistic applications. The experiments carried out on these applications confirmed that all properties were satisfied, thus convincing the protocol's designers of the correctness of the φ-comp solution. |
| Conclusions: |
This is one of the first attempts to use formal verification techniques
for cloud platforms dealing with healthcare. The main perspective of
this work is to improve the current management protocol by using
blockchains to store the health data in a secure way, while providing
traceability and transparency of the approach.
|
| Publications: |
[Cuci-Ozeer-Salaun-23]
Almo Cuci, Umar Ozeer, and Gwen Salaün.
"Modelling and Verification of an Application for Managing Sensitive
Health Data". Proceedings of the 11th International Symposium From Data
to Models and Back (DATAMOD'2023), Eindhoven, The Netherlands, Lecture
Notes in Computer Science vol. 14618, pp. 127-141. Springer Verlag,
November 2023.
Available on-line at: https://hal.inria.fr/hal-05066343/en |
| Contact: | Gwen Salaün INRIA Centre of University Grenoble Alpes 655, avenue de l'Europe F-38330 Montbonnot Saint Martin FRANCE Email: gwen.salaun@inria.fr |
| Further remarks: | This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page