During the past decade, differential privacy has become the gold standard for
protecting the privacy of individuals. However, verifying that a particular
program provides differential privacy often remains a manual task to be
completed by an expert in the field. Language-based techniques have been
proposed for fully automating proofs of differential privacy via type system
design, however these results have lagged behind advances in
differentially-private algorithms, leaving a noticeable gap in programs which
can be automatically verified while also providing state-of-the-art bounds on
privacy.
We propose Duet, an expressive higher-order language, linear type system and
tool for automatically verifying differential privacy of general-purpose
higher-order programs. In addition to general purpose programming, Duet
supports encoding machine learning algorithms such as stochastic gradient
descent, as well as common auxiliary data analysis tasks such as clipping,
normalization and hyperparameter tuning - each of which are particularly
challenging to encode in a statically verified differential privacy framework.
We present a core design of the Duet language and linear type system, and
complete key proofs about privacy for well-typed programs. We then show how to
extend Duet to support realistic machine learning applications and recent
variants of differential privacy which result in improved accuracy for many
practical differentially private algorithms. Finally, we implement several
differentially private machine learning algorithms in Duet which have never
before been automatically verified by a language-based tool, and we present
experimental results which demonstrate the benefits of Duet's language design
in terms of accuracy of trained machine learning models.