Verificación Formal en Consenso: Modelado matemático con TLA+

Las pruebas de un sistema distribuido tienen un problema de fondo: ejecutan algunas ejecuciones, no todas. En un consenso BFT, el error que importa suele ser una intercalación rara de mensajes, un líder que equivoca y un cambio de vista que llega en el peor momento. La verificación formal ataca ese problema desde otro ángulo: primero se escribe el diseño como un objeto matemático y después se pregunta si una propiedad vale en todos sus estados alcanzables.

Este artículo presenta TLA+ desde la perspectiva de quien diseña protocolos tipo HotStuff. Veremos qué se especifica, cómo se escribe un invariante de safety, por qué liveness requiere fórmulas temporales y supuestos de equidad, en qué se diferencian TLC y Apalache, y por qué todo esto complementa, sin reemplazar, a las pruebas sistemáticas como Twins.

Qué especifica TLA+: estados, acciones y comportamientos

TLA, la lógica temporal de acciones de Lamport, es una lógica para especificar y razonar sobre sistemas concurrentes. Su rasgo distintivo es que el sistema y sus propiedades se escriben en la misma lógica, de modo que "el sistema cumple su especificación" y "un sistema implementa otro" se expresan ambos como implicaciones lógicas. [1]

Los ingredientes son pocos. Un estado asigna valores a las variables. Una acción es una fórmula que relaciona un estado con el siguiente: las variables sin prima hablan del estado actual y las variables con prima (votes') del siguiente. Un comportamiento es una secuencia infinita de estados. La especificación típica tiene la forma $Init \land \Box[Next]_{vars}$, más condiciones de equidad cuando se quiere hablar de progreso: "el primer estado satisface $Init$ y cada paso es un paso de $Next$ o deja $vars$ sin cambios". [1]

Ese último detalle, permitir pasos que no cambian nada (stuttering), no es un tecnicismo. Es lo que permite comparar una especificación abstracta con otra más detallada: un paso del modelo abstracto puede corresponder a varios pasos internos del refinado. Para un consenso, eso significa que se puede escribir primero "las réplicas deciden un único valor" y después demostrar que un protocolo con fases, votos y certificados implementa esa abstracción. [1]

TLA+ es el lenguaje de especificación construido sobre esa lógica. Sus primitivas incluyen booleanos, enteros, funciones, tuplas, registros, secuencias y conjuntos de todo ello, y los diseñadores lo usan para especificar protocolos concurrentes, distribuidos y tolerantes a fallas que tradicionalmente se presentan en pseudocódigo. [2]

Un fragmento ilustrativo: votos, quórums y un invariante

El siguiente módulo es un ejemplo didáctico escrito para este artículo; no proviene de ningún proyecto real ni modela HotStuff completo. Describe una sola ranura de decisión: réplicas correctas que votan a lo sumo una vez, réplicas bizantinas que pueden votar varios bloques y una acción de commit que exige un quórum de más de dos tercios.

---------------------------- MODULE ToyVoting ----------------------------
\* Fragmento ilustrativo: no proviene de ningun proyecto real.
EXTENDS Naturals, FiniteSets
 
CONSTANTS Replicas, Byz, Blocks
ASSUME Byz \subseteq Replicas /\ 3 * Cardinality(Byz) < Cardinality(Replicas)
 
VARIABLES votes, committed
vars == <<votes, committed>>
 
Correct == Replicas \ Byz
Quorums == { Q \in SUBSET Replicas :
               3 * Cardinality(Q) > 2 * Cardinality(Replicas) }
 
Init == /\ votes = [r \in Replicas |-> {}]
        /\ committed = {}
 
CorrectVote(r, b) == /\ r \in Correct
                     /\ votes[r] = {}
                     /\ votes' = [votes EXCEPT ![r] = {b}]
                     /\ UNCHANGED committed
 
ByzVote(r, b) == /\ r \in Byz
                 /\ votes' = [votes EXCEPT ![r] = @ \union {b}]
                 /\ UNCHANGED committed
 
Commit(b) == /\ \E Q \in Quorums : \A r \in Q : b \in votes[r]
             /\ committed' = committed \union {b}
             /\ UNCHANGED votes
 
Next == \E r \in Replicas, b \in Blocks :
          CorrectVote(r, b) \/ ByzVote(r, b) \/ Commit(b)
 
Spec == Init /\ [][Next]_vars
 
NoConflictingCommits == Cardinality(committed) <= 1
===========================================================================

Leámoslo como un diseñador. Init fija el estado inicial: nadie votó y nada está confirmado. CorrectVote codifica la regla de una réplica correcta, que solo vota si aún no lo hizo. ByzVote deja a una réplica bizantina añadir cualquier bloque a su conjunto de votos, que es la forma más simple de modelar la equivocación. Commit permite confirmar un bloque cuando todas las réplicas de algún quórum lo votaron.

NoConflictingCommits es el invariante: en esta ranura única, dos bloques distintos cuentan como conflicto, así que nunca debe haber más de uno confirmado. Es la versión de juguete del teorema de safety de HotStuff, que afirma que dos nodos en conflicto no pueden ser confirmados, cada uno por una réplica correcta. [3] El argumento que el model checker confirmaría por fuerza bruta es el de siempre: dos quórums de más de dos tercios comparten más réplicas de las que el adversario controla, y la réplica correcta del cruce no vota dos veces.

Safety como invariante, liveness como fórmula temporal

Safety dice que algo malo nunca ocurre, y por eso se comprueba estado a estado: si existe un estado alcanzable con dos commits en conflicto, el model checker devuelve la traza que lleva hasta él. Liveness dice que algo bueno acaba ocurriendo, y eso no se puede ver en un estado aislado: hace falta una fórmula temporal sobre comportamientos completos, como $\Diamond(committed \neq \emptyset)$, "en algún momento se confirma algo". [1]

La fórmula $\Box[Next]_{vars}$ por sí sola permite que el sistema se quede quieto para siempre, porque los pasos sin cambios siempre están permitidos. Para hablar de progreso hay que añadir supuestos de equidad, como la equidad débil $WF_{vars}(Next)$: si una acción queda habilitada de forma continua, termina ejecutándose. [1]

El juguete anterior enseña aquí algo útil. Aun con equidad, la liveness falla: con cuatro réplicas, una bizantina y dos bloques, las tres correctas pueden repartir sus votos dos contra uno y la bizantina puede negarse a completar el quórum de ninguno de los dos. Nada viola safety, pero nada se confirma nunca. Ese contraejemplo es exactamente la razón por la que los protocolos reales tienen vistas, líderes y cambios de vista.

HotStuff formula su liveness con esa forma: después de GST existe un periodo acotado tal que, si todas las réplicas correctas permanecen en la vista $v$ durante ese periodo y el líder de $v$ es correcto, se alcanza una decisión. [3] Especificar eso en TLA+ obliga a modelar tiempo o, de forma más abstracta, a declarar como supuesto de equidad que eventualmente hay una vista suficientemente larga con líder correcto. Ese supuesto queda escrito y revisable, en lugar de esconderse en un comentario del código.

TLC y Apalache: enumerar estados o resolver restricciones

Una especificación no se comprueba sola. TLC, el model checker clásico de TLA+, enumera explícitamente valores y estados; Apalache, presentado como el primer model checker simbólico para TLA+, traduce la relación de transición a restricciones SMT sin cuantificadores y delega la búsqueda en un solver. [2]

Ambos comparten un supuesto que conviene tener presente al leer cualquier resultado: todos los parámetros de la especificación están fijados y todos los estados son estructuras finitas. [2] En el ejemplo, eso significa elegir Replicas con cuatro elementos, Byz con uno y Blocks con dos. Si la herramienta no encuentra violaciones, la conclusión es sobre esa instancia. Extenderla a todo $n$ requiere una prueba, a mano o con un asistente de demostración, como la que acompaña al paper de HotStuff. [3]

La diferencia práctica entre las dos herramientas está en cómo escalan. La enumeración explícita es directa y produce trazas legibles, pero sufre cuando el espacio de estados crece por combinatoria de mensajes, votos y vistas. Los autores de Apalache reportan que su herramienta supera a TLC en ejemplos con espacios de estados grandes. [2] No es una regla universal para elegir; es un motivo para probar ambas sobre la misma especificación.

Qué aporta frente a Twins y qué no

Twins aborda el mismo miedo desde la implementación. En lugar de una especificación, crea copias gemelas de un nodo con la misma identidad y credenciales, de modo que el resto del sistema ve a un único nodo que se comporta de forma sospechosa; así emula equivocación del líder, doble voto y pérdida de estado interno como los locks. [4] Los escenarios se generan sistemáticamente variando particiones y líderes por ronda, y los autores reportan que su despliegue sobre DiemBFT puede ejecutar 44 millones de escenarios al día. [4]

Los autores son explícitos sobre el contraste: la enumeración exhaustiva de fallas bizantinas en model checking conduce a explosión de estados, y Twins la evita modelando solo ejecuciones correctas, a cambio de cubrir muchos, pero no todos, los ataques bizantinos. La caracterización formal de esa cobertura queda como problema abierto. [4]

De ahí sale una división de trabajo razonable. TLA+ pregunta si el diseño es seguro en todas las ejecuciones de una instancia pequeña, incluidas las que nadie imaginó. Twins pregunta si el código que corre en producción respeta ese diseño frente a escenarios bizantinos generados a escala. Ninguna sustituye a la otra: un modelo verificado no detecta un lockedQC que la implementación olvida persistir, y una batería de escenarios no garantiza que el diseño no tenga una traza mala que ningún generador produjo.

La trampa más común es leer un resultado limpio como "el protocolo está demostrado". Ojo con eso. Un model checker valida la especificación que se le dio, con los parámetros que se fijaron y los supuestos de equidad que se escribieron. Si el modelo omite el cambio de vista, nada dice sobre el cambio de vista.

Siguiente lectura

Para ver cómo se generan escenarios bizantinos contra una implementación real, sigue con Twins: detección de errores de estado y bloqueos. Si quieres repasar las propiedades que una especificación de HotStuff debería capturar, vuelve a Safety, liveness y responsiveness en HotStuff.