Abstract
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. [1], 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.
Original language | English |
---|---|
Title of host publication | CCS '23 |
Subtitle of host publication | proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security |
Place of Publication | New York |
Publisher | Association for Computing Machinery |
Pages | 1718-1731 |
Number of pages | 14 |
ISBN (Electronic) | 9798400700507 |
DOIs | |
Publication status | Published - 2023 |
Event | 30th ACM SIGSAC Conference on Computer and Communications Security - Copenhagen, Denmark Duration: 26 Nov 2023 → 30 Nov 2023 Conference number: 30th |
Conference
Conference | 30th ACM SIGSAC Conference on Computer and Communications Security |
---|---|
Abbreviated title | ACM CCS 2023 |
Country/Territory | Denmark |
City | Copenhagen |
Period | 26/11/23 → 30/11/23 |
Keywords
- Formal verification for utility
- privacy-utility trade-off