Distance makes the types grow stronger: a calculus for differential privacy

We want assurances that sensitive information will not be disclosed when aggregate data derived from a database is published. Differential privacy offers a strong statistical guarantee that the effect of the presence of any individual in a database will be negligible, even when an adversary has auxiliary knowledge. Much of the prior work in this area consists of proving algorithms to be differentially private one at a time; we propose to streamline this process with a functional language whose type system automatically guarantees differential privacy, allowing the programmer to write complex privacy-safe query programs in a flexible and compositional way. The key novelty is the way our type system captures function sensitivity, a measure of how much a function can magnify the distance between similar inputs: well-typed programs not only can't go wrong, they can't go too far on nearby inputs. Moreover, by introducing a monad for random computations, we can show that the estab...

• Type: Conference
• Year: 2010
• Where: ICFP
• Authors: Jason Reed, Benjamin C. Pierce
• Keywords: Captures Function Sensitivity, Complex Privacy-safe Query, ICFP 2010, Programming Languages, Strong Statistical Guarantee