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

Sintesi Tecnica: Specifiche di Privacy che non si Compongono

Problematica
I pubblicatori di dati energetici rilasciano regolarmente statistiche sul consumo di elettricità, registri di impianti e log di ricarica, spesso accompagnati dalla promessa che individui o piccoli gruppi non possano essere identificati. Queste promesse vengono tipicamente verificate su base "one-shot", controllando ogni rilascio isolatamente rispetto a una regola di privacy dichiarata (ad esempio, $k$-anonimato con $k \ge 5$). Tuttavia, i pubblicatori emettono questi dataset sequenzialmente nel corso degli anni. Il documento sostiene che un rilascio che appare sicuro in isolamento può rivelare significativamente più informazioni se accatastato con rilasci precedenti o successivi. Nello specifico, il documento identifica che le specifiche di privacy a rilascio singolo spesso non si compongono nel tempo, portando a "attacchi di differenziazione" (differencing attacks) dove la sottrazione tra rilasci consecutivi espone gruppi marginali (ad esempio, un cambiamento di 1–4 metri in un quartiere) che erano stati singolarmente soppressi.

Metodologia
Gli autori propongono una pipeline di audit a due lati per valutare i rilasci di dati energetici pubblici sia empiricamente che formalmente.

1. Misurazione Empirica: L'audit misura la postura di re-identificazione dei file rilasciati utilizzando metriche di controllo della divulgazione consolidate ($k$-anonimato, $\ell$-diversità, $t$-closeness) tramite un'implementazione Python personalizzata (pyARX-equiv) validata incrociatamente con la libreria di riferimento ARX. Utilizza inoltre giochi avversari (singling-out, linkability, inference) usando il framework Anonymeter e un profiler specifico del dominio (PENM) come controlli secondari.
2. Verifica Formale: La politica di trasformazione dichiarata dal pubblicatore viene codificata come vincoli logici in formato SMT-LIB. Un portfolio di solver automatizzati (Z3 e Yices2) verifica se la politica codificata implica logicamente la garanzia di privacy dichiarata. Se la politica non implica la garanzia, il solver produce un core UNSAT etichettato.
3. Localizzazione del Gap: Quando viene rilevata una divergenza tra la postura empirica e la dichiarazione, il core UNSAT etichettato viene mappato su una di cinque famiglie di fallimento: Quasi-Identificatore Mancante, Composizione di Finestra di Rilascio Non Sicura, Errore nell'Ordine delle Operazioni, Collegamento tra Rilasci Diversi o Omissione di Documentazione.
4. Diagnostica Longitudinale: Per i rilasci sequenziali, l'audit introduce due diagnostiche: "emivita della specifica" (il numero di rilasci dopo i quali una regola a finestra singola non descrive più della metà della serie) e "budget di validità della specifica" ($W^*$), che quantifica quanti rilasci una regola a finestra singola rimane descrittiva prima di decadere.

Contributi Chiave

• Framework di Audit a Due Lati: Una nuova metodologia che combina la misurazione empirica dei dati con la verifica formale della politica dichiarata dal pubblicatore, permettendo l'identificazione di assunzioni mancanti piuttosto che la semplice misurazione del rischio.
• Confutazione Formale delle Specifiche: Il documento dimostra che i solver formali possono confutare la regola di privacy dichiarata stessa. Trattando i conteggi dei dati come variabili sconosciute, gli autori mostrano che la politica documentata (ad esempio, $k \ge 5$ per finestra) permette intrinsecamente coppie di rilasci non sicure, indipendentemente dai valori specifici dei dati.
• Artefatto di Riproducibilità: Gli autori rilasciano il codice di audit, le politiche codificate, le dichiarazioni verbum del pubblicatore e i template di divulgazione, coprendo un corpus di undici rilasci che spaziano in quattro tipi di dati energetici (tracce domestiche, ricarica EV, registri di asset e trasparenza di sistema).

