💻 computer science

SuperDP: Differential Privacy Refutation via Supermartingales

Este artigo apresenta o SuperDP, uma ferramenta totalmente automatizada que refuta a privacidade diferencial ( $\epsilon$ -DP) utilizando supermartingales e submartingales de expectativa para encontrar contraexemplos em mecanismos estocásticos com distribuições discretas e contínuas, oferecendo garantias de correção e semi-completude superiores aos métodos existentes.

Autores originais: Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, {\DJ}or{\dj}e Žikelić

Publicado 2026-03-30

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, {\DJ}or{\dj}e Žikelić

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem uma máquina mágica que analisa dados sensíveis (como notas de alunos ou registros médicos) e devolve estatísticas úteis, mas sem revelar a identidade de ninguém. Essa é a promessa da Privacidade Diferencial (DP). É como se a máquina dissesse: "Eu posso te contar a média das notas, mas se eu mudar a nota de apenas um aluno, a média que eu te der será quase a mesma. Assim, ninguém consegue descobrir a nota de ninguém."

No entanto, criar essas máquinas é difícil. Um pequeno erro de programação pode fazer com que a máquina "vaze" segredos. O grande desafio é: como provar que uma máquina NÃO é segura? (Ou seja, como provar que ela está vazando informações?)

É aqui que entra o trabalho dos autores, chamado SuperDP. Vamos explicar como eles fazem isso usando uma analogia simples.

O Problema: Encontrar a Falha na Armadura

Pense na privacidade como uma armadura blindada. Para provar que a armadura é forte, você tenta atirar nela com flechas (dados de entrada). Se a flecha atravessar, a armadura é fraca.
O problema é que, em programas de computador complexos, não é fácil saber onde atirar. Você pode tentar milhões de combinações e nunca achar o ponto fraco, ou pior, achar um ponto que parece fraco, mas na verdade é uma ilusão de ótica.

Os métodos antigos tentavam:

Testar aleatoriamente: Jogar muitas flechas e ver o que acontece (lento e não garante 100% de certeza).
Analisar o código manualmente: Tentar adivinhar onde está o buraco (muito difícil e propenso a erros humanos).

A Solução: SuperDP e a "Balança Mágica"

Os autores criaram uma nova ferramenta chamada SuperDP. Em vez de apenas atirar flechas aleatoriamente, eles usam uma abordagem matemática inteligente baseada em algo chamado Supermartingales (uma palavra chique da teoria das probabilidades).

Vamos usar uma analogia de Balança e Peso:

A Ideia Central: Em vez de tentar encontrar um resultado específico que vaze o segredo, o SuperDP procura por uma "função de peso" (uma regra matemática) que, quando aplicada aos resultados da máquina, cria um desequilíbrio enorme.
O Experimento:
- Pegue dois cenários quase idênticos (ex: um aluno tirou 10, o outro tirou 9).
- Passe esses dois cenários pela máquina.
- A máquina devolve resultados aleatórios.
- O SuperDP cria uma "régua" especial (a função não-negativa).
- Se, ao pesar os resultados da régua, a média do cenário 1 for muito maior do que a média do cenário 2 (além de um limite permitido), a máquina foi pega! Ela vazou a diferença.

Como o SuperDP faz isso automaticamente?

Aqui entra a mágica da Supermartingale (Supermartingala). Imagine que você tem dois guardiões invisíveis:

O Guardião Superior (Supermartingale): Ele garante que o valor máximo que a máquina pode entregar no cenário 2 não ultrapasse certo limite.
O Guardião Inferior (Submartingale): Ele garante que o valor mínimo que a máquina entrega no cenário 1 não fique abaixo de certo limite.

O SuperDP usa matemática avançada para criar esses guardiões e a "régua" de peso ao mesmo tempo. Ele diz:

"Olhem! Se eu usar essa régua específica, o valor mínimo do cenário 1 é 100, e o valor máximo do cenário 2 é 10. Como 100 é muito maior que 10, a máquina não pode ser segura!"

Isso é como se o SuperDP não apenas apontasse o buraco na armadura, mas também desenhasse o mapa exato do buraco e provasse matematicamente que ele existe, sem precisar testar milhões de vezes.

Por que isso é revolucionário?

