-
Notifications
You must be signed in to change notification settings - Fork 1
/
bibliography.bib
216 lines (204 loc) · 21.3 KB
/
bibliography.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
@article{10.1145/2480359.2429113,
author = {Gaboardi, Marco and Haeberlen, Andreas and Hsu, Justin and Narayan, Arjun and Pierce, Benjamin C.},
title = {Linear Dependent Types for Differential Privacy},
year = {2013},
issue_date = {January 2013},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {48},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/2480359.2429113},
doi = {10.1145/2480359.2429113},
abstract = {Differential privacy offers a way to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Proving that a given query has this property involves establishing a bound on the query's sensitivity---how much its result can change when a single record is added or removed.A variety of tools have been developed for certifying that a given query differentially private. In one approach, Reed and Pierce [34] proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity and a probability monad to express randomized computation; it guarantees that any program with a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the sensitivity analysis depends on values that are not known statically.We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to certify a larger class of queries as differentially private, including ones whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantee follows directly from the soundness theorem of the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy for a broad class of iterative algorithms that could not be typed previously.},
journal = {SIGPLAN Not.},
month = jan,
pages = {357–370},
numpages = {14},
keywords = {linear logic, dependent types, type systems, differential privacy}
}
@inproceedings{10.1145/2429069.2429113,
author = {Gaboardi, Marco and Haeberlen, Andreas and Hsu, Justin and Narayan, Arjun and Pierce, Benjamin C.},
title = {Linear Dependent Types for Differential Privacy},
year = {2013},
isbn = {9781450318327},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2429069.2429113},
doi = {10.1145/2429069.2429113},
abstract = {Differential privacy offers a way to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Proving that a given query has this property involves establishing a bound on the query's sensitivity---how much its result can change when a single record is added or removed.A variety of tools have been developed for certifying that a given query differentially private. In one approach, Reed and Pierce [34] proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity and a probability monad to express randomized computation; it guarantees that any program with a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the sensitivity analysis depends on values that are not known statically.We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to certify a larger class of queries as differentially private, including ones whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantee follows directly from the soundness theorem of the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy for a broad class of iterative algorithms that could not be typed previously.},
booktitle = {Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {357–370},
numpages = {14},
keywords = {type systems, differential privacy, linear logic, dependent types},
location = {Rome, Italy},
series = {POPL '13}
}
@inproceedings{10.1145/1863543.1863568,
author = {Reed, Jason and Pierce, Benjamin C.},
title = {Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy},
year = {2010},
isbn = {9781605587943},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1863543.1863568},
doi = {10.1145/1863543.1863568},
abstract = {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 established definition of differential privacy falls out naturally as a special case of this soundness principle. We develop examples including known differentially private algorithms, privacy-aware variants of standard functional programming idioms, and compositionality principles for differential privacy.},
booktitle = {Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming},
pages = {157–168},
numpages = {12},
keywords = {type systems, differential privacy},
location = {Baltimore, Maryland, USA},
series = {ICFP '10}
}
@article{10.1145/1932681.1863568,
author = {Reed, Jason and Pierce, Benjamin C.},
title = {Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy},
year = {2010},
issue_date = {September 2010},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {45},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/1932681.1863568},
doi = {10.1145/1932681.1863568},
abstract = {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 established definition of differential privacy falls out naturally as a special case of this soundness principle. We develop examples including known differentially private algorithms, privacy-aware variants of standard functional programming idioms, and compositionality principles for differential privacy.},
journal = {SIGPLAN Not.},
month = sep,
pages = {157–168},
numpages = {12},
keywords = {type systems, differential privacy}
}
@inproceedings{10.1145/3009837.3009884,
author = {Zhang, Danfeng and Kifer, Daniel},
title = {LightDP: Towards Automating Differential Privacy Proofs},
year = {2017},
isbn = {9781450346603},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3009837.3009884},
doi = {10.1145/3009837.3009884},
abstract = { The growing popularity and adoption of differential privacy in academic and industrial settings has resulted in the development of increasingly sophisticated algorithms for releasing information while preserving privacy. Accompanying this phenomenon is the natural rise in the development and publication of incorrect algorithms, thus demonstrating the necessity of formal verification tools. However, existing formal methods for differential privacy face a dilemma: methods based on customized logics can verify sophisticated algorithms but come with a steep learning curve and significant annotation burden on the programmers, while existing programming platforms lack expressive power for some sophisticated algorithms. In this paper, we present LightDP, a simple imperative language that strikes a better balance between expressive power and usability. The core of LightDP is a novel relational type system that separates relational reasoning from privacy budget calculations. With dependent types, the type system is powerful enough to verify sophisticated algorithms where the composition theorem falls short. In addition, the inference engine of LightDP infers most of the proof details, and even searches for the proof with minimal privacy cost when multiple proofs exist. We show that LightDP verifies sophisticated algorithms with little manual effort. },
booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
pages = {888–901},
numpages = {14},
keywords = {dependent types, Differential privacy, type inference},
location = {Paris, France},
series = {POPL 2017}
}
@article{10.1145/3093333.3009884,
author = {Zhang, Danfeng and Kifer, Daniel},
title = {LightDP: Towards Automating Differential Privacy Proofs},
year = {2017},
issue_date = {January 2017},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {52},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/3093333.3009884},
doi = {10.1145/3093333.3009884},
abstract = { The growing popularity and adoption of differential privacy in academic and industrial settings has resulted in the development of increasingly sophisticated algorithms for releasing information while preserving privacy. Accompanying this phenomenon is the natural rise in the development and publication of incorrect algorithms, thus demonstrating the necessity of formal verification tools. However, existing formal methods for differential privacy face a dilemma: methods based on customized logics can verify sophisticated algorithms but come with a steep learning curve and significant annotation burden on the programmers, while existing programming platforms lack expressive power for some sophisticated algorithms. In this paper, we present LightDP, a simple imperative language that strikes a better balance between expressive power and usability. The core of LightDP is a novel relational type system that separates relational reasoning from privacy budget calculations. With dependent types, the type system is powerful enough to verify sophisticated algorithms where the composition theorem falls short. In addition, the inference engine of LightDP infers most of the proof details, and even searches for the proof with minimal privacy cost when multiple proofs exist. We show that LightDP verifies sophisticated algorithms with little manual effort. },
journal = {SIGPLAN Not.},
month = jan,
pages = {888–901},
numpages = {14},
keywords = {dependent types, type inference, Differential privacy}
}
@inproceedings{10.1145/3314221.3314619,
author = {Wang, Yuxin and Ding, Zeyu and Wang, Guanhong and Kifer, Daniel and Zhang, Danfeng},
title = {Proving Differential Privacy with Shadow Execution},
year = {2019},
isbn = {9781450367127},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3314221.3314619},
doi = {10.1145/3314221.3314619},
abstract = {Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness -- generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those two requires substantial changes to program logics: one recent paper is able to verify Report Noisy Max automatically, but it involves a complex verification system using customized program logics and verifiers. In this paper, we propose a new proof technique, called shadow execution, and embed it into a language called ShadowDP. ShadowDP uses shadow execution to generate proofs of differential privacy with very few programmer annotations and without relying on customized logics and verifiers. In addition to verifying Report Noisy Max, we show that it can verify a new variant of Sparse Vector that reports the gap between some noisy query answers and the noisy threshold. Moreover, ShadowDP reduces the complexity of verification: for all of the algorithms we have evaluated, type checking and verification in total takes at most 3 seconds, while prior work takes minutes on the same algorithms.},
booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation},
pages = {655–669},
numpages = {15},
keywords = {dependent types, Differential privacy},
location = {Phoenix, AZ, USA},
series = {PLDI 2019}
}
@inproceedings{10.1109/CSF.2014.36,
author = {Barthe, Gilles and Gaboardi, Marco and Arias, Emilio Jes\'{u}s Gallego and Hsu, Justin and Kunz, C\'{e}sar and Strub, Pierre-Yves},
title = {Proving Differential Privacy in Hoare Logic},
year = {2014},
isbn = {9781479942909},
publisher = {IEEE Computer Society},
address = {USA},
url = {https://doi.org/10.1109/CSF.2014.36},
doi = {10.1109/CSF.2014.36},
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.},
booktitle = {Proceedings of the 2014 IEEE 27th Computer Security Foundations Symposium},
pages = {411–424},
numpages = {14},
keywords = {probabilistic hoare logic, verification, hoare logic, privacy, relational hoare logic, differential privacy},
series = {CSF '14}
}
@article{10.1145/3341697,
author = {Zhang, Hengchu and Roth, Edo and Haeberlen, Andreas and Pierce, Benjamin C. and Roth, Aaron},
title = {Fuzzi: A Three-Level Logic for Differential Privacy},
year = {2019},
issue_date = {August 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {ICFP},
url = {https://doi.org/10.1145/3341697},
doi = {10.1145/3341697},
abstract = {Curators of sensitive datasets sometimes need to know whether queries against the data are differentially private. Two sorts of logics have been proposed for checking this property: (1) type systems and other static analyses, which fully automate straightforward reasoning with concepts like “program sensitivity” and “privacy loss,” and (2) full-blown program logics such as apRHL (an approximate, probabilistic, relational Hoare logic), which support more flexible reasoning about subtle privacy-preserving algorithmic techniques but offer only minimal automation. We propose a three-level logic for differential privacy in an imperative setting and present a prototype implementation called Fuzzi. Fuzzi’s lowest level is a general-purpose logic; its middle level is apRHL; and its top level is a novel sensitivity logic adapted from the linear-logic-inspired type system of Fuzz, a differentially private functional language. The key novelty is a high degree of integration between the sensitivity logic and the two lower-level logics: the judgments and proofs of the sensitivity logic can be easily translated into apRHL; conversely, privacy properties of key algorithmic building blocks can be proved manually in apRHL and the base logic, then packaged up as typing rules that can be applied by a checker for the sensitivity logic to automatically construct privacy proofs for composite programs of arbitrary size. We demonstrate Fuzzi’s utility by implementing four different private machine-learning algorithms and showing that Fuzzi’s checker is able to derive tight sensitivity bounds.},
journal = {Proc. ACM Program. Lang.},
month = jul,
articleno = {93},
numpages = {28},
keywords = {Differential privacy, apRHL, typechecking, Fuzz, static analysis, Fuzzi}
}
@article{10.1145/3360598,
author = {Near, Joseph P. and Darais, David and Abuah, Chike and Stevens, Tim and Gaddamadugu, Pranav and Wang, Lun and Somani, Neel and Zhang, Mu and Sharma, Nikhil and Shan, Alex and Song, Dawn},
title = {Duet: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy},
year = {2019},
issue_date = {October 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {OOPSLA},
url = {https://doi.org/10.1145/3360598},
doi = {10.1145/3360598},
abstract = {During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy. We propose Duet, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, Duet supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning - each of which are particularly challenging to encode in a statically verified differential privacy framework. We present a core design of the Duet language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend Duet to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in Duet which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of Duet's language design in terms of accuracy of trained machine learning models.},
journal = {Proc. ACM Program. Lang.},
month = oct,
articleno = {172},
numpages = {30},
keywords = {Differential privacy, machine learning, typechecking}
}
@article{selinger2009quantum,
title={Quantum lambda calculus},
author={Selinger, Peter and Valiron, Beno{\i}t and others},
journal={Semantic techniques in quantum computation},
pages={135--172}
}
@article{selinger2004towards,
title={Towards a quantum programming language},
author={Selinger, Peter},
journal={Mathematical Structures in Computer Science},
volume={14},
number={4},
pages={527--586},
year={2004},
publisher={Cambridge University Press New York, NY, USA}
}
@inproceedings{10.5555/1382436.1382751,
author = {Yao, Andrew C.},
title = {Protocols for Secure Computations},
year = {1982},
publisher = {IEEE Computer Society},
address = {USA},
booktitle = {Proceedings of the 23rd Annual Symposium on Foundations of Computer Science},
pages = {160–164},
numpages = {5},
series = {SFCS '82}
}