Risultati
L'audit è stato applicato a undici dataset energetici pubblici (più una serie di utility statunitense come comparatore).

• Fallimento di Composizione (BEIS): Nelle statistiche elettriche sub-nazionali del Regno Unito (BEIS/DESNZ), la regola dichiarata $k \ge 5$ è rispettata per i singoli rilasci annuali. Tuttavia, la differenziazione tra rilasci rivela che il 93% delle aree subisce una transizione di 1–4 metri tra un anno e l'altro, esponendo un gruppo inferiore ai cinque metri. L' "emivita della specifica" per questa serie è di tre rilasci annuali; dopo questo punto, la regola a finestra singola non descrive più la serie.
• Dipendenza dalla Volatilità: Un confronto con la serie utility US EIA-861 mostra che il rischio di composizione non è uniforme. La serie US, caratterizzata da totali di utility più stabili, decade molto più lentamente (non raggiunge mai la soglia di emivita attraverso 11 rilasci) rispetto ai volatili dati domestici del Regno Unito.
• Unicità Strutturale vs. Operativa: Sebbene quasi tutti i rilasci presentino un'unicità strutturale ($k=1$ sui quasi-identificatori pubblicati), il rischio di re-identificazione operativa stimato (probabilità di identificare una persona reale) è effettivamente zero per nove dei dieci rilasci di persone naturali, eccetto per il rilascio di ricarica EV ACN-Data.
• Divergenze Specifiche:
  • BEIS: Divergenza dovuta a "Composizione di Finestra di Rilascio Non Sicura".
  • MaStR (Registro Impianti Tedesco): Divergenza dovuta a "Quasi-Identificatore Mancante" (la tupla pubblicata permette impianti singleton).
  • GoiEner: Divergenza dovuta a "Errore nell'Ordine delle Operazioni" (soppressione applicata dopo l'hashing).
  • OCPP-EV: Omissione di documentazione riguardo alle definizioni di avversario.
• Collegamento Ausiliario: Collegare il registro MaStR alla tabella delle unità del regolatore stesso rende il 24% degli impianti unicamente identificabile, evidenziando come i registri ausiliari del pubblicatore stesso siano il principale vettore di amplificazione.

Significatività e Rivendicazioni
Il documento sostiene che la modalità di fallimento dominante nella privacy dei dati energetici non è l'unicità di un singolo rilascio, ma il fallimento delle protezioni nel comporsi attraverso una sequenza di rilasci. Gli autori affermano che:

1. Gli audit a rilascio singolo sono insufficienti: Non possono rilevare la minaccia di "differenziazione" inerente ai regimi di ripubblicazione periodica imposti da regolamenti come la piattaforma di trasparenza ENTSO-E o le metodologie DESNZ.
2. La verifica formale aggiunge valore: Sposta l'attenzione dalla misurazione del rischio all'identificazione del gap logico specifico nella politica del pubblicatore (ad esempio, la mancanza di un operatore di budget per la finestra incrociata).
3. Remediation Azionabile: Gli autori propongono un "budget di validità della specifica" ($W^*$) come un controllo di audit pratico. I pubblicatori dovrebbero dichiarare le chiavi che spaziano tra le ripubblicazioni, misurare l'erosione della composizione prima di ogni rilascio e pubblicare un budget di validità per indicare per quanto tempo la loro regola a finestra singola rimane descrittiva.

Il documento dichiara esplicitamente di non pretendere di aver re-identificato individui specifici nei dati aggregati BEIS, ma piuttosto che l'esistenza e la dimensione di piccoli gruppi marginali possono essere inferite, il che costituisce un fallimento del controllo della divulgazione rispetto alla logica dichiarata dal pubblicatore. Il lavoro è posizionato come un audit di dati pubblici esistenti, non come una proposta di nuovi meccanismi di privacy differenziale, sebbene rilevi che le protezioni legacy "degradano scarsamente sotto composizione" in modo simile alle scoperte riguardanti la riprogettazione del Censimento USA 2020.