Proving Differential Privacy in Hoare Logic

Citations Over TimeTop 10% of 2014 papers

Abstract

Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output distributions of a probabilistic program on adjacent inputs. Like many 2-safety properties, differential privacy lies outside the scope of traditional verification techniques. Existing approaches to enforce privacy are based on intricate, non-conventional type systems, or customized relational logics. These approaches are difficult to implement and often cumbersome to use. We present an alternative approach that verifies differential privacy by standard, non-relational reasoning on non-probabilistic programs. Our approach transforms a probabilistic program into a non-probabilistic program which simulates two executions of the original program. We prove that if the target program is correct with respect to a Hoare specification, then the original probabilistic program is differentially private. We provide a variety of examples from the differential privacy literature to demonstrate the utility of our approach. Finally, we compare our approach with existing verification techniques for privacy.

Related Papers

• → Don’t Know in Probabilistic Systems(2006)98 cited
• → Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm(2007)53 cited
• Almost always and sometime definitely are not enough: Probabilistic quanifiers and probabilistic model-checking(1996)
• → Repairing errors in probabilistic databases models using probabilistic abduction reasoning(2017)
• → Repairing errors in probabilistic databases models using probabilistic abduction reasoning(2017)