This is a summary of the group meeting on 23 December 2020

Depeng: Deciding Accuracy of Differential Privacy Schemes, GILLES BARTHE, ROHIT CHADHA, PAUL KROGMEIER, A. PRASAD SISTLA, MAHESH VISWANATHAN (POPL ’21)

Contributions includes:

• Establishes a general definition of accuracy, which subsumes the definition used in theoretical computer science and captures known accuracy claims for dp algorithms in the literature:

Three parameters to describe bounds on inputs, outputs and probabilities:

Def2

A differential privacy algorithm ? is accurate w.r.t det(?) if on all inputs ? that have a large distance disagreement, ?’s output on ? is close to det(?) with high probability.

• Studies the verification problem under the definition for accuracy: generally undecidable:

similar to the proof in (LICS ’20).

• Defines a fragment of programs: DiPWhile+, whose operational semantics is an encoding of finite-state discrete-time Markov chains(DTMCs), describing common dp algorithms in the literature:

DiPWhile+ is an extension of DiPWhile (LICS ’20), but allows real variables evaluation rather than only domain variables;

States in DTMC represent the evaluations for variables of execution of each statement.

• Studies the decidability/conditional decidability results for checking accuracy in DiPWhile+:

More theoretic decidability results given conditions of whether Shanuel’s conjecture is used, inputs and outputs of finite or infinite domain;

Decides the theories of parameters under decidability results:

Table1

Experiment evaluations on accuracy bounds for dp algorithms under decidable fragments, including NoisyMax, SVT, etc.

Table2

Song: A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, Benjamin Kaminski and J-P Katoen (LICS 2017)

link to download this paper

A sound weakest pre-expectation calculus is proposed for reasoning about mixed–sign unbounded expectations.

1. A new notion of mixed–sign expectations is presented called integrability–witnessing expectations, which incorporate bookkeeping for the integrability of the expectations.
   • define mixed-sign expectations
   • define integrability-witness pairs
   • define quasi-order on integrability-witness pairs, equivalence classes and partial order
   • define integrability-witnessing expectations (IE)
2. Based on the integrability–witnessing expectations in 1, the weakest pre-expectation calculus is presented.
   • define ~wp~transformer (on IE)
   • discuss the limit of sequence in IE and the uniqueness of the limit
   • prove the calculus for while-loop is well-defined
3. It is shown that the calculus is sound and allows for monotonic reasoning.
4. An invariant rule is presented for reasoning about loops and some examples are provided to show its applicability