Transforming Privacy Policies to Auditing Specifications

With more and more personal data being collected and stored by service providers, there is an increasing need to ensure that their usage is compliant with privacy regulations. We consider the specific scenario where policies are defined in metric temporal logic and audited against the database usage logs. Previous works have shown that this can indeed be achieved in an efficient manner for a very expressive set of policies. One of the main ingredients of such an auditing process is the availability of sufficient database logs. Currently, it is a manual process to first determine the logs needed, and then come up with the necessary auditing specifications to generate them. This is not only a time consuming process but can be erroneous as well, leading to either insufficient or redundant logging. Logging in general is costly as it is an overhead on the real-time database performance, and hence redundant logging is not an alternative either. Our contribution in this work is to streamline the log generation process by deriving the auditing specifications directly from the policies to be audited. We also show how the required logging can be minimized based on the temporal constraints specified in the policies. Given privacy policies as input, the output of the proposed tool is the corresponding auditing specifications that can be installed directly in the databases, to produce logs that are both minimal and sufficient to audit the given policies. The tool has been implemented and tested in a real-life scenario.