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

Resumo Técnico: Especificações de Privacidade que não se Compõem

Definição do Problema
Publicadores de dados energéticos lançam rotineiramente estatísticas sobre o consumo de eletricidade, registros de usinas e logs de carregamento, frequentemente acompanhadas por uma promessa de que indivíduos ou pequenos grupos não podem ser identificados. Essas promessas são tipicamente verificadas de forma "unilateral" (one-shot), checando cada lançamento isoladamente contra uma regra de privacidade declarada (ex: $k$-anonimato com $k \ge 5$). No entanto, os publicadores emitem esses conjuntos de dados sequencialmente ao longo dos anos. O artigo argumenta que um lançamento que parece seguro isoladamente pode revelar significativamente mais informações quando empilhado com lançamentos anteriores ou subsequentes. Especificamente, o artigo identifica que as especificações de privacidade de lançamento único falham frequentemente ao se comporem ao longo do tempo, levando a "ataques de diferenciação" (differencing attacks), onde a subtração de lançamentos consecutivos expõe grupos marginais (ex: uma mudança de 1–4 metros em um bairro) que foram individualmente suprimidos.

Metodologia
Os autores propõem um pipeline de auditoria de dois lados para avaliar os lançamentos de dados de energia pública tanto de forma empírica quanto formal.

1. Medição Empírica: A auditoria mede a postura de reidentificação dos arquivos lançados usando métricas estabelecidas de controle de divulgação ($k$-anonimato, $\ell$-diversidade, $t$-proximidade) via uma implementação customizada em Python (pyARX-equiv) validada cruzadamente contra a biblioteca de referência ARX. Também emprega jogos adversariais (singling-out, linkability, inference) usando o framework Anonymeter e um perfilador específico do domínio (PENM) como verificações secundárias.
2. Verificação Formal: A política de transformação declarada pelo publicador é codificada como restrições lógicas no formato SMT-LIB. Um portfólio de solvers automatizados (Z3 e Yices2) verifica se a política codificada implica logicamente a garantia de privacidade reivindicada. Se a política não implica a garantia, o solver produz um núcleo UNSAT rotulado.
3. Localização de Lacunas: Quando uma divergência é detectada entre a postura empírica e a reivindicação declarada, o núcleo UNSAT rotulado é mapeado para uma de cinco famílias de falhas: Quasi-Identificador Ausente, Composição de Janela de Lançamento Insegura, Erro de Ordem de Operações, Vinculação entre Lançamentos ou Omissão de Documentação.
4. Diagnósticos Longitudinais: Para lançamentos sequenciais, a auditoria introduz dois diagnósticos: "meia-vida da especificação" (o número de lançamentos após o qual uma regra de janela única não descreve mais do que metade da série) e "orçamento de validade da especificação" ($W^*$), que quantifica quantos lançamentos uma regra de janela única permanece descritiva antes de decair.

Principais Contribuições

• Framework de Auditoria de Dois Lados: Uma metodologia inovadora que combina a medição empírica dos dados com a verificação formal da política declarada pelo publicador, permitindo a identificação de suposições ausentes em vez de apenas medir o risco.
• Refutação Formal de Especificações: O artigo demonstra que solvers formais podem refutar a própria regra de privacidade declarada. Ao tratar contagens de dados como variáveis desconhecidas, os autores mostram que a política documentada (ex: por janela $k \ge 5$) permite intrinsecamente pares de lançamentos inseguros, independentemente de valores de dados específicos.
• Artefato de Reprodutibilidade: Os autores liberam o código de auditoria, as políticas codificadas, as reivindicações verbais do publicador e os templates de divulgação, cobrindo um corpus de onze lançamentos abrangendo quatro tipos de dados de energia (traços domésticos, carregamento de VE, registros de ativos e transparência do sistema).

Resultados
A auditoria foi aplicada a onze conjuntos de dados de energia pública (mais uma série de utilidades dos EUA como comparador).

• Falha de Composição (BEIS): Nas estatísticas de eletricidade subnacionais do Reino Unido (BEIS/DESNZ), a regra declarada de $k \ge 5$ mantém-se para lançamentos anuais individuais. No entanto, a diferenciação entre lançamentos revela que 93% das áreas passam por uma transição de 1–4 metros entre os anos, expondo um grupo de menos de cinco metros. A "meia-vida da especificação" para esta série é de três lançamentos anuais; após este ponto, a regra de janela única não descreve mais a série.
• Dependência de Volatilidade: Uma comparação com a série de utilidades EIA-861 dos EUA mostra que o risco de composição não é uniforme. A série dos EUA, caracterizada por totais de utilidades mais estáveis, decai muito mais devagar (nunca atingindo o limiar de meia-vida ao longo de 11 lançamentos) comparada aos voláteis dados domésticos do Reino Unido.
• Unicidade Estrutural vs. Operacional: Embora quase todos os lançamentos exibam unicidade estrutural ($k=1$ nos quasi-identificadores publicados), o risco de reidentificação operacional estimado (probabilidade de identificar uma pessoa real) é efetivamente zero para nove dos dez lançamentos de pessoas naturais, exceto para o lançamento de carregamento de VE ACN-Data.
• Divergências Específicas:
  • BEIS: Divergência devido a "Composição de Janela de Lançamento Insegura".
  • MaStR (Registro de Plantas Alemão): Divergência devido a "Quasi-Identificador Ausente" (a tupla publicada permite plantas singulares).
  • GoiEner: Divergência devido a "Erro de Ordem de Operações" (supressão aplicada após o hashing).
  • OCPP-EV: Omissão de documentação em relação às definições de adversários.
• Vinculação Auxiliar: Vincular o registro MaStR contra a própria tabela de unidades do regulador torna 24% das plantas unicamente identificáveis, destacando que os próprios registros auxiliares do publicador são o principal vetor de amplificação.

Significância e Alegações
O artigo alega que o modo de falha dominante na privacidade de dados de energia não é a unicidade de um único lançamento, mas a falha das proteções em se comporem através de uma sequência de lançamentos. Os autores afirmam que:

1. Auditorias de lançamento único são insuficientes: Elas não conseguem detectar a ameaça de "diferenciação" inerente aos regimes de republicação periódica exigidos por regulamentações como a plataforma de transparência da ENTSO-E ou metodologias da DESNZ.
2. A verificação formal agrega valor: Ela vai além de medir o risco para identificar a lacuna lógica específica na política do publicador (ex: a falta de um operador de orçamento de janela cruzada).
3. Remediação Acionável: Os autores propõem um "orçamento de validade da especificação" ($W^*$) como um controle de auditoria prático. Os publicadores devem declarar as chaves que abrangem as republicações, medir a erosão da composição antes de cada lançamento e publicar um orçamento de validade para indicar por quanto tempo sua regra de janela única permanece descritiva.

O artigo declara explicitamente que não pretende ter reidentificado indivíduos específicos nos dados agregados do BEIS, mas sim que a existência e o tamanho de pequenos grupos marginais podem ser inferidos, o que constitui uma falha de controle de divulgação relativa à lógica declarada pelo publicador. O trabalho posiciona-se como uma auditoria de dados públicos existentes, não como uma proposta de novos mecanismos de privacidade diferencial, embora note que as proteções legadas "degradam-se mal sob composição", de forma semelhante aos achados no redesign do Censo de 2020 dos EUA.