DataProVe: Fully Automated Conformance Verification Between Data Protection Policies and System Architectures

Authors: Vinh Thong Ta (Edge Hill University, Ormskirk, UK), Max Hashem Eiza (Liverpool John Moores University, Liverpool, UK)

Volume: 2022
Issue: 1
Pages: 565–585
DOI: https://doi.org/10.2478/popets-2022-0028

artifact

Download PDF

Abstract: Privacy and data protection by design are relevant parts of the General Data Protection Regulation (GDPR), in which businesses and organisations are encouraged to implement measures at an early stage of the system design phase to fulfil data protection requirements. This paper addresses the policy and system architecture design and propose two variants of privacy policy language and architecture description language, respectively, for specifying and verifying data protection and privacy requirements. In addition, we develop a fully automated algorithm based on logic, for verifying three types of conformance relations (privacy, data protection, and functional conformance) between a policy and an architecture specified in our languages’ variants. Compared to related works, this approach supports a more systematic and fine-grained analysis of the privacy, data protection, and functional properties of a system. Our theoretical methods are then implemented as a software tool called DataProVe and its feasibility is demonstrated based on the centralised and decentralised approaches of COVID-19 contact tracing applications.

Keywords: privacy, GDPR, formal verification, security

Copyright in PoPETs articles are held by their authors. This article is published under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 license.