Abstract
Data Integration Systems (DIS) are concerned with integrating data from multiple data sources to resolve user queries. Typically, organisations providing data sources specify security policies that impose stringent requirements on the collection, processing, and disclosure of personal and sensitive data. If the security policies were not correctly enforced by the integration component of DIS, the data is exposed to data leakage threats, e.g. unauthorised disclosure or secondary use of the data. SecureDIS is a framework that helps system designers to mitigate data leakage threats during the early phases of DIS development. SecureDIS provides designers with a set of informal guidelines written in natural language to specify and enforce security policies that capture confidentiality, privacy, and trust properties. In this paper, we apply a formal approach to model a DIS with the SecureDIS security policies and verify the correctness and consistency of the model. The model can be used as a basis to perform security policies analysis or automatically generate a Java code to enforce those policies within DIS.