O artigo destaca quatro qualidades que tornam o SuperDP único:

Totalmente Automático: Você não precisa ser um gênio da matemática para usar. Você joga o código do programa e a ferramenta faz o resto.
Funciona com Tudo: Funciona tanto com dados inteiros (como contagem de pessoas) quanto com números decimais contínuos (como ruído de Laplace, usado em privacidade real).
Garantia de Verdade (Sonoridade): Se o SuperDP diz "essa máquina é insegura", é verdade. Não é uma aposta estatística. É uma prova matemática.
Quase Completo: Se houver um jeito de provar que a máquina é insegura usando essa lógica, o SuperDP vai achar.

O Resultado na Prática

Os autores testaram o SuperDP em vários exemplos famosos da literatura de privacidade.

O que aconteceu? O SuperDP conseguiu provar que várias máquinas eram inseguras, inclusive em casos onde as ferramentas anteriores falhavam ou demoravam horas.
Comparação: Enquanto outras ferramentas tentavam "chutar" e às vezes erravam (dizendo que algo era inseguro quando não era, ou não achando o erro), o SuperDP foi preciso e rápido.

Resumo em uma frase

O SuperDP é como um detetive matemático que, em vez de vasculhar a casa inteira procurando uma janela aberta, constrói um modelo matemático que prova, de uma vez só, que a janela tem que estar aberta, garantindo que a privacidade foi violada de forma irrefutável.

Isso é um grande passo para garantir que, quando usamos dados sensíveis, as ferramentas de proteção realmente funcionem como prometem.

1. O Problema

A Privacidade Diferencial (DP) é o padrão formal para garantir a privacidade de dados individuais em algoritmos estocásticos. No entanto, verificar se um mecanismo satisfaz a DP é uma tarefa complexa e propensa a erros. Pequenas alterações em mecanismos corretos podem quebrar a propriedade de privacidade.

O problema central abordado neste trabalho é a refutação de DP (demonstrar que um mecanismo não é $\epsilon$ -DP).

Desafios existentes: Métodos anteriores de refutação automática são limitados. Métodos dinâmicos (baseados em amostragem) não oferecem garantias formais de correção. Métodos estáticos muitas vezes não são totalmente automatizados, restringem-se a distribuições discretas ou não suportam variáveis de ponto flutuante e distribuições contínuas (como Laplaciana), que são essenciais na prática.
Objetivo: Desenvolver um método totalmente automatizado, com garantias de correção (soundness) e semi-completude, capaz de lidar com programas probabilísticos que incluem tanto distribuições discretas quanto contínuas.

2. Metodologia

A proposta dos autores, chamada SuperDP, baseia-se na ideia de "mismatch de expectativa" (descompasso de expectativa) e utiliza conceitos de análise de programas probabilísticos, especificamente Supermartingales de Expectativa Superior (UESM) e Submartingales de Expectativa Inferior (LESM).

Conceito Central: Refutação via Expectativa

Em vez de procurar diretamente um evento de saída $A$ onde a probabilidade viola a desigualdade de DP ( $P_{x_1}[A] > e^\epsilon \cdot P_{x_2}[A]$ ), o método procura:

Um par de entradas similares $x_1 \sim x_2$ .
Uma função não negativa $f$ sobre as saídas do programa.
Demonstrar que a expectativa de $f$ nessas entradas viola a condição:
$E_{x_1}[f] > e^\epsilon \cdot E_{x_2}[f]$
O artigo prova que essa condição é necessária e suficiente para refutar a $\epsilon$ -DP.

O Papel dos Martingales

Como calcular a expectativa exata de $f$ é frequentemente inviável (devido a laços não limitados ou distribuições complexas), o método utiliza:

UESM (Upper Expectation Supermartingale): Fornece um limite superior ( $U$ ) para $E_{x_2}[f]$ .
LESM (Lower Expectation Submartingale): Fornece um limite inferior ( $L$ ) para $E_{x_1}[f]$ .

O algoritmo busca simultaneamente as entradas, a função $f$ e os martingales de forma que a desigualdade $L > e^\epsilon \cdot U$ seja satisfeita. Se essa desigualdade for verdadeira, a DP é refutada.

Algoritmo de Síntese Baseada em Modelos (Template-based Synthesis)

