Coq deep specification of security aware data integration – DataCert

Integrating and exchanging data from multiple sources has been a long-standing challenge in the database community. This problem is crucial in numerous contexts, including data integration for enterprises and organizations, data sharing on the Internet, collaboration among government agencies, and the exchange of scientific data. Today, data integration and exchange usually starts by collecting the data from disparate sources, then further abstracting the data into repositories providing a single entry point, while carefully removing or manually protecting security-sensitive information. This process is extremely time consuming and labor intensive as well as error-prone.

Data integration and exchange is seriously hampered by an inability to efficiently ensure security and privacy as well as by the unprecedented scale at which data is produced and consumed. On the one hand, without a relevant security framework, sources are reluctant to share their data. Problems include both the fear of disclosing confidential information as well as the enforcement of regulations protecting individual privacy. On the other hand, the variety and the volume of the data need automatic methods that ease the integration and exchange processes. This observations calls for a strong attention to the foundational study of security principles in the context of data integration and exchange. Both security concerns and scale are major barriers that impede these efforts.

Security is addressed today by preventing dissemination rather than implementing security policies as key parts of the data integration and sharing process itself. Security concerns should be considered in the very design phase and not approximately recovered after it. Moreover, the mechanisms that enforce security policies should be ultimately trusted with the highest possible assurance levels. This requirement is particularly significant in the presence of high-value data assets. This project will develop the techniques needed to integrate and exchange data while controlling the effectiveness of trusted data integration and exchange algorithms in presence of security and privacy policies.

Our aim is to develop a comprehensive framework handling the fundamental problems underlying security aware data integration and sharing, resulting in a paradigm shift in the design and implementation of security aware data integration systems. To fill the gap between both worlds, we will strongly rely on deep specifications and proven correct software, develop formal models yielding highly reliable technology while controlling the disclosure of private or confidential information. This research will proceed along several interrelated issues to make the following advances:

- Deep specification of state-of-the-art algorithms for data integration and exchange. The most significant algorithms will be considered and formalized using the Coq interactive theorem prover. The key objective is to obtain formally designed and verified software through automatic code extraction from formal proofs.

- Design of robust techniques to capture and enforce security policies in the data integration process. We will leverage existing access control techniques to a new distributed setting of large scale. In general, establishing that a system is secure can be very hard. We will investigate techniques, study and establish properties that are sufficient to guarantee that a data integration technique is secure with regards to a set of security policies.

- Design of innovative data integration methods for loosely constrained data with particular attention to record-linkage techniques and RDF data: the cornerstone of Linked-Open-Data and the semantic web. Formal methods will by used afresh to obtain the strongest guarantees on software.

The outcome will have wider merit as well, by pioneering a new secured data integration paradigm relying on the ability to share data in a formally verified framework.