SuperDP: Differential Privacy Refutation via Supermartingales

1. Il Problema: La Verifica e la Refutazione della Privacy Differenziale

La Privacy Differenziale (DP) è lo standard formale per garantire la privacy dei dati individuali nei calcoli statistici. Un algoritmo probabilistico è detto $\epsilon$-DP se, modificando leggermente l'input (es. cambiando un singolo record), la distribuzione delle probabilità degli output non cambia in modo significativo.

Sebbene la definizione sia matematicamente elegante, il ragionamento sulla DP è complesso e soggetto a errori. La verifica formale della DP è un problema indecidibile per linguaggi di programmazione probabilistici completi (Turing-completi). Di conseguenza, la ricerca si è divisa in due direzioni:

1. Verifica DP: Dimostrare che un meccanismo è DP.
2. Refutazione DP: Dimostrare che un meccanismo non è DP (trovare un controesempio).

Il paper si concentra sulla refutazione automatica e formale. Le sfide principali affrontate dagli approcci esistenti sono:

• Automazione: Molti metodi richiedono intervento umano.
• Supporto per distribuzioni continue: Molti strumenti funzionano solo su domini discreti o finiti, mentre i meccanismi DP reali (come il rumore Laplaciano) usano distribuzioni continue.
• Garanzie di correttezza (Soundness): I metodi statistici (dinamici) non offrono garanzie formali, ma solo probabilità.
• Semi-completezza: Garantire che il metodo trovi un controesempio se esiste, sotto certe condizioni.

2. Metodologia: Refutazione tramite "Mismatch di Aspettativa"

Il cuore dell'approccio SuperDP è una nuova regola di prova basata sul concetto di mismatch di aspettativa (expectation mismatch), che evita la ricerca diretta di eventi di output specifici.

Il Concetto Chiave

Invece di cercare un evento di output $A$ tale che $P_{x_1}(A) > e^\epsilon \cdot P_{x_2}(A)$, il metodo cerca:

1. Una coppia di input simili $x_1 \sim_\Phi x_2$.
2. Una funzione non negativa $f$ sugli output.
3. Tale che l'aspettativa di $f$ sui due input violi il vincolo:
   $$E_{x_1}[f] > e^\epsilon \cdot E_{x_2}[f]$$

Il paper dimostra teoricamente che questa condizione è necessaria e sufficiente per la violazione della $\epsilon$-DP.

Strumenti Matematici: Supermartingale e Submartingale

Poiché calcolare esattamente il valore atteso $E[f]$ è spesso impossibile (specialmente con cicli non limitati o distribuzioni complesse), SuperDP utilizza:

• UESM (Upper Expectation Supermartingales): Per calcolare un limite superiore ($U$) per $E_{x_2}[f]$.
• LESM (Lower Expectation Submartingales): Per calcolare un limite inferiore ($L$) per $E_{x_1}[f]$.

Se si riesce a trovare $x_1, x_2, f, L, U$ tali che $L > e^\epsilon \cdot U$, allora la disuguaglianza $E_{x_1}[f] > e^\epsilon \cdot E_{x_2}[f]$ è garantita, e la DP è refutata.

Algoritmo di Sintesi Basata su Template

L'algoritmo automatizza la ricerca di questi oggetti attraverso una sintesi basata su template:

1. Template: Si definiscono template simbolici (polinomi) per gli input $x_1, x_2$, la funzione $f$, e le martingale $L_f, U_f$.
2. Raccolta Vincoli: Si generano vincoli algebrici che assicurano che i template soddisfino le condizioni di UESM/LESM e la disuguaglianza di refutazione.
3. Eliminazione dei Quantificatori: Si utilizzano teoremi di geometria algebrica (Teorema di Handelman) per trasformare i vincoli universali in sistemi di disuguaglianze lineari/esistenziali.
4. Risoluzione SMT: Un solver SMT (come Z3 o MathSAT5) risolve il sistema per trovare i coefficienti concreti che costituiscono la prova formale.

3. Contributi Chiave

Il paper presenta quattro contributi fondamentali che distinguono SuperDP dallo stato dell'arte:

1. Regola di Prova Completa e Sound: Introduce il "witness di martingala super/sub-aspettativa", una regola di prova sound e completa per la refutazione della $\epsilon$-DP in programmi probabilistici con espressioni aritmetiche misurabili di Borel e campionamento da distribuzioni discrete e continue.
2. Automazione Piena: L'algoritmo è completamente automatico e non richiede input manuali oltre al programma e alla relazione di similarità.
3. Supporto per Distribuzioni Continue: A differenza di molti strumenti precedenti, SuperDP gestisce nativamente distribuzioni continue (Laplaciana, Normale, Uniforme) e programmi con variabili reali.
4. Garanzie di Semi-Completezza Condizionale: Sebbene il problema sia indecidibile in generale, l'algoritmo garantisce di trovare un controesempio se esiste un witness esprimibile tramite polinomi e se l'invariante di supporto è chiuso e limitato.

4. Risultati Sperimentali

Gli autori hanno implementato un prototipo chiamato SuperDP e lo hanno confrontato con lo stato dell'arte:

• Baseline Statiche: CheckDP (l'unico altro strumento automatico per refutazione formale).
• Baseline Dinamiche: StatDP (metodo statistico basato su campionamento).

Risultati su 15 Benchmark:

• Efficacia: SuperDP ha refutato la DP con il valore di $\epsilon$ più alto (o ha dimostrato la violazione per $\epsilon$ arbitrariamente grandi) in 13 su 15 casi. Ha gestito con successo esempi complessi (come il meccanismo geometrico con cicli non limitati e il meccanismo "lowprob") che hanno fatto fallire o timeout gli altri strumenti.
• Efficienza: In 11 casi su 15, SuperDP è stato più veloce o competitivo rispetto alle baseline, spesso completando l'analisi in meno di 3 secondi.
• Limiti: SuperDP ha avuto difficoltà con benchmark che richiedono un ragionamento simbolico complesso su probabilità di ramificazioni condizionali (es. if x >= y dove x è un campione Laplaciano) o con sistemi di vincoli di grado molto elevato, portando a timeout in alcuni casi specifici (NoisyMax, SVT).

5. Significato e Impatto

Questo lavoro rappresenta un avanzamento significativo nella verifica formale della privacy:

• Superamento dei limiti precedenti: È il primo metodo che combina automazione completa, supporto per distribuzioni continue, garanzie di soundness e semi-completezza.
• Affidabilità: Fornisce prove formali matematiche di violazione della privacy, superando l'incertezza intrinseca dei metodi statistici (che possono dare falsi positivi/negativi).
• Fondazione Teorica: Estende l'uso delle martingale (tradizionalmente usate per analisi di terminazione e sicurezza) al dominio della privacy differenziale, offrendo un nuovo paradigma per l'analisi di sistemi probabilistici.

In sintesi, SuperDP trasforma la refutazione della privacy differenziale da un problema spesso manuale o statisticamente approssimato in un processo automatizzato, rigoroso e capace di gestire la complessità dei meccanismi DP moderni.