O método é implementado como um algoritmo automatizado para programas aritméticos polinomiais:

Templates: Define-se templates simbólicos (polinômios) para as entradas, a função $f$ e os martingales $U_f$ e $L_f$ .
Coleta de Restrições: Gera um sistema de restrições que garante que os martingales satisfaçam as condições de definição (como a condição de "Zero na saída" e a propriedade de aumento/disminuição esperada) e que a desigualdade de refutação seja válida.
Eliminação de Quantificadores: Utiliza o Teorema de Handelman da geometria algébrica para transformar restrições universais em restrições existenciais sobre os coeficientes dos polinômios.
Resolução: Um solver SMT (Satisfiability Modulo Theories) resolve o sistema de restrições. Se uma solução for encontrada, ela constitui uma prova formal de refutação.

3. Principais Contribuições

O trabalho apresenta quatro contribuições principais que distinguem o SuperDP do estado da arte:

Regra de Prova Completa e Sólida: Introduz a noção de "Witness de Super/Sub-martingale de Expectativa" para refutação de DP. É provado que essa regra é sólida (se o witness existe, a DP é realmente violada) e completa (se a DP for violada, um witness existe) para programas probabilísticos com expressões aritméticas Borel-mensuráveis e amostragem de distribuições discretas e contínuas.
Algoritmo Automatizado: Desenvolve um algoritmo que é sólido e condicionalmente semi-completo. Isso significa que, sob certas condições (como o uso de polinômios e invariantes adequados), o algoritmo garantirá encontrar uma refutação se ela existir.
Suporte Geral: É o primeiro método de refutação de DP que suporta:
- Total automação.
- Programas com variáveis reais e distribuições contínuas (ex: Laplaciana, Normal).
- Garantias formais de correção.
Ferramenta SuperDP: Implementação de um protótipo que demonstra a viabilidade prática do método.

4. Resultados Experimentais

Os autores avaliaram o SuperDP em 15 benchmarks da literatura, comparando-o com o estado da arte:

Baselines:
- CheckDP: Análise estática (suporte limitado a Laplaciana, sem garantias de completude).
- StatDP: Análise dinâmica/estatística (sem garantias formais, requer muitas amostras).
Desempenho:
- O SuperDP conseguiu refutar a DP em 13 de 15 benchmarks, superando ou igualando os baselines em todos os casos.
- Em benchmarks onde a DP é violada para qualquer $\epsilon$ finito, o SuperDP conseguiu refutar valores de $\epsilon$ até 15, enquanto o CheckDP falhou na maioria e o StatDP não conseguiu refutar nenhum.
- O SuperDP foi mais rápido que os baselines em 11 dos 15 casos, com tempos de execução geralmente inferiores a 3 segundos.
- O método foi capaz de refutar casos complexos (como o mecanismo "geometric" com laços não limitados estaticamente) que causaram erros de tempo de execução ou falhas nos métodos existentes.

5. Significado e Limitações

Significado:
O trabalho preenche uma lacuna crítica na verificação formal de privacidade. Ao fornecer um método automatizado, sólido e capaz de lidar com distribuições contínuas, o SuperDP permite que desenvolvedores e verificadores detectem falhas de privacidade em mecanismos complexos com confiança matemática, algo que métodos estatísticos não oferecem e que métodos estáticos anteriores não conseguiam fazer de forma geral.

Limitações:

Restrição a $\epsilon$ -DP: O método atual refuta apenas a definição estrita de $\epsilon$ -DP. A extensão para $(\epsilon, \delta)$ -DP (mais comum na prática) não é direta devido à natureza da desigualdade envolvida.
Aritmética Polinomial: O algoritmo de síntese assume que as expressões aritméticas do programa são polinômios. Embora suporte amostragem de distribuições não polinomiais (como Laplaciana), a lógica interna do programa deve ser polinomial.
Complexidade de Restrições: Em programas com muitos locais ou que exigem polinômios de alto grau, o sistema de restrições pode tornar-se computacionalmente caro para os solvers SMT.

Em resumo, o SuperDP representa um avanço significativo na verificação formal de privacidade, combinando teoria de martingales com síntese automatizada para oferecer uma ferramenta robusta de refutação de DP.