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.

翻译：尽管现代隐私法规（如欧盟的GDPR）规定了“隐私设计”（PbD），但在实际软件系统中实现PbD是一项众所周知的艰巨任务。实现PbD的一种新兴技术是运行时执行（RE），即加载了系统隐私需求规范的实施器观察系统执行的操作，并指示其执行确保始终符合这些要求的操作。为了将RE技术用于PbD，需要先将隐私法规转化为可执行的规范。本文报告了我们在形式化GDPR方面的持续工作。我们首先提出了一组需求和一种迭代方法，用于创建法律条款的可执行形式化规范。随后，我们报告了一项初步案例研究，其中运用该方法推导出GDPR部分条款的可执行规范。该案例研究表明，我们的方法可有效用于开发精确的可执行规范。