Proving differential privacy with shadow execution

Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, Danfeng Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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.

Original languageEnglish (US)
Title of host publicationPLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsKathryn S. McKinley, Kathleen Fisher
PublisherAssociation for Computing Machinery
Pages655-669
Number of pages15
ISBN (Electronic)9781450367127
DOIs
StatePublished - Jun 8 2019
Event40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 - Phoenix, United States
Duration: Jun 22 2019Jun 26 2019

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
CountryUnited States
CityPhoenix
Period6/22/196/26/19

Fingerprint

Formal verification

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Wang, Y., Ding, Z., Wang, G., Kifer, D., & Zhang, D. (2019). Proving differential privacy with shadow execution. In K. S. McKinley, & K. Fisher (Eds.), PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 655-669). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). Association for Computing Machinery. https://doi.org/10.1145/3314221.3314619
Wang, Yuxin ; Ding, Zeyu ; Wang, Guanhong ; Kifer, Daniel ; Zhang, Danfeng. / Proving differential privacy with shadow execution. PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. editor / Kathryn S. McKinley ; Kathleen Fisher. Association for Computing Machinery, 2019. pp. 655-669 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).
@inproceedings{99c2c602e8f749e09ce6695d58b50ab2,
title = "Proving differential privacy with shadow execution",
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.",
author = "Yuxin Wang and Zeyu Ding and Guanhong Wang and Daniel Kifer and Danfeng Zhang",
year = "2019",
month = "6",
day = "8",
doi = "10.1145/3314221.3314619",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "655--669",
editor = "McKinley, {Kathryn S.} and Kathleen Fisher",
booktitle = "PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation",

}

Wang, Y, Ding, Z, Wang, G, Kifer, D & Zhang, D 2019, Proving differential privacy with shadow execution. in KS McKinley & K Fisher (eds), PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Association for Computing Machinery, pp. 655-669, 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, United States, 6/22/19. https://doi.org/10.1145/3314221.3314619

Proving differential privacy with shadow execution. / Wang, Yuxin; Ding, Zeyu; Wang, Guanhong; Kifer, Daniel; Zhang, Danfeng.

PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ed. / Kathryn S. McKinley; Kathleen Fisher. Association for Computing Machinery, 2019. p. 655-669 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Proving differential privacy with shadow execution

AU - Wang, Yuxin

AU - Ding, Zeyu

AU - Wang, Guanhong

AU - Kifer, Daniel

AU - Zhang, Danfeng

PY - 2019/6/8

Y1 - 2019/6/8

N2 - 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.

AB - 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.

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

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

U2 - 10.1145/3314221.3314619

DO - 10.1145/3314221.3314619

M3 - Conference contribution

AN - SCOPUS:85067698752

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 655

EP - 669

BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

A2 - McKinley, Kathryn S.

A2 - Fisher, Kathleen

PB - Association for Computing Machinery

ER -

Wang Y, Ding Z, Wang G, Kifer D, Zhang D. Proving differential privacy with shadow execution. In McKinley KS, Fisher K, editors, PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery. 2019. p. 655-669. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/3314221.3314619