Resumen Técnico: Verificación Formal de la Seguridad por Sondeo mediante Independencia Condicional

Enunciado del Problema

Los ataques por canales laterales representan una amenaza significativa para la seguridad de los esquemas criptográficos, lo que ha impulsado la adopción generalizada del enmascaramiento como contramedida. El enmascaramiento divide los valores secretos en compartimentos para garantizar que la fuga de cualquier subconjunto de valores intermedios no revele el secreto subyacente. Sin embargo, demostrar la seguridad de los algoritmos enmascarados, particularmente bajo el modelo de sondeo ISW (donde un adversario puede sondear hasta $t$ valores intermedios), es notoriamente propenso a errores cuando se realiza manualmente. Se han identificado varias fallas en las pruebas de seguridad manuales, lo que hace necesaria la verificación formal.

Aunque la lógica de separación probabilística se ha aplicado con éxito para verificar propiedades como la independencia de entrada (por ejemplo, en libretas de un solo uso), aún no se ha utilizado para verificar la seguridad por sondeo (específicamente la no-interferencia $t$) de los algoritmos enmascarados. Las herramientas existentes de verificación formal a menudo dependen de métodos basados en sustitución o inferencia de tipos, los cuales pueden carecer de la modularidad o expresividad necesarias para el razonamiento condicional complejo inherente al enmascaramiento.

Metodología

Este trabajo propone un enfoque novedoso para la verificación formal estableciendo una conexión rigurosa entre las definiciones de seguridad basadas en simuladores y la independencia condicional. La metodología se basa en Lilac, una lógica de separación probabilística diseñada para razonar sobre la independencia condicional.

1. Fundamento Teórico: Simuladores e Independencia Condicional

Los autores reformulan la definición estándar de no-interferencia basada en simuladores en términos de independencia condicional.

• Visión basada en simuladores: Un algoritmo enmascarado es seguro si, para cualquier conjunto de sondeos $O$ (observados por un adversario), existe un simulador que puede generar la distribución de $O$ utilizando únicamente un subconjunto de compartimentos de entrada $I$, sin acceso a los compartimentos secretos restantes.
• Visión de independencia condicional: Este requisito de seguridad es equivalente a la afirmación de que los valores observados $O$ son condicionalmente independientes de los compartimentos de entrada secretos ($\Delta \setminus I$) dados los compartimentos de entrada públicos $I$. Formalmente, esto se expresa como $O \perp (\Delta \setminus I) \mid I$.

El artículo demuestra que esta equivalencia se mantiene dentro del marco semántico de Lilac, que modela la independencia probabilística utilizando combinaciones independientes de espacios de probabilidad y el condicionamiento mediante desintegración.

2. Extensión de Lilac

Para aplicar Lilac a la seguridad por sondeo, los autores extienden la lógica con reglas de prueba específicas que no estaban presentes en la formulación original de Lilac:

• Axiomas Semi-Grafoide: El artículo demuestra que los axiomas semi-gradoides para la independencia condicional (Simetría, Descomposición, Unión Débil y Contracción) se cumplen dentro de la semántica de Lilac. Estos axiomas son cruciales para manipular las afirmaciones de independencia condicional durante las pruebas.
• Reglas de Composición: Se introducen nuevas reglas para manejar la composición de propiedades de no-interferencia, específicamente para la composición secuencial y los bucles for. Estas reglas permiten la verificación modular de algoritmos complejos construidos a partir de componentes más pequeños.
• Propiedad y Debilitamiento: Reglas adicionales facilitan el razonamiento sobre la propiedad de las variables aleatorias y el debilitamiento de las propiedades de no-interferencia al tratar con entradas no compartidas o subconjuntos de variables.

3. Marco de Verificación

El proceso de verificación implica:

1. Traducir los algoritmos enmascarados (escritos en el lenguaje de programación probabilística APPL) a triples de Hoare dentro de Lilac.
2. Utilizar la equivalencia establecida (Teorema V.1) para reducir la verificación de la no-interferencia $(I, O)$ a la demostración de un triple de Hoare de independencia condicional específico:
   $$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$$
3. Aplicar el conjunto extendido de reglas de prueba (incluyendo los nuevos axiomas semi-gradoides y las reglas de composición) para derivar las implicaciones requeridas.

Contribuciones Clave

1. Conexión Formal: El artículo establece una equivalencia formal entre las definiciones de seguridad por sondeo basadas en simuladores y las propiedades de independencia condicional expresables en Lilac. Esto cierra la brecha entre las nociones de seguridad criptográfica y la lógica de separación probabilística.
2. Extensión de Lilac: Los autores proporcionan un conjunto de reglas de prueba adicionales necesarias para verificar algoritmos enmascarados, incluyendo los axiomas semi-gradoides para la independencia condicional y las reglas de composición para la composición secuencial y los bucles.
3. Estudios de Caso: La efectividad del enfoque se demuestra mediante la verificación formal de la seguridad por sondeo de tres algoritmos críticos utilizando Lilac:
   • MINIADDREPNOISE: Una subrutina para agregar ruido uniforme a valores enmascarados.
   • REFRESH: Un algoritmo fundamental para refrescar compartimentos y prevenir la acumulación de fugas.
   • SECMULT: Un algoritmo estándar de multiplicación enmascarada.
   • ADDREPNOISEER: Una variante utilizada en el esquema de firma Raccoon (un candidato para la estandarización de Criptografía Post-Cuántica del NIST), demostrando que satisface la propiedad de No-Interferencia Fuerte $t$ con Entrada No Compartida ($t$-SNIU).

Resultados

El artículo deriva con éxito triples de Hoare para los algoritmos objetivo, confirmando sus propiedades de no-interferencia.

• Para MINIADDREPNOISE, la prueba muestra que los compartimentos de salida son condicionalmente independientes de los compartimentos de entrada no observados dados los inputs observados.
• Para REFRESH, la prueba verifica que el algoritmo satisface la No-Interferencia Fuerte $t$ ($t$-SNI), una propiedad más fuerte que la no-interferencia estándar, esencial para la composabilidad en enmascaramiento de orden superior.
• Para SECMULT y ADDREPNOISEER, las pruebas aprovechan las nuevas reglas de composición para manejar los bucles anidados y las dependencias de datos complejas inherentes a estos algoritmos.

La verificación de ADDREPNOISEER es particularmente significativa ya que valida un componente clave de la prueba de seguridad del esquema de firma Raccoon, el cual depende de la propiedad $t$-SNIU.

Significado y Afirmaciones

Los autores afirman que este trabajo proporciona la primera aplicación de la lógica de separación probabilística (específicamente Lilac) a la verificación formal de la seguridad por sondeo para algoritmos enmascarados. Al traducir las pruebas de seguridad al razonamiento de independencia condicional, el enfoque ofrece una alternativa modular y lógicamente rigurosa a las herramientas existentes basadas en sustitución o inferencia de tipos.

El artículo enfatiza que, aunque la idea subyacente de conectar simuladores con independencia condicional es conceptualmente simple, su formalización en Lilac es técnicamente no trivial debido a la dependencia de la lógica en combinaciones independientes en lugar de espacios de probabilidad de producto estándar. La derivación exitosa del teorema principal y la aplicación a componentes criptográficos del mundo real (Raccoon) demuestran que este marco es viable para verificar esquemas de enmascaramiento complejos y de alto orden.

El trabajo se mantiene modesto en cuanto a su alcance, señalando que los resultados actuales se limitan al entorno de información teórica de la seguridad por sondeo. Los autores identifican la extensión del enfoque al entorno computacional e implementar el método en un demostrador de teoremas interactivo como direcciones importantes para el trabajo futuro. También sugieren que el marco podría aplicarse a otras propiedades de seguridad basadas en simuladores, como las encontradas en la computación multipartita segura.