SuperDP: Differential Privacy Refutation via Supermartingales

Resumen Técnico: SuperDP

1. El Problema: Refutación de Privacidad Diferencial (DP)

La Privacidad Diferencial (DP) es el estándar actual para garantizar la privacidad de los datos individuales en algoritmos aleatorizados. Formalmente, un mecanismo es $\epsilon$-DP si la probabilidad de cualquier evento de salida no cambia significativamente (por un factor de $e^\epsilon$) cuando se modifica ligeramente la entrada (por ejemplo, la presencia o ausencia de un solo individuo).

Aunque la definición es sólida, verificar o refutar si un programa estocástico cumple con DP es una tarea extremadamente difícil y propensa a errores:

• Indecidibilidad: El problema de verificar DP para lenguajes de programación probabilística Turing-completos es indecidible.
• Limitaciones de métodos existentes:
  • Los métodos dinámicos (basados en muestreo) carecen de garantías formales de corrección (son estadísticos).
  • Los métodos estáticos existentes a menudo no son totalmente automáticos, se limitan a dominios finitos o discretos, o no soportan distribuciones continuas (como la Laplaciana o Gaussiana), que son fundamentales en la práctica.
  • Ningún método anterior ofrecía simultáneamente: automatización total, soporte para distribuciones continuas, garantías de sonido (si dice que no es DP, realmente no lo es) y garantías de semi-completitud.

El objetivo de este trabajo es desarrollar un método para la refutación automática y formal de la propiedad $\epsilon$-DP. Es decir, demostrar que un mecanismo no es privado encontrando un contraejemplo.

2. Metodología: Desajuste de Expectativa y Martingalas

La propuesta central de los autores es un nuevo enfoque basado en el desajuste de expectativa (expectation mismatch) y el uso de supermartingalas y submartingalas de expectativa.

A. El Principio de Desajuste de Expectativa
En lugar de buscar directamente un evento de salida $A$ que viole la desigualdad de DP, el método busca:

1. Un par de entradas similares $x_{in}^1 \sim x_{in}^2$.
2. Una función no negativa $f$ sobre las salidas del programa.
3. Tal que la esperanza de $f$ en la primera entrada sea significativamente mayor que en la segunda:
   $$E_{x_{in}^1}[f] > e^\epsilon \cdot E_{x_{in}^2}[f]$$
   El teorema 4.6 demuestra que esta condición es necesaria y suficiente para refutar $\epsilon$-DP.

B. Uso de Supermartingalas y Submartingalas
Calcular el valor esperado exacto de una función en programas probabilísticos es a menudo inviable (no tiene forma cerrada). Para superar esto, SuperDP utiliza:

• Supermartingalas de Expectativa Superior (UESM): Para calcular una cota superior ($U$) de la esperanza en la segunda entrada.
• Submartingalas de Expectativa Inferior (LESM): Para calcular una cota inferior ($L$) de la esperanza en la primera entrada.

El método busca un testigo (witness) que consista en un tuple $(x_{in}^1, x_{in}^2, f, L_f, U_f)$ tal que:
$$L_f(x_{in}^1) > e^\epsilon \cdot U_f(x_{in}^2)$$
Donde $L_f$ y $U_f$ son funciones que satisfacen condiciones de martingala (basadas en el Teorema de Parada Opcional - OST) que garantizan que $L$ es una cota inferior válida y $U$ una superior válida.

C. Algoritmo de Síntesis Basada en Plantillas
Para automatizar la búsqueda de este testigo, el algoritmo:

1. Asume que el programa es un programa aritmético probabilístico (con expresiones polinómicas).
2. Define plantillas simbólicas polinómicas para las entradas, la función $f$, y las funciones de martingala ($L_f, U_f$).
3. Recopila un sistema de restricciones sobre los coeficientes de estas plantillas que aseguran:
   • Que las entradas son similares.
   • Que $f$ es no negativa.
   • Que $L_f$ y $U_f$ cumplen las condiciones de martingala (disminución/incremento esperado).
   • Que se cumple la desigualdad de refutación.
