Proving that Programs Are Differentially Private

被引：2

作者：

McIver, Annabelle ^{[1
]}

Morgan, Carroll ^{[2
,3
]}

机构：

[1] Macquarie Univ, Dept Comp, Sydney, NSW, Australia

[2] Univ New South Wales, Sydney, NSW, Australia

[3] Data61, Sydney, NSW, Australia

来源：

PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2019 | 2019年 / 11893卷

基金：

澳大利亚研究理事会;

关键词：

Quantitative Information Flow; Probabilistic program semantics; verification; privacy; Differential privacy;

D O I：

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

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：3 / 18

页数：16

共 22 条

[11]

Bognar M., KUIFJE PROTOTYPE QUA

[12]

Chatzikokolakis Konstantinos, 2013, Privacy Enhancing Technologies.13th International Symposium, PETS 2013. Proceedings: LNCS 7981, P82, DOI 10.1007/978-3-642-39077-7_5

[13]

Dwork C, 2006, LECT NOTES COMPUT SC, V4052, P1

[14] A Categorical Approach to Probability Theory [J].

Fric, Roman ;

Papco, Martin .

STUDIA LOGICA, 2010, 94 (02) :215-230

[15]

Gibbons C.M.J., 2019, FDN PROBABILISTIC PR

[16]

McIver A., 2015, P LICS 2015

[17]

McIver A, 2010, LECT NOTES COMPUT SC, V6199, P223, DOI 10.1007/978-3-642-14162-1_19

[18] A MATHEMATICAL THEORY OF COMMUNICATION [J].

SHANNON, CE .

BELL SYSTEM TECHNICAL JOURNAL, 1948, 27 (04) :623-656

[19]

Smith G, 2009, LECT NOTES COMPUT SC, V5504, P288

[20] Proving Differential Privacy with Shadow Execution [J].

Wang, Yuxin ;

Ding, Zeyu ;

Wang, Guanhong ;

Kifer, Daniel ;

Zhang, Danfeng .

PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, :655-669

← 1 2 3 →