Modern software systems must comply with increasingly complex regulations in domains ranging from industrial automation to data protection. Runtime enforcement addresses this challenge by empowering systems to not only observe, but also actively control the behavior of target systems by modifying their actions to ensure policy compliance. We propose a novel approach to the proactive real-time enforcement of policies expressed in metric first-order temporal logic (MFOTL). We introduce a new system model, define an expressive MFOTL fragment that is enforceable in that model, and develop a sound enforcement algorithm for this fragment. We implement this algorithm in a new tool called WhyEnf and carry out a case study on enforcing GDPR-related policies. Our tool can enforce all policies from the study in real-time with modest overhead. Our work thus provides the first tool-supported approach that can proactively enforce expressive first-order policies in real time.

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.

In this paper, we develop the first language-based, Privacy by Design approach that provides support for a rich class of privacy policies. These policies may be user-defined, rather than programmer-defined policies, and combine fine-grained information flow policies (considering individual application inputs and outputs) with temporal constraints. Our approach, called Taint, Track, and Control (TTC), combines dynamic information-flow control with runtime enforcement to enforce these policies in the presence of malicious users and developers. We provide semantics and correctness proofs for TTC, formalized using the Isabelle/HOL proof assistant. We also implement our approach in a proof-of-concept web development framework and port three baseline applications from previous work into this framework for evaluation. Overall, our approach enforces expressive user-defined privacy policies with practical runtime performance.

Violations of data protection laws such as the General Data Protection Regulation (GDPR) are ubiquitous. Currently building IT support to implement such laws is difficult and the alternatives such as manual controls augmented by auditing are limited and scale poorly. This calls for developing automated enforcement techniques that can rely on a formalization of the law.

In this paper, we present the first enforceable specification of a comprehensive set of GDPR provisions, and describe an architecture that automatically enforces thisspecification in web applications. We evaluate our architecture by implementing three case studies and show that our approach incurs only modest development and runtime overhead, while covering the most relevant privacy-related aspects of GDPR that can be enforced at runtime.

We introduce Interleave-Disjunction-Lock parallel multiple context-free grammars (IDL-PMCFG), a novel grammar formalism designed to describe the syntax of free word order languages that allow for extensive interleaving of grammatical constituents. Though interleaved constituents, and especially the so-called hyperbaton, are common in several ancient (Classical Latin and Greek, Sanskrit...) and modern (Hungarian, Finnish...) languages, these syntactic structures are often difficult to express in existing formalisms. The IDL-PMCFG formalism combines Seki et al.’s parallel multiple context-free grammars (PMCFG) with Nederhof and Satta’s IDL expressions. We define the semantics of IDL-PMCFGs and study their expressivity, proving that IDL-PMCFG extends both PMCFG and IDL-CFG (context-free grammars equipped with IDL expressions) and that IDL-PMCFG parsing is NP-hard. We then introduce COMPĀ, a programming language extending Ranta’s Grammatical Framework (GF) and built as a high-level front-end formalism to IDL-PMCFG for practical grammar development. We present a parsing algorithm for IDL-PMCFG inspired by earlier Earley-style PMCFG parsing algorithms and Nederhof and Satta’s IDL graphs and give a worst-case estimate of its complexity as a function of several metrics on IDL expressions, the size of the input and a new notion of the G-density of a language.

Correctness and regulatory compliance of today’s software systems are crucial for our safety and security. This can be achieved with policy enforcement: the process of correcting system behavior to satisfy a given policy. The enforcer’s capabilities determine which policies are enforceable.

We study the enforceability of policies specified in metric first-order temporal logic (MFOTL) with enforcers that can cause and suppress different system actions in real time. We show that a formula from an expressive safety fragment of MFOTL is enforceable if and only if it is equivalent to a formula in a simpler, syntactically defined MFOTL fragment. We propose an enforcement algorithm for all monitorable formulae (i.e., formulae whose violations can be detected by manipulating finite sets of satisfying valuations) from the latter fragment, and show that our EnfPoly enforcer tool outperforms state-of-the-art enforcers.

In this thesis, we design and implement the 'Databank Model', a new privacy-preserving web architecture for database-backed applications. The Databank Model aims at making the web more user-centric and safe by separating data storage fromdata processing functions. In this model, data storage and data policy enforcement are delegated to a trusted third party called the Databank, which serves as a proxy between users and applications. Application developers deploy parts of their code which interact with user data directly to the Databank. This allows them to provide their service without retrieving user data. The Databank monitors code executed against its database and prevents violations of its users’ policies. The overall infrastructure provides strong formal guarantees to users that their policies will be correctly enforced.

Through a novel combination of ideas from both information-flow monitoring and runtime verification, we design a realistic Python-like programming language called Dmol, tailored for the development of database-backed web applications. The Dmol' language features both static and dynamic information-flow propagation and uses an external monitoring backend to detect violations of users' policies, specified in a fragment of Metric First-Order Temporal Logic (MFOTL), at runtime. Noninterference properties are proved for this language and user policies are shown to be correctly enforced in the resulting execution model. We implement a prototype of the Databank infrastructure in Python and OCaml with Dmol' as a Databank-side programming language and assess the practicality of our approach in a case study.