Linear dependent types for differential privacy

By Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, Benjamin C. Pierce. 2013

211 citations recorded by the source corpus.

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

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): “…approaches: 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): “2015c), linear (dependent) type systems (Reed and Pierce 2010; Gaboardi et al. 2013), product programs (Barthe et al.”
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.”
LightDP: towards automating differential privacy proofs (2016, methodology): “Except the very recent work by Barthe et al. (2016c,b), existing formal methods (e.g., (Reed and Pierce 2010; Gaboardi et al. 2013; Barthe et al. 2012, 2014)) rely on the composition theorem, hence fail to prove that the Sparse Vector method satisfies ′-privacy for any ′.”
Differential Privacy by Typing in Security Protocols (2013, background): “[4] extended this type system to allow the certification of a larger class of queries whose sensitivity might depend on runtime information.”
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].”
DStress: Efficient Differentially Private Computations on Distributed Data (2017, methodology): “, using linear type systems [31, 38] or a system like CertiPriv [4].”
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 ǫ ′ .”
Towards Practical Differential Privacy for SQL Queries (2017, background): “Fuzz [28, 29] enforces differential privacy for functional programs, but does not support one-to-many or many-tomany joins.”
Practical Differential Privacy for SQL Queries Using Elastic Sensitivity (2017, background): “Fuzz [20,21] enforces differential privacy for functional programs, but does not support one-to-many or many-to-many joins.”
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].”
Verified Computational Differential Privacy with Applications to Smart Metering (2013, background): “These include extending the protocols and proofs of Sections II and IV to the malicious model, and enhancing EasyCrypt with support for reasoning about continuous probability distributions and real-world implementations based on floating-point arithmetic.”
Differential Privacy (2015, background): “Another line of work developing the Fuzz and DFuzz prototypes [10, 12, 23] describes non-interactive differential privacy in which the whole computation over private data is described by a domain-specific functional program, and a sensitivity-based static type system determines statically whether th”
Pain-Free Random Differential Privacy with Sensitivity Sampling (2017, background): “Limited to a similar level of program expressiveness as PINQ, Fuzz cannot typecheck many desirable target programs and speciﬁcally cannot track data-dependent function sensitivity, with the DFuzz system demonstrating preliminary work towards this challenge (Gaboardi et al., 2013).”
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”
Verifiable differential privacy (2015, methodology): “VerDP’s query language is based on the Fuzz language for differentially private data analysis [18, 21, 39] because: 1) it is sufficiently expressive to implement a number of practical differentially-private queries, and 2) it uses static analysis to certify privacy properties without running the que”
Property Testing For Differential Privacy (2018, methodology): “Several algorithms and tools have been proposed for formal verification of the DP guarantee of an algorithm (6, 27, 26, 20, 29, 6, 27, 26, 20, 29, 7, 5, 23).”