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 条
  • [1] Alvim M., 2014, POST, P120
  • [2] Alvim M.S., 2010, ABS10124250 CORR
  • [3] On the information leakage of differentially-private mechanisms
    Alvim, Mario S.
    Andres, Miguel E.
    Chatzikokolakis, Konstantinos
    Degano, Pierpaolo
    Palamidessi, Catuscia
    [J]. JOURNAL OF COMPUTER SECURITY, 2015, 23 (04) : 427 - 469
  • [4] Additive and multiplicative notions of leakage, and their capacities
    Alvim, Mario S.
    Chatzikokolakis, Konstantinos
    McIver, Annabelle
    Morgan, Carroll
    Palamidessi, Catuscia
    Smith, Geoffrey
    [J]. 2014 IEEE 27TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2014, : 308 - 322
  • [5] Measuring Information Leakage using Generalized Gain Functions
    Alvim, Mario S.
    Chatzikokolakis, Kostas
    Palamidessi, Catuscia
    Smith, Geoffrey
    [J]. 2012 IEEE 25TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2012, : 265 - 279
  • [6] Alvim MS, 2011, LECT NOTES COMPUT SC, V6756, P60, DOI 10.1007/978-3-642-22012-8_4
  • [7] [Anonymous], 2017, JPC
  • [8] Barthe G., 2016, ACM SIGLOG News, V3, P34
  • [9] Proving Differential Privacy via Probabilistic Couplings
    Barthe, Gilles
    Gaboardi, Marco
    Gregoire, Benjamin
    Hsu, Justin
    Strub, Pierre-Yves
    [J]. PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016), 2016, : 749 - 758
  • [10] Proving differential privacy in Hoare logic
    Barthe, Gilles
    Gaboardi, Marco
    Arias, Emilio Jesus Gallego
    Hsu, Justin
    Kunz, Cesar
    Strub, Pierre-Yves
    [J]. 2014 IEEE 27TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2014, : 411 - 424
123