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

Resumen Técnico: Especificaciones de Privacidad que no se Componen

Planteamiento del Problema
Los editores de datos energéticos publican rutinariamente estadísticas sobre el consumo de electricidad, registros de plantas y registros de carga, a menudo acompañadas de la promesa de que no se podrá identificar a individuos o grupos pequeños. Estas promesas se verifican típicamente de forma "unitaria", comprobando cada publicación de forma aislada frente a una regla de privacidad establecida (por ejemplo, $k$-anonimato con $k \ge 5$). Sin embargo, los editores emiten estos conjuntos de datos secuencialmente a lo largo de los años. El artículo sostiene que una publicación que parece segura de forma aislada puede revelar significativamente más información cuando se apila con publicaciones anteriores o posteriores. Específicamente, el artículo identifica que las especificaciones de privacidad de una sola publicación suelen fallar al componerse a lo largo del tiempo, lo que conduce a "ataques de diferenciación" donde la resta de publicaciones consecutivas expone grupos marginales (por ejemplo, un cambio de 1 a 4 metros en un vecindario) que fueron suprimidos individualmente.

Metodología
Los autores proponen un flujo de auditoría de dos lados para evaluar las publicaciones de datos energéticos públicos tanto de forma empírica como formal.

1. Medición Empírica: La auditoría mide la postura de reidentificación de los archivos publicados utilizando métricas establecidas de control de divulgación ($k$-anonimato, $\ell$-diversidad, $t$-cercanía) mediante una implementación personalizada en Python (pyARX-equiv) validada cruzadamente contra la biblioteca de referencia ARX. También emplea juegos adversariales (aislamiento, vinculabilidad, inferencia) utilizando el marco Anonymeter y un perfilador de dominio específico (PENM) como comprobaciones secundarias.
2. Verificación Formal: La política de transformación declarada por el editor se codifica como restricciones lógicas en formato SMT-LIB. Un portafolio de resolvedores automatizados (Z3 y Yices2) comprueba si la política codificada implica lógicamente la garantía de privacidad declarada. Si la política no implica la garantía, el resolvedor produce un núcleo UNSAT etiquetado.
3. Localización de Brechas: Cuando se detecta una divergencia entre la postura empírica y la afirmación declarada, el núcleo UNSAT etiquetado se mapea a una de cinco familias de fallos: Cuasi-Identificador Faltante, Composición de Ventana de Publicación Insegura, Error de Orden de Operaciones, Vinculación entre Publicaciones o Omisión de Documentación.
4. Diagnósticos Longitudinales: Para las publicaciones secuenciales, la auditoría introduce dos diagnósticos: "vida media de la especificación" (el número de publicaciones después de las cuales una regla de ventana única ya no describe más de la mitad de la serie) y "presupuesto de validez de la especificación" ($W^*$), que cuantifica cuántas publicaciones una regla de ventana única permanece descriptiva antes de decaer.

Contribuciones Clave

• Marco de Auditoría de Dos Lados: Una metodología novedosa que combina la medición empírica de los datos con la verificación formal de la política declarada por el editor, permitiendo la identificación de supuestos faltantes en lugar de solo medir el riesgo.
• Refutación Formal de Especificaciones: El artículo demuestra que los resolvedores formales pueden refutar la propia regla de privacidad declarada. Al tratar los recuentos de datos como variables desconocidas, los autores muestran que la política documentada (por ejemplo, por ventana $k \ge 5$) permite intrínsecamente pares de publicaciones inseguros, independientemente de los valores de datos específicos.
• Artefacto de Reproducibilidad: Los autores publican el código de auditoría, las políticas codificadas, las afirmaciones verbatim de los editores y las plantillas de divulgación, cubriendo un corpus de once publicaciones que abarca cuatro tipos de datos energéticos (trazas domésticas, carga de vehículos eléctricos, registros de activos y transparencia del sistema).

Resultados
La auditoría se aplicó a once conjuntos de datos energéticos públicos (más una serie de servicios públicos de EE. UU. como comparador).

• Fallo de Composición (BEIS): En las estadísticas subnacionales de electricidad del Reino Unido (BEIS/DESNZ), la regla establecida de $k \ge 5$ se mantiene para las publicaciones anuales individuales. Sin embargo, la diferenciación entre publicaciones revela que el 93% de las áreas experimentan una transición de 1 a 4 metros entre años, exponiendo un grupo de menos de cinco metros. La "vida media de la especificación" para esta serie es de tres publicaciones anuales; después de este punto, la regla de ventana única ya no describe la serie.
• Dependencia de la Volatilidad: Una comparación con la serie de servicios públicos EIA-861 de EE. UU. muestra que el riesgo de composición no es uniforme. La serie de EE. UU., caracterizada por totales de servicios públicos más estables, decae mucho más lento (nunca alcanza el umbral de vida media a través de 11 publicaciones) en comparación con los volátiles datos domésticos del Reino Unido.
• Unicidad Estructural vs. Operativa: Aunque casi todas las publicaciones exhiben unicidad estructural ($k=1$ en los cuasi-identificadores publicados), el riesgo de reidentificación operativa estimado (probabilidad de identificar a una persona real) es efectivamente cero para nueve de las diez publicaciones de personas naturales, excepto para la publicación de carga de vehículos eléctricos de ACN-Data.
• Divergencias Específicas:
  • BEIS: Divergencia debido a "Composición de Ventana de Publicación Insegura".
  • MaStR (Registro de Plantas Alemán): Divergencia debido a "Cuasi-Identificador Faltante" (la tupla publicada permite plantas únicas/singulares).
  • GoiEner: Divergencia debido a "Error de Orden de Operaciones" (supresión aplicada después del hashing).
  • OCPP-EV: Omisión de documentación respecto a las definiciones de adversarios.
• Vinculación Auxiliar: Vincular el registro MaStR contra la propia tabla de unidades del regulador hace que el 24% de las plantas sean identificables de forma única, resaltando que los propios registros auxiliares del editor son el principal vector de amplificación.

Significancia y Afirmaciones
El artículo afirma que el modo de fallo dominante en la privacidad de los datos energéticos no es la unicidad de una sola publicación, sino el fallo de las protecciones al componerse a través de una secuencia de publicaciones. Los autores sostienen que:

1. Las auditorías de una sola publicación son insuficientes: No pueden detectar la amenaza de "diferenciación" inherente a los regímenes de republicación periódica obligados por regulaciones como la Plataforma de Transparencia de ENTSO-E o las metodologías de DESNZ.
2. La verificación formal añade valor: Va más allá de medir el riesgo para identificar la brecha lógica específica en la política del editor (por ejemplo, la falta de un operador de presupuesto de ventana cruzada).
3. Remediación Accionable: Los autores proponen un "presupuesto de validez de la especificación" ($W^*$) como un control de auditoría práctico. Los editores deben declarar las claves que abarcan las republicaciones, medir la erosión de la composición antes de cada publicación y publicar un presupuesto de validez para indicar cuánto tiempo su regla de ventana única sigue siendo descriptiva.

El artículo establece explícitamente que no pretende haber reidentificado a individuos específicos en los datos agregados de BEIS, sino que la existencia y el tamaño de los grupos pequeños pueden inferirse, lo cual constituye un fallo de control de divulgación relativo a la lógica declarada por el editor. El trabajo se posiciona como una auditoría de datos públicos existentes, no como una propuesta de nuevos mecanismos de privacidad diferencial, aunque señala que las protecciones heredadas "degradan mal bajo la composición", de forma similar a los hallazgos en el rediseño del Censo de EE. UU. 2020.