Skip to main content

Proving differential privacy with shadow execution

Publication ,  Conference
Wang, Y; Ding, Z; Wang, G; Kifer, D; Zhang, D
Published in: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
June 8, 2019

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.

Duke Scholars

Altmetric Attention Stats
Dimensions Citation Stats

Published In

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

DOI

Publication Date

June 8, 2019

Start / End Page

655 / 669
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Wang, Y., Ding, Z., Wang, G., Kifer, D., & Zhang, D. (2019). Proving differential privacy with shadow execution. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (pp. 655–669). https://doi.org/10.1145/3314221.3314619
Wang, Y., Z. Ding, G. Wang, D. Kifer, and D. Zhang. “Proving differential privacy with shadow execution.” In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 655–69, 2019. https://doi.org/10.1145/3314221.3314619.
Wang Y, Ding Z, Wang G, Kifer D, Zhang D. Proving differential privacy with shadow execution. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2019. p. 655–69.
Wang, Y., et al. “Proving differential privacy with shadow execution.” Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019, pp. 655–69. Scopus, doi:10.1145/3314221.3314619.
Wang Y, Ding Z, Wang G, Kifer D, Zhang D. Proving differential privacy with shadow execution. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2019. p. 655–669.

Published In

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

DOI

Publication Date

June 8, 2019

Start / End Page

655 / 669