Model-Checking the Implementation of Consent
Ra\'ul Pardo, Daniel Le M\'etayer

TL;DR
This paper presents a method to refine high-level GDPR privacy requirements into low-level models using TLA+ and model-checking, ensuring correct implementation in consent management systems across diverse technologies.
Contribution
It introduces a systematic approach to translate GDPR privacy policies into formal models verified by model-checking, aiding developers in compliant system implementation.
Findings
Successfully modeled cookie banners and IoT consent systems.
Verified that low-level models implement GDPR requirements.
Demonstrated applicability in real-world scenarios.
Abstract
Privacy policies define the terms under which personal data may be collected and processed by data controllers. The General Data Protection Regulation (GDPR) imposes requirements on these policies that are often difficult to implement. Difficulties arise in particular due to the heterogeneity of existing systems (e.g., the Internet of Things (IoT), web technology, etc.). In this paper, we propose a method to refine high level GDPR privacy requirements for informed consent into low-level computational models. The method is aimed at software developers implementing systems that require consent management. We mechanize our models in TLA+ and use model-checking to prove that the low-level computational models implement the high-level privacy requirements; TLA+ has been used by software engineers in companies such as Microsoft or Amazon. We demonstrate our method in two real world scenarios:…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCriminal Law and Policy · Law and Political Science · Digitalization, Law, and Regulation
