Formalising privacy regulations with bigraphs

Area of Science:

• Computer Science
• Formal Methods
• Software Engineering

Background:

• Increasingly stringent data privacy regulations (e.g., GDPR, CCPA, PDPL) necessitate robust methods for ensuring system compliance.
• Manual compliance checking is often complex, time-consuming, and prone to errors, highlighting the need for automated and verifiable solutions.

Purpose of the Study:

• To propose a formal methods-based framework for mathematically modeling and verifying data privacy compliance in systems.
• To enhance the usability of formal methods through a diagrammatic approach for privacy experts.

Main Methods:

• Utilizing bigraphical reactive systems for a visual and mathematically rigorous representation of system behavior.
• Employing rewrite rules to model system updates and integrate privacy policies.
• Defining and proving privacy properties (e.g., consent, purpose limitation, data sharing) using Computation Tree Logic (CTL) and model checking.

Main Results:

• Demonstrated the framework's generality by applying it to a bank notification system (inspired by Monzo) and a home healthcare system (inspired by Fitbit).
• Showcased how the formal model can mathematically prove adherence to specific privacy requirements.

Conclusions:

• Formal methods, particularly when combined with a diagrammatic approach like bigraphical reactive systems, provide strong guarantees for data privacy compliance.
• The proposed framework offers a flexible and verifiable method for companies to demonstrate adherence to complex data privacy legislation.