Formalising privacy regulations with bigraphs

With many governments regulating the handling of user data-the General Data Protection Regulation, the California Consumer Privacy Act, and the Saudi Arabian Personal Data Protection Law-ensuring systems comply with data privacy legislation is of high importance. Checking compliance is a tricky process and often includes many manual elements. We propose that formal methods, that model systems mathematically, can provide strong guarantees to help companies <i>prove</i> their adherence to legislation. To increase usability we advocate a diagrammatic approach, based on bigraphical reactive systems, where privacy experts can explicitly <i>visualise</i> the systems and describe updates, via rewrite rules, that describe system behaviour. The rewrite rules allow flexibility in integrating privacy policies with user-specified systems. We focus on modelling notions of <i>providing consent, withdrawing consent, purpose limitations, the right to access and sharing data with third parties</i>, and define privacy properties that we want to prove within the systems. Properties are expressed using the computation tree logic and proved using model checking. To show the generality of the proposed framework, we apply it to two examples: a bank notification system, inspired by Monzo's privacy policy, and a cloud-based home healthcare system based on the Fitbit app's privacy policy.