Proving that programs are differentially private

Annabelle McIver; Carroll Morgan

doi:10.1007/978-3-030-34175-6_1

Proving that programs are differentially private

Annabelle McIver^*, Carroll Morgan

^*Corresponding author for this work

Department of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution

Abstract

We extend recent work in Quantitative Information Flow (QIF) to provide tools for the analysis of programs that aim to implement differentially private mechanisms. We demonstrate how differential privacy can be expressed using loss functions, and how to use this idea in conjunction with a QIF-enabled program semantics to verify differentially private guarantees. Finally we describe how to use this approach experimentally using Kuifje, a recently developed tool for analysing information-flow properties of programs.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	17th Asian Symposium, APLAS 2019, Proceedings
Editors	Anthony Widjaja Lin
Place of Publication	Cham
Publisher	Springer, Springer Nature
Pages	3-18
Number of pages	16
ISBN (Electronic)	9783030341756
ISBN (Print)	9783030341749
DOIs	https://doi.org/10.1007/978-3-030-34175-6_1
Publication status	Published - 1 Jan 2019
Event	17th Asian Symposium on Programming Languages and Systems, APLAS 2019 - Bali, Indonesia Duration: 1 Dec 2019 → 4 Dec 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11893 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th Asian Symposium on Programming Languages and Systems, APLAS 2019
Country	Indonesia
City	Bali
Period	1/12/19 → 4/12/19

Keywords

Differential privacy
privacy
Probabilistic program semantics
Quantitative Information Flow
verification

Access to Document

10.1007/978-3-030-34175-6_1

Fingerprint Dive into the research topics of 'Proving that programs are differentially private'. Together they form a unique fingerprint.

Cite this

McIver, A., & Morgan, C. (2019). Proving that programs are differentially private. In A. W. Lin (Ed.), Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Proceedings (pp. 3-18). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11893 LNCS). Cham: Springer, Springer Nature. https://doi.org/10.1007/978-3-030-34175-6_1

McIver, Annabelle ; Morgan, Carroll. / Proving that programs are differentially private. Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Proceedings. editor / Anthony Widjaja Lin. Cham : Springer, Springer Nature, 2019. pp. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{a7cf7b5c5e9949798910ed0affd312d2,

title = "Proving that programs are differentially private",

abstract = "We extend recent work in Quantitative Information Flow (QIF) to provide tools for the analysis of programs that aim to implement differentially private mechanisms. We demonstrate how differential privacy can be expressed using loss functions, and how to use this idea in conjunction with a QIF-enabled program semantics to verify differentially private guarantees. Finally we describe how to use this approach experimentally using Kuifje, a recently developed tool for analysing information-flow properties of programs.",

keywords = "Differential privacy, privacy, Probabilistic program semantics, Quantitative Information Flow, verification",

author = "Annabelle McIver and Carroll Morgan",

year = "2019",

month = "1",

day = "1",

doi = "10.1007/978-3-030-34175-6_1",

language = "English",

isbn = "9783030341749",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Springer Nature",

pages = "3--18",

editor = "Lin, {Anthony Widjaja}",

booktitle = "Programming Languages and Systems",

address = "United States",

}

McIver, A & Morgan, C 2019, Proving that programs are differentially private. in AW Lin (ed.), Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11893 LNCS, Springer, Springer Nature, Cham, pp. 3-18, 17th Asian Symposium on Programming Languages and Systems, APLAS 2019, Bali, Indonesia, 1/12/19. https://doi.org/10.1007/978-3-030-34175-6_1

Proving that programs are differentially private. / McIver, Annabelle; Morgan, Carroll.

Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Proceedings. ed. / Anthony Widjaja Lin. Cham : Springer, Springer Nature, 2019. p. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11893 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution

TY - GEN

T1 - Proving that programs are differentially private

AU - McIver, Annabelle

AU - Morgan, Carroll

PY - 2019/1/1

Y1 - 2019/1/1

N2 - We extend recent work in Quantitative Information Flow (QIF) to provide tools for the analysis of programs that aim to implement differentially private mechanisms. We demonstrate how differential privacy can be expressed using loss functions, and how to use this idea in conjunction with a QIF-enabled program semantics to verify differentially private guarantees. Finally we describe how to use this approach experimentally using Kuifje, a recently developed tool for analysing information-flow properties of programs.

AB - We extend recent work in Quantitative Information Flow (QIF) to provide tools for the analysis of programs that aim to implement differentially private mechanisms. We demonstrate how differential privacy can be expressed using loss functions, and how to use this idea in conjunction with a QIF-enabled program semantics to verify differentially private guarantees. Finally we describe how to use this approach experimentally using Kuifje, a recently developed tool for analysing information-flow properties of programs.

KW - Differential privacy

KW - privacy

KW - Probabilistic program semantics

KW - Quantitative Information Flow

KW - verification

UR - http://www.scopus.com/inward/record.url?scp=85076692762&partnerID=8YFLogxK

UR - http://purl.org/au-research/grants/arc/DP140101119

U2 - 10.1007/978-3-030-34175-6_1

DO - 10.1007/978-3-030-34175-6_1

M3 - Conference proceeding contribution

SN - 9783030341749

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 18

BT - Programming Languages and Systems

A2 - Lin, Anthony Widjaja

PB - Springer, Springer Nature

CY - Cham

ER -

McIver A, Morgan C. Proving that programs are differentially private. In Lin AW, editor, Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Proceedings. Cham: Springer, Springer Nature. 2019. p. 3-18. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-34175-6_1