Solo: A Lightweight Static Analysis for Differential Privacy

TL;DR

This paper introduces Solo, a lightweight static analysis method that enforces differential privacy without relying on complex type systems, making it easier to embed in mainstream languages like Haskell, Scala, and OCaml.

Contribution

The paper presents a new type system for differential privacy that avoids complex types and can be integrated into popular programming languages.

Findings

Successfully embedded in Haskell and demonstrated on case studies

Proved soundness of the type-based enforcement

Achieved lightweight static analysis for differential privacy

Abstract

All current approaches for statically enforcing differential privacy in higher order languages make use of either linear or relational refinement types. A barrier to adoption for these approaches is the lack of support for expressing these "fancy types" in mainstream programming languages. For example, no mainstream language supports relational refinement types, and although Rust and modern versions of Haskell both employ some linear typing techniques, they are inadequate for embedding enforcement of differential privacy, which requires "full" linear types a la Girard. We propose a new type system that enforces differential privacy, avoids the use of linear and relational refinement types, and can be easily embedded in mainstream richly typed programming languages such as Scala, OCaml and Haskell. We demonstrate such an embedding in Haskell, demonstrate its expressiveness on case studies, and prove that our type-based enforcement of differential privacy is sound.