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.