We combine Kronecker products, and quantitative information flow, to give a novel formal analysis for the fine-grained verification of utility in complex privacy pipelines. The combination explains a surprising anomaly in the behaviour of utility of privacy-preserving pipelines -- that sometimes a reduction in privacy results also in a decrease in utility. We use the standard measure of utility for Bayesian analysis, introduced by Ghosh at al., to produce tractable and rigorous proofs of the fine-grained statistical behaviour leading to the anomaly. More generally, we offer the prospect of formal-analysis tools for utility that complement extant formal analyses of privacy. We demonstrate our results on a number of common privacy-preserving designs.

翻译：我们结合Kronecker积与量化信息流，对复杂隐私管线中的效用细粒度验证提出了一种新颖的形式化分析方法。该组合解释了隐私保护管线中一个令人意外的效用行为异常——即隐私降低有时也会导致效用下降。我们采用Ghosh等人提出的贝叶斯分析标准效用度量，给出导致该异常现象的细粒度统计行为的可处理且严谨的证明。更一般地，我们提出了形式化效用分析工具的前景，以补充现有的隐私形式化分析方法。我们在一系列常见隐私保护设计中验证了所得结论。