# Proving Differential Privacy with Shadow Execution

## TL;DR

This paper introduces shadow execution within ShadowDP, a new proof technique that simplifies and speeds up the formal verification of differential privacy for complex algorithms with minimal annotations.

## Contribution

It presents shadow execution as a novel verification method embedded in ShadowDP, enabling efficient and less annotation-intensive proofs of differential privacy.

## Key findings

- Verifies Report Noisy Max automatically
- Verifies a new Sparse Vector variant
- Verification time reduced to seconds

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