Raúl Pardo will give a talk about his work on Model-Checking the Implementation of Consent. Details below.
SPEAKER
Raúl Pardo, Prof., ITU.
TITLE
Model-Checking the Implementation of Consent
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 talk, I will introduce 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. I will demonstrate the use of our method in two real world scenarios: an implementation of cookie banners and a IoT system communicating via Bluetooth low energy.
This is a dry-run presentation. The paper will appear in the proceedings of SEFM’24. Pre-print: https://arxiv.org/abs/2409.11803