Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy

1. El Problema

La verificación de propiedades de seguridad en sistemas complejos (especialmente protocolos distribuidos) se basa tradicionalmente en encontrar invariantes induktivos seguros. Un invariante induktivo es una propiedad que se cumple en los estados iniciales y se preserva en cada transición del sistema; si implica la propiedad de seguridad deseada, la prueba está completa.

Sin embargo, a medida que los sistemas y sus propiedades se vuelven más complejos, los invariantes induktivos necesarios pueden volverse extremadamente complicados. Esta complejidad se manifiesta en:

• Estructura Booleana compleja: Necesidad de combinaciones intrincadas de conjunciones y disyunciones (no-clausales).
• Cuantificación: Uso de múltiples cuantificadores y, críticamente, alternancias de cuantificadores (ej. $\forall \exists \forall$).
• Desafíos: Esta complejidad genera un espacio de búsqueda enorme para la síntesis automática de invariantes y dificulta la validación de la induktividad debido a problemas de decidibilidad y escalabilidad.

Los enfoques existentes de razonamiento modular (dividir el sistema en componentes) a menudo no son suficientes cuando un solo componente requiere pruebas intrincadas.

2. Metodología

Los autores proponen un enfoque incremental que divide la prueba de seguridad en una secuencia de pasos más simples, en lugar de buscar un único invariante complejo. Este sistema de pruebas combina tres pilares fundamentales:

A. Razonamiento Hacia Adelante y Hacia Atrás (Forward-Backward)

• Razonamiento Hacia Adelante: Utiliza invariantes induktivos estándar que se mantienen en todos los estados alcanzables desde el inicio.
• Razonamiento Hacia Atrás: Utiliza invariantes induktivos de un sistema con el tiempo invertido. Estos invariantes se mantienen en todos los estados que pueden alcanzar un estado "malo" (bad state) si se retrocede en el tiempo.
• Sinergia: Al combinar ambos, la prueba puede utilizar predicados auxiliares que no son invariantes puros hacia adelante ni hacia atrás, pero que son válidos a lo largo de cualquier traza de error (desde el inicio hasta un estado malo). Esto permite simplificar la estructura booleana de los predicados, eliminando disyunciones complejas que serían necesarias en una prueba puramente hacia adelante.

B. Profecía (Prophecy)

• Se introduce un mecanismo para manejar la cuantificación existencial. En lugar de mantener variables cuantificadas existencialmente ($\exists x$) en los invariantes, se introduce un testigo de profecía (un símbolo constante fresco $w$) que representa un elemento específico que satisface una propiedad.
• Condición de Sonoridad: Para que un paso de profecía sea válido, se debe demostrar que para cualquier traza de error, existe un valor para el testigo que satisface la propiedad a lo largo de toda la traza. Esto se formaliza como un problema de seguridad auxiliar.
• Beneficio: Esto permite eliminar alternancias de cuantificadores y reducir la profundidad de cuantificación en los invariantes auxiliares, transformando fórmulas complejas en conjunciones de cláusulas universalmente cuantificadas.

C. Pruebas Incrementales

El sistema permite construir la prueba paso a paso:

1. Probar un invariante simple (hacia adelante o hacia atrás).
2. Añadirlo como axioma al problema de seguridad.
3. Repetir el proceso con invariantes más simples bajo la nueva suposición.
4. Finalmente, demostrar que la combinación de estos invariantes simples implica la seguridad.

El artículo demuestra teóricamente que cualquier prueba incremental de este tipo puede convertirse en un único invariante induktivo seguro para el sistema original, pero que el proceso de conversión revela que el invariante final es una combinación booleana compleja de los invariantes simples usados en los pasos.

3. Contribuciones Clave

1. Sistema de Pruebas Incremental: Definición de un sistema formal que combina razonamiento hacia adelante, hacia atrás y la introducción de profecías de manera sinérgica.
2. Caracterización de la Sonoridad de la Profecía: Formalización de la condición de sonoridad para los testigos de profecía como un problema de seguridad auxiliar, lo que permite verificar su validez dentro del mismo marco de trabajo.
3. Traducción a Invariantes Induktivos: Demostración de que cualquier prueba incremental (con o sin profecía) puede transformarse en un invariante induktivo seguro estándar, estableciendo la equivalencia lógica y permitiendo analizar la complejidad de los invariantes resultantes.
4. Aumento del Poder de Prueba: Prueba teórica de que, bajo restricciones naturales en el conjunto de fórmulas disponibles, cada regla de prueba (incrementalidad, retroceso, profecía) aumenta estrictamente el poder de prueba del sistema. Es decir, existen problemas que no tienen invariante induktivo seguro dentro de un conjunto de fórmulas dado, pero sí tienen una prueba incremental con ese mismo conjunto.
5. Estudio de Caso: Aplicación exitosa a protocolos de consenso distribuido complejos (Paxos, sus variantes y Raft).

4. Resultados

El equipo aplicó su metodología a varios modelos de Paxos (incluyendo variantes como Flexible Paxos, Multi-Paxos, Fast Paxos) y Raft, utilizando el verificador mypyvy y el solver Z3.

• Simplificación Booleana: En la mayoría de los casos, las pruebas hacia adelante y hacia atrás permitieron reemplazar invariantes no-clausales (con mezclas de $\land$ y $\lor$) por conjunciones de cláusulas puras (solo disyunciones). Esto reduce drásticamente el espacio de búsqueda para la síntesis automática.
• Eliminación de Cuantificadores: El uso de profecía permitió eliminar alternancias de cuantificadores y cuantificadores existenciales de los predicados especificados por el usuario. Por ejemplo, invariantes que requerían $\exists \forall$ se redujeron a cláusulas universalmente cuantificadas ($\forall$) al introducir testigos de profecía.
• Rendimiento:
  • Las pruebas simplificadas redujeron los tiempos de verificación en ejemplos difíciles (de ~1.6s a ~0.6s en Paxos FOL, y de ~3.7s a ~2.8s en Raft).
  • Para ejemplos más simples, los tiempos se mantuvieron comparables.
  • Se demostró que es posible probar la seguridad de variantes de Paxos y Raft utilizando únicamente predicados universalmente cuantificados y clausales, algo que las herramientas de inferencia de invariantes de última generación no lograron hacer automáticamente sin ayuda manual o con tiempos de ejecución muy largos.

5. Significado e Impacto

Este trabajo es significativo por varias razones:

• Novedad en la Interacción: Es la primera vez que se explora sistemáticamente la sinergia entre el razonamiento hacia adelante/hacia atrás y las variables de profecía en la verificación de protocolos.
• Reducción del Espacio de Búsqueda: Al permitir que las pruebas incrementales utilicen fórmulas más simples (clausales y sin alternancias), el enfoque facilita enormemente la automatización de la verificación. Las herramientas de inferencia de invariantes pueden enfocarse en un espacio de búsqueda mucho más pequeño y manejable.
• Generalidad: Aunque se centra en protocolos distribuidos, la metodología es aplicable a cualquier sistema modelado en lógica de primer orden donde la complejidad de los invariantes sea un cuello de botella.
• Herramientas: El trabajo ha sido integrado en la herramienta mypyvy, haciendo que estas técnicas avanzadas sean accesibles para la comunidad de verificación formal.

En resumen, el artículo demuestra que descomponer una prueba de seguridad compleja en pasos incrementales que combinan análisis hacia adelante, hacia atrás y profecías no solo es teóricamente sólido, sino que ofrece beneficios prácticos tangibles al simplificar la estructura lógica de los invariantes necesarios para verificar sistemas críticos.