A type-driven approach for sensitivity checking with branching

Sammanfattning: Differential Privacy (DP) is a promising approach to allow privacy preserving statistics over large datasets of sensitive data. It works by adding random noise to the result of the analytics. Understanding the sensitivity of a query is key to add the right amount of noise capable of protecting privacy of individuals in the dataset. The domain-specific language Spar[1] implements a programming language that uses the type system to automatically track the sensitivity of queries in Haskell. Queries can be constructed from basic operations in an EDSL. The operations’ impact on sensitivity need to be well-known and made explicit at type-level. Spar lacks branching operations. In general branching is a discontinuous operation, so the sensitivity of the whole branch might not be bounded. Due to this reason, most languages that track sensitivity do not provide branching as a basic operation. We introduce a modular and type-driven branching operation that checks for continuity at compile-time. It is implemented in Template Haskell and thus operates on the syntax of the condition and bodies of the branches. To demonstrate our approach, we provide basic examples common in literature. Additionally, we also provide the implementation of more sophisticated operations such as Mergesort. We develop requirements under which the use of our branching operator is sound.