A Language for the Composition of Privacy-Enforcement Techniques

Today´s large-scale computations, for instance, in the cloud, are subject to a multitude of risks concerning the divulging and ownership of private data. Privacy risks are mainly addressed using encryption-based techniques. These make data private, but costly to operate. Furthermore, today´s computations have to ensure privacy properties in the context of complex software compositions, however, no general support for the declarative definition and implementation of privacy-preserving applications has been put forward. This article presents an approach to the correct composition of privacy-preserving applications in the cloud. Our approach provides language support for the composition of encryption-and fragmentation-based privacy-preserving algorithms. This language comes with a set of laws that allows us to verify privacy properties. Finally, we introduce implementation support in Scala that ensures privacy properties by construction using advanced features of Scala´s type system.