Modelling Privacy Compliance in Cross-border Data Transfers with Bigraphs

TL;DR

This work introduces a bigraph-based framework for modelling and automatically verifying GDPR-compliant cross-border data transfers. By encoding regulatory requirements as reusable reaction rules and checking properties with CTL through PRISM, the approach demonstrates rigorous, automated validation of data flows, exemplified on WhatsApp. The integration is supported by sorting disciplines and multiple perspectives (system, sender/receiver types, and locations) to ensure well-formed models and facilitate collaboration between engineers and privacy experts. The results indicate that formal methods can effectively capture spatial and contractual aspects of data transfers, enabling evidence-based compliance and violation detection in real-world policies. Future directions include expanding safeguards, handling user-consent scenarios, and broader application to real systems with automated sorting generation.

Abstract

Advancements in information technology have led to the sharing of users' data across borders, raising privacy concerns, particularly when destination countries lack adequate protection measures. Regulations like the European General Data Protection Regulation (GDPR) govern international data transfers, imposing significant fines on companies failing to comply. To achieve compliance, we propose a privacy framework based on Milner's Bigraphical Reactive Systems (BRSs), a formalism modelling spatial and non-spatial relationships between entities. BRSs evolve over time via user-specified rewriting rules, defined algebraically and diagrammatically. In this paper, we rely on diagrammatic notations, enabling adoption by end-users and privacy experts without formal modelling backgrounds. The framework comprises predefined privacy reaction rules modelling GDPR requirements for international data transfers, properties expressed in Computation Tree Logic (CTL) to automatically verify these requirements with a model checker and sorting schemes to statically ensure models are well-formed. We demonstrate the framework's applicability by modelling WhatsApp's privacy policies.

Figures (25)

• Figure 1: Overview of our bigraph-based privacy framework: The teal box represents the system entities and rules that end-users should specify. The process starts by combining the privacy framework with the system's entities and rules (via links) into a unified model. This combined model is then analysed using BigraphER and the PRISM model checker to prove the privacy properties. If the verification result is true, it indicates that the system meets the GDPR requirements for cross-border data transfers. If false, the system model should be fixed to address the identified issues, after which it is reanalysed. This loop continues until the system passes verification.
• Figure 2: (a) A bigraph representing the initial state of a $\mathsf{WhatsApp}$ system that transfers $\mathsf{Data}$ to $\mathsf{Facebook}$; (b) Rule transD transfers the $\mathsf{Data}$ from $\mathsf{WhatsApp}$ to $\mathsf{Facebook}$; (c) The result of applying rule transD to the initial state, where $\mathsf{Facebook}$ acquires the $\mathsf{Data}$.
• Figure 3: A partial initial state for the WhatsApp example. System-specific entities are shaded in teal. The predefined privacy model appears within the uncoloured regions.
• Figure 4: The process of checking the sender's and receiver's regions by tagging the pointers linked to their specified types.
• Figure 5: sameReg: the sender and the receiver are in the same region.