TY - GEN
T1 - CheckDP
T2 - 27th ACM SIGSAC Conference on Computer and Communications Security, CCS 2020
AU - Wang, Yuxin
AU - Ding, Zeyu
AU - Kifer, Daniel
AU - Zhang, Danfeng
N1 - Funding Information:
We thank the anonymous reviewers for their insightful feedbacks. This work was supported by NSF Awards CNS-1702760.
Publisher Copyright:
© 2020 ACM.
PY - 2020/10/30
Y1 - 2020/10/30
N2 - We propose CheckDP, an automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Furthermore, it was able to automatically generate proofs for correct mechanisms for which no formal verification was reported before. CheckDP is built on static program analysis, allowing it to be more efficient and precise in catching infrequent events than sampling based counterexample generators (which run mechanisms hundreds of thousands of times to estimate their output distribution). Moreover, its sound approach also allows automatic verification of correct mechanisms. When evaluated on standard benchmarks and newer privacy mechanisms, CheckDP generates proofs (for correct mechanisms) and counterexamples (for incorrect mechanisms) within 70 seconds without any false positives or false negatives.
AB - We propose CheckDP, an automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Furthermore, it was able to automatically generate proofs for correct mechanisms for which no formal verification was reported before. CheckDP is built on static program analysis, allowing it to be more efficient and precise in catching infrequent events than sampling based counterexample generators (which run mechanisms hundreds of thousands of times to estimate their output distribution). Moreover, its sound approach also allows automatic verification of correct mechanisms. When evaluated on standard benchmarks and newer privacy mechanisms, CheckDP generates proofs (for correct mechanisms) and counterexamples (for incorrect mechanisms) within 70 seconds without any false positives or false negatives.
UR - http://www.scopus.com/inward/record.url?scp=85096174065&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85096174065&partnerID=8YFLogxK
U2 - 10.1145/3372297.3417282
DO - 10.1145/3372297.3417282
M3 - Conference contribution
AN - SCOPUS:85096174065
T3 - Proceedings of the ACM Conference on Computer and Communications Security
SP - 919
EP - 938
BT - CCS 2020 - Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery
Y2 - 9 November 2020 through 13 November 2020
ER -