4. Utiliza eliminación de cuantificadores universales (Teorema de Handelman) y un solver SMT (como Z3 o MathSAT5) para resolver el sistema de restricciones y encontrar los coeficientes concretos.

3. Contribuciones Clave

El trabajo presenta cuatro contribuciones principales que lo distinguen del estado del arte:

1. Regla de Prueba Sonda y Completa: Introducen el concepto de "testigo de super/sub-martingala de expectativa" para la refutación de DP. Demuestran teóricamente que esta regla es sonda (si encuentra un testigo, la refutación es correcta) y completa (si el programa no es DP, existe tal testigo bajo ciertas condiciones).
2. Automatización Total: El método es completamente automático, sin necesidad de intervención humana para guiar la búsqueda de contraejemplos.
3. Soporte General: Es aplicable a mecanismos estocásticos que utilizan tanto distribuciones discretas como continuas (ej. Laplaciana, Gaussiana), superando la limitación de herramientas anteriores que solo soportaban dominios finitos.
4. Garantías de Semi-completitud: A diferencia de métodos puramente estadísticos o heurísticos, ofrecen garantías formales. Si el algoritmo falla en encontrar un testigo, no significa necesariamente que el programa sea DP, pero si lo encuentra, la refutación es matemáticamente irrefutable.

4. Resultados Experimentales

Los autores implementaron una herramienta prototipo llamada SuperDP y la evaluaron contra el estado del arte (CheckDP para análisis estático y StatDP para análisis dinámico) en 15 ejemplos de la literatura.

• Efectividad: SuperDP logró refutar $\epsilon$-DP en 13 de 15 casos.
  • En los 9 casos donde el mecanismo es DP para un $\epsilon$ finito, SuperDP encontró límites de refutación más ajustados (más cercanos al valor teórico) en 7 casos.
  • En los 6 casos donde el mecanismo no es DP para ningún $\epsilon$ finito, SuperDP refutó valores de $\epsilon$ hasta 15 en todos los casos, mientras que CheckDP solo lo logró en 2 y StatDP en ninguno.
  • SuperDP fue capaz de manejar ejemplos que las herramientas anteriores no podían resolver (ej. mecanismos con distribuciones geométricas o Bernoulli).
• Eficiencia: En 11 de 15 casos, SuperDP fue más rápido que las herramientas de referencia. Los tiempos de ejecución fueron consistentemente bajos (generalmente < 3 segundos), excepto en casos con sistemas de restricciones muy grandes.
• Limitaciones Prácticas:
  • Dificultad en el razonamiento simbólico sobre probabilidades de bifurcaciones condicionales (if) complejas.
  • El tamaño del sistema de restricciones crece rápidamente con el grado del polinomio, lo que puede saturar a los solvers SMT en programas muy complejos.

5. Significado e Impacto

Este trabajo representa un avance significativo en la verificación formal de privacidad:

• Cierre de Brechas: Es la primera herramienta que combina automatización, soporte para distribuciones continuas y garantías formales de sonido/completitud.
• Rigor Formal: Proporciona una base teórica sólida para la refutación de DP, moviéndose más allá de las aproximaciones estadísticas que pueden dar falsos positivos o negativos.
• Aplicabilidad Práctica: Al manejar distribuciones continuas (como la Laplaciana, estándar en DP), el método es directamente aplicable a los mecanismos utilizados en la industria y la investigación actual.
• Nuevas Direcciones: Abre la puerta a futuras investigaciones para extender estas técnicas a la privacidad $(\epsilon, \delta)$-DP y a la verificación (prueba de que un programa sí es privado), no solo a la refutación.

En resumen, SuperDP establece un nuevo estándar para la detección automática de vulnerabilidades de privacidad en programas probabilísticos complejos, ofreciendo una herramienta robusta, teóricamente fundamentada y práctica.