Automated Analysis and Synthesis for the Compliance of Privacy and Other Legal Provisions

Enforcing legal compliance into software systems is a non-trivial task that requires an interdisciplinary approach. This thesis presents a new methodology for legal compliance checking against European legal provisions, namely the EU Data Protection Directive, the EU General Data Protection Regulation and the revised EU Payment Services Directive. We propose two types of compliance checking mechanisms that should be exploited at design-time or run-time. The former is based on security policy analysis of access control policies. The later is built on top of an approach to synthesizing run-time monitors for workflow-driven applications. Our contributions include a comprehensive methodology for legal compliance checking, the formalization of the regulations and the prototype tool of the implemented compliance methodology.