Privacy Specifications that do not Compose: Empirical and Formal Auditing of Sequentially Published Energy Data

Résumé technique : Spécifications de confidentialité qui ne se composent pas

Énoncé du problème
Les éditeurs de données énergétiques publient régulièrement des statistiques sur la consommation d'électricité, les registres d'installations et les journaux de recharge, souvent accompagnées d'une promesse selon laquelle les individus ou les petits groupes ne peuvent être identifiés. Ces promesses sont généralement vérifiées de manière « ponctuelle », en examinant chaque publication isolément par rapport à une règle de confidentialité définie (par exemple, l'anonymat $k$ avec $k \ge 5$). Cependant, les éditeurs publient ces ensembles de données de manière séquentielle sur plusieurs années. L'article soutient qu'une publication apparaissant sûre de manière isolée peut révéler nettement plus d'informations lorsqu'elle est cumulée avec des publications précédentes ou suivantes. Plus précisément, l'article identifie que les spécifications de confidentialité à publication unique échouent souvent à se composer dans le temps, menant à des « attaques par différence » où la soustraction de publications consécutives expose des groupes marginaux (par exemple, un changement de 1 à 4 mètres dans un quartier) qui étaient individuellement supprimés.

Méthodologie
Les auteurs proposent un pipeline d'audit à deux volets pour évaluer les publications de données énergétiques publiques, tant de manière empirique que formelle.

1. Mesure empirique : L'audit mesure la posture de ré-identification des fichiers publiés en utilisant des métriques de contrôle de la divulgation établies ($k$-anonymat, $\ell$-diversité, $t$-proximité) via une implémentation Python personnalisée (pyARX-equiv) validée par rapport à la bibliothèque de référence ARX. Il emploie également des jeux adverses (isolement, lien, inférence) en utilisant le cadre Anonymeter et un profileur spécifique au domaine (PENM) comme contrôles secondaires.
2. Vérification formelle : La politique de transformation déclarée par l'éditeur est encodée sous forme de contraintes logiques au format SMT-LIB. Un portefeuille de solveurs automatisés (Z3 et Yices2) vérifie si la politique encodée entraîne logiquement la garantie de confidentialité revendiquée. Si la politique n'entraîne pas la garantie, le solveur produit un noyau UNSAT étiqueté.
3. Localisation des écarts : Lorsqu'une divergence est détectée entre la posture empirique et la revendication énoncée, le noyau UNSAT étiqueté est associé à l'une des cinq familles d'échec : Quasi-identifiant manquant, Composition de fenêtre de publication non sûre, Erreur d'ordre des opérations, Liaison inter-publications, ou Omission de documentation.
4. Diagnostics longitudinaux : Pour les publications séquentielles, l'audit introduit deux diagnostics : la « demi-vie de la spécification » (le nombre de publications après lesquelles une règle de fenêtre unique ne décrit plus plus de la moitié de la série) et le « budget de validité de la spécification » ($W^*$), qui quantifie le nombre de publications pendant lesquelles une règle de fenêtre unique reste descriptive avant de décliner.

Contributions clés

• Cadre d'audit à deux volets : Une méthodologie novatrice qui combine la mesure empirique des données avec la vérification formelle de la politique déclarée par l'éditeur, permettant d'identifier les hypothèses manquantes plutôt que de simplement mesurer le risque.
• Réfutation formelle des spécifications : L'article démontre que les solveurs formels peuvent infirmer une règle de confidentialité elle-même. En traitant les comptes de données comme des variables inconnues, les auteurs montrent que la politique documentée (par exemple, $k \ge 5$ par fenêtre) permet intrinsèquement des paires de publications non sûres, indépendamment des valeurs de données spécifiques.
• Artefact de reproductibilité : Les auteurs publient le code d'audit, les politiques encodées, les revendications verbatim des éditeurs et les modèles de divulgation, couvrant un corpus de onze publications comprenant quatre types de données énergétiques (traces de ménages, recharge de VE, registres d'actifs et transparence du système).

Résultats
L'audit a été appliqué à onze ensembles de données énergétiques publiques (plus une série d'utilités américaine pour comparaison).

• Échec de composition (BEIS) : Dans les statistiques d'électricité infranationale du Royaume-Uni (BEIS/DESNZ), la règle $k \ge 5$ est respectée pour les publications annuelles individuelles. Cependant, la différence entre les publications révèle que 93 % des zones subissent une transition de 1 à 4 mètres entre les années, exposant un groupe de moins de cinq mètres. La « demi-vie de la spécification » pour cette série est de trois publications annuelles ; après ce point, la règle de fenêtre unique ne décrit plus la série.
• Dépendance à la volatilité : Une comparaison avec la série d'utilités US EIA-861 montre que le risque de composition n'est pas uniforme. La série américaine, caractérisée par des totaux d'utilités plus stables, décline beaucoup plus lentement (ne dépassant jamais le seuil de demi-vie à travers 11 publications) par rapport aux données volatiles des ménages britanniques.
• Unicité structurelle vs opérationnelle : Bien que presque toutes les publications présentent une unicité structurelle ($k=1$ sur les quasi-identifiants publiés), le risque de ré-identification opérationnelle estimé (probabilité d'identifier une personne réelle) est effectivement nul pour neuf des dix publications de personnes physiques, à l'exception de la publication de recharge de VE ACN-Data.
• Divergences spécifiques :
  • BEIS : Divergence due à une « Composition de fenêtre de publication non sûre ».
  • MaStR (Registre allemand des installations) : Divergence due à un « Quasi-identifiant manquant » (le tuple publié permet des installations uniques).
  • GoiEner : Divergence due à une « Erreur d'ordre des opérations » (suppression appliquée après le hachage).
  • OCPP-EV : Omission de documentation concernant les définitions d'adversaires.
• Liaison auxiliaire : Le rapprochement du registre MaStR avec la propre table d'unités du régulateur rend 24 % des installations identifiables de manière unique, soulignant que les propres registres auxiliaires de l'éditeur sont le principal vecteur d'amplification.

Signification et Revendications
L'article soutient que le mode de défaillance dominant dans la confidentialité des données énergétiques n'est pas l'unicité d'une publication unique, mais l'échec des protections à se composer à travers une séquence de publications. Les auteurs affirment que :

1. Les audits de publication unique sont insuffisants : Ils ne peuvent pas détecter la menace de « différence » inhérente aux régimes de republication périodique imposés par des réglementations telles que la plateforme de transparence de l'ENTSO-E ou les méthodologies du DESNZ.
2. La vérification formelle apporte une valeur ajoutée : Elle va au-delà de la mesure du risque pour identifier l'écart logique spécifique dans la politique de l'éditeur (par exemple, l'absence d'un opérateur de budget de fenêtre croisée).
3. Remédiation actionnable : Les auteurs proposent un « budget de validité de la spécification » ($W^*$) comme un contrôle d'audit pratique. Les éditeurs devraient déclarer les clés s'étendant sur les republications, mesurer l'érosion de la composition avant chaque publication, et publier un budget de validité pour indiquer combien de temps leur règle de fenêtre unique reste descriptive.

L'article précise explicitement qu'il ne prétend pas avoir ré-identifié des individus spécifiques dans les données agrégées du BEIS, mais plutôt que l'existence et la taille de petits groupes marginaux peuvent être inférées, ce qui constitue un échec de contrôle de la divulgation par rapport à la logique déclarée de l'éditeur. Le travail est positionné comme un audit de données publiques existantes, et non comme une proposition de nouveaux mécanismes de confidentialité différentielle, bien qu'il note que les protections héritées « se dégradent mal sous la composition », à l'instar des conclusions concernant la refonte du recensement américain de 2020.