  Curators of sensitive datasets sometimes need to know whether queries against
the data are differentially private [Dwork et al. 2006]. Two sorts of logics
have been proposed for checking this property: (1) type systems and other
static analyses, which fully automate straightforward reasoning with concepts
like "program sensitivity" and "privacy loss," and (2) full-blown program
logics such as apRHL (an approximate, probabilistic, relational Hoare logic)
[Barthe et al. 2016], which support more flexible reasoning about subtle
privacy-preserving algorithmic techniques but offer only minimal automation.
  We propose a three-level logic for differential privacy in an imperative
setting and present a prototype implementation called Fuzzi. Fuzzi's lowest
level is a general-purpose logic; its middle level is apRHL; and its top level
is a novel sensitivity logic adapted from the linear-logic-inspired type system
of Fuzz, a differentially private functional language [Reed and Pierce 2010].
The key novelty is a high degree of integration between the sensitivity logic
and the two lower-level logics: the judgments and proofs of the sensitivity
logic can be easily translated into apRHL; conversely, privacy properties of
key algorithmic building blocks can be proved manually in apRHL and the base
logic, then packaged up as typing rules that can be applied by a checker for
the sensitivity logic to automatically construct privacy proofs for composite
programs of arbitrary size.
  We demonstrate Fuzzi's utility by implementing four different private
machine-learning algorithms and showing that Fuzzi's checker is able to derive
tight sensitivity bounds.
