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.

翻译：我们结合克罗内克积与量化信息流，为复杂隐私流水线中的细粒度效用验证提出了一种新颖的形式化分析方法。该组合解释了一个关于隐私保护流水线效用行为的反常现象——即隐私的降低有时也会导致效用的下降。我们采用Ghosh等人提出的贝叶斯分析标准效用度量，通过可处理且严谨的证明揭示了导致这一反常现象的细粒度统计行为。更广泛而言，我们展望了能够补充现有隐私形式化分析的效用形式化分析工具。我们在一系列常见隐私保护设计方案上验证了所得结果。