Consent 实现的模型检查
密码学与安全
2024-09-19 v1 软件工程
摘要
隐私政策定义了个人数据由数据控制器收集和处理的条件。通用数据保护条例（GDPR）对这些政策提出了往往难以实施的要求。特别是由于现有系统的异构性（例如，物联网（IoT），Web 技术等），这些要求的实现存在困难。本文提出一种方法，将高层 GDPR 隐私要求（用于知情同意）细化为低层计算模型。该方法旨在需要同意管理的软件开发人员。我们在 TLA+ 中实现这些模型，并使用模型检查证明低层计算模型实现了高层隐私要求；TLA+ 已被微软或亚马逊等公司的软件工程师所采用。我们在两个实际场景中演示了该方法：饼干横幅的实现以及通过低能蓝牙通信的物联网系统。
引用
@article{arxiv.2409.11803,
title = {Model-Checking the Implementation of Consent},
author = {Raúl Pardo and Daniel Le Métayer},
journal= {arXiv preprint arXiv:2409.11803},
year = {2024}
}
备注
Pre-print of paper to appear in the proceedings of SEFM'24