Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards an Enforceable GDPR Specification

François Hublet, Alexander Kvamme, Srđan Krstić

TL;DR

The paper addresses the challenge of translating GDPR into enforceable specifications suitable for runtime enforcement to realize Privacy by Design. It proposes four requirements and an iterative TE-LE collaboration methodology to produce enforceable, transparent, and instrumentable specifications, demonstrated through a GDPR case study that refines prior formalisms. By adopting Metric First-Order Temporal Logic (MFOTL) as the target specification language and converting DAPRECO-derived GDPR material, the authors reveal several inaccuracies in existing work and illustrate how MFOTL can capture time-based regulatory constraints and be checked by tools like WhyEnf. The results suggest a practical path toward RE-enabled privacy compliance and highlight the need for broader regulatory coverage, interdisciplinary collaboration, and user-friendly temporal formalisms for real-world deployment.

Abstract

While Privacy by Design (PbD) is prescribed by modern privacy regulations such as the EU's GDPR, achieving PbD in real software systems is a notoriously difficult task. One emerging technique to realize PbD is Runtime enforcement (RE), in which an enforcer, loaded with a specification of a system's privacy requirements, observes the actions performed by the system and instructs it to perform actions that will ensure compliance with these requirements at all times. To be able to use RE techniques for PbD, privacy regulations first need to be translated into an enforceable specification. In this paper, we report on our ongoing work in formalizing the GDPR. We first present a set of requirements and an iterative methodology for creating enforceable formal specifications of legal provisions. Then, we report on a preliminary case study in which we used our methodology to derive an enforceable specification of part of the GDPR. Our case study suggests that our methodology can be effectively used to develop accurate enforceable specifications.

Towards an Enforceable GDPR Specification

TL;DR

The paper addresses the challenge of translating GDPR into enforceable specifications suitable for runtime enforcement to realize Privacy by Design. It proposes four requirements and an iterative TE-LE collaboration methodology to produce enforceable, transparent, and instrumentable specifications, demonstrated through a GDPR case study that refines prior formalisms. By adopting Metric First-Order Temporal Logic (MFOTL) as the target specification language and converting DAPRECO-derived GDPR material, the authors reveal several inaccuracies in existing work and illustrate how MFOTL can capture time-based regulatory constraints and be checked by tools like WhyEnf. The results suggest a practical path toward RE-enabled privacy compliance and highlight the need for broader regulatory coverage, interdisciplinary collaboration, and user-friendly temporal formalisms for real-world deployment.

Abstract

While Privacy by Design (PbD) is prescribed by modern privacy regulations such as the EU's GDPR, achieving PbD in real software systems is a notoriously difficult task. One emerging technique to realize PbD is Runtime enforcement (RE), in which an enforcer, loaded with a specification of a system's privacy requirements, observes the actions performed by the system and instructs it to perform actions that will ensure compliance with these requirements at all times. To be able to use RE techniques for PbD, privacy regulations first need to be translated into an enforceable specification. In this paper, we report on our ongoing work in formalizing the GDPR. We first present a set of requirements and an iterative methodology for creating enforceable formal specifications of legal provisions. Then, we report on a preliminary case study in which we used our methodology to derive an enforceable specification of part of the GDPR. Our case study suggests that our methodology can be effectively used to develop accurate enforceable specifications.
Paper Structure (14 sections, 6 equations, 4 figures)

This paper contains 14 sections, 6 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Related work
  3. Runtime enforcement
  4. System model.
  5. Specification.
  6. Properties of policies.
  7. Requirements and methodology
  8. Requirements.
  9. Methodology.
  10. Case study
  11. Formalism selection and conversion.
  12. Deriving an enforceable formal specification of Art. 7(1).
  13. Discussion.
  14. Conclusion and open questions

Figures (4)

  • Figure 1: System model for runtime enforcement
  • Figure 2: Syntax and semantics of selected MFOTL operators.
  • Figure 3: Summary of requirements
  • Figure 4: Flowchart of our methodology