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

By Jason Reed, Benjamin C. Pierce. 2010

281 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, Statistical Learning Theory, Privacy & Security

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Statistical Learning Theory

In Privacy & Security

Citations in the corpus

Detecting Violations of Differential Privacy (2018, background): “On the other hand, static methods exist for verifying that a program obeys differential privacy during any execution, based on relational program logic [1–7] and relational type system [24, 35, 41].”
Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “…dynamic checking [24, 36], relational program logic [2, 6] and relational reﬁnement type systems [9], linear (dependent) type systems [29, 42], product programs [7], meth-ods based on computing bisimulations families for probabilistic automata [50, 51], and methods based on counting…”
Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “…including dynamic checking [17, 26], the already mentioned relational program logic [2, 4] and relational re-ﬁnement type systems [8], linear (dependent) type systems [18, 29], product programs [5], and methods based on computing bisimu-lations families for probabilistic automata [31, 32].”
Proving Differential Privacy in Hoare Logic (2014, methodology): “Fuzz [33] and DFuzz [25] use a type-based approach for inferring and checking the sensitivity of functional programs.”
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (2013, methodology): “Moreover, several language-based methods have been developed for guaranteeing differential privacy; these methods are based on runtime verification, such as PINQ [21] or Airavat [28], type systems [26, 18], or deductive verification [10].”
Relational Symbolic Execution (2017, background): “We already mentioned different works that reduce the verification of relational properties to the one of properties through self-composition Barthe et al. [2004], Terauchi and Aiken [2005] and product programs Butler and Schulte [2011], Asada et al. [2017], Eilers et al. [2018]. Several works have s”
Optimal Geo-Indistinguishable Mechanisms for Location Privacy (2014, background): “This concept can be naturally extended to any set of secrets X , equipped with a metric dX [15, 12].”
Metrics for Differential Privacy in Concurrent Systems (2014, methodology): “Among the approaches based on formal methods, we mention those based on type-systems [24,16] and logical formulations [3].”
Distributed Differential Privacy and Applications (2015, methodology): “VerDP’s query language is based on the Fuzz language for differentially private data analysis (Reed and Pierce, 2010; Haeberlen et al., 2011; Gaboardi et al., 2013) because: 1) it is sufficiently expressive to implement a number of practical differentially-private queries, and 2) it uses static anal”
AutoPriv: Automating Differential Privacy Proofs (2016, methodology): “Except the very recent work by Barthe et al. (2016), all existing formal methods (e.g., (Reed and Pierce 2010; Gaboardi et al. 2013; Barthe et al. 2012, 2014)) solely rely on the composition theorem, hence fail to prove that the Sparse Vector method satisfies ǫ ′ privacy for any ǫ ′ .”
Local Differential Private Data Aggregation for Discrete Distribution Estimation (2019, methodology): “As a metric generalization of the original -LDP in [23] for capturing intrinsic structures of values in general discrete data, the -LDP in Definition 1 of this work is also known as -geoindistinguishability [17], dX -privacy [18] or data obfuscation [18], [19], [22], [25].”
Property Testing For Differential Privacy (2018, methodology): “There is a line of work (Barthe et al., 2014, Roy et al., 2010, Reed and Pierce, 2010, Gaboardi et al., 2013, Tschantz et al., 2011, Barthe et al., 2012, 2013, McSherry, 2009) using logical arguments (type systems, I/O automata, Hoare logic, etc.) to verify privacy.”
Probabilistic relational reasoning for differential privacy (2012, background): “The linear type system of [29] extends sensitivity analysis to a higher-order functional language.”
LightDP: towards automating differential privacy proofs (2016, methodology): “…enabling the verification of sophisticated algorithms (e.g., the Sparse Vector method) that are beyond the capability of many existing methods (Reed and Pierce 2010; Gaboardi et al. 2013; Barthe et al. 2012, 2014) based on the composition thePermission to make digital or hard copies of all or…”
Testing the Lipschitz Property over Product Distributions with Applications to Data Privacy (2013, background): “One approach (e.g. [25,30,29]) that has been taken to address the above problem is to require clients to write their programs using a speciﬁc set of trusted built-in functions provided by the platform.”