Cómo Twins detecta pérdida de estado y doble voto en protocolos BFT

En HotStuff-2, DAG-BFT y Twins Twins apareció como una herramienta de la frontera. Aquí lo miramos con lupa: qué emula exactamente, cómo construye escenarios y qué tipo de errores puede sacar a la luz. Twins es una metodología de testing para sistemas BFT propuesta por Bano y coautores. [1]

El problema de fondo es incómodo. Una prueba de safety en papel razona sobre un adversario arbitrario, pero un test unitario razona sobre los casos que su autor imaginó. Los bugs de consenso suelen vivir en el hueco entre ambos: una combinación concreta de líder, retrasos y estado local que nadie escribió a mano.

La idea: dos instancias, una identidad

Escribir un nodo bizantino a mano es caro. Hay que decidir qué mentiras dice, cuándo y a quién, y cada estrategia maliciosa es un programa nuevo que mantener. Twins evita ese trabajo con un truco: ejecuta dos instancias de la misma réplica, con la misma identidad y las mismas claves, y las dos corren el código correcto sin modificar. [1]

Para las demás réplicas, los dos gemelos son un único participante. Si cada gemelo está en una parte distinta de la red, cada uno ve propuestas distintas y responde con honestidad a lo que ve. Desde fuera, esa réplica acaba de firmar dos votos o dos propuestas en conflicto para la misma ronda. Eso es equivocación, y aparece sin una sola línea de código malicioso. [1]

Como un sistema con $n = 3f + 1$ réplicas tolera a lo sumo $f$ bizantinas, Twins limita la duplicación a $f$ réplicas. [1] Una réplica con gemelo se cuenta como bizantina; las demás son correctas, y sobre ellas se verifican las propiedades. Esa elección mantiene el experimento dentro del modelo de fallas del protocolo: si algo se rompe, se rompió con un adversario que el protocolo promete tolerar.

Qué fallas bizantinas cubre y cuáles no

Los autores agrupan los comportamientos que Twins reproduce en tres familias: equivocación, voto doble y pérdida del estado interno. [1] Las dos primeras salen directamente de que los gemelos vean mensajes distintos. La tercera es más sutil y es la que da título a este artículo.

Imagina que un gemelo estuvo en la partición donde se formó un QC y se bloqueó en él, mientras el otro gemelo estaba aislado y nunca lo vio. Si en la ronda siguiente la red pone al segundo gemelo junto a las réplicas que reciben una propuesta conflictiva, ese gemelo vota sin ninguna restricción. Para el resto del sistema, esa identidad acaba de comportarse como una réplica que olvidó su lockedQC. La amnesia se emula sin simular un disco ni un reinicio.

Twins no pretende cubrir todo lo que un adversario arbitrario puede hacer. Los gemelos siempre ejecutan el protocolo; no envían mensajes mal formados ni inventan campos. El argumento del paper es que los ataques que importan contra protocolos de la familia HotStuff, los que rompen safety o detienen el progreso, se reducen en la práctica a combinaciones de equivocación, voto doble y amnesia. [1] Validar mensajes mal formados sigue siendo trabajo de otras pruebas.

Generación sistemática de escenarios

Un escenario de Twins fija, para cada ronda, quién es el líder y cómo se parte la red. Dentro de una partición los mensajes se entregan; entre particiones se descartan. [1] Con eso basta para describir situaciones que un tester humano tardaría en imaginar: un líder gemelo que propone una cosa a un grupo y otra al otro, una réplica correcta que se queda sin oír un QC, o un cambio de vista en el que solo parte de la red vio la propuesta anterior.

El generador construye los escenarios en etapas: enumera las particiones posibles de las réplicas, las combina con las asignaciones de líder y luego encadena esas combinaciones a lo largo de varias rondas. [1] El número de escenarios crece de forma combinatoria con las réplicas y las rondas, de modo que la búsqueda se acota con parámetros explícitos y puede recorrerse de forma exhaustiva dentro de esos límites o muestrearse.

La ejecución es determinista: la misma descripción produce la misma traza. [1] Eso cambia la relación con un bug. En lugar de un fallo intermitente en un clúster real, el equipo recibe un escenario que se puede reproducir, reducir y convertir en test de regresión. Los autores describen su implementación sobre la base de código de DiemBFT, el descendiente de HotStuff diseñado para producción. [1] [3]

Anatomía de un bug de pérdida de estado

Veamos un ejemplo ilustrativo construido por TrautsLab, no un caso reportado en el paper. Supón una implementación de Chained HotStuff que guarda su lockedQC y su última ronda votada solo en memoria. Las reglas del protocolo son correctas: una réplica solo vota una propuesta que extienda su lockedQC o que traiga un QC de vista más alta. [2] El problema está en la implementación, que puede perder ese estado.

La réplica $R_1$ vota la propuesta $A$ en la vista 5 y queda bloqueada en el QC correspondiente. Después se reinicia y vuelve con su estado inicial. En la vista 6 un líder propone $A'$, que no extiende $A$. Con la memoria vacía, $R_1$ no tiene nada que le prohíba votar, y su voto puede completar un QC conflictivo junto a réplicas que no vieron $A$. El argumento de safety de HotStuff cuenta con que cada réplica correcta del quórum recuerde su lock; aquí el testigo correcto de la intersección perdió la memoria. [2]

Twins encuentra este tipo de error sin modelar el reinicio, porque un gemelo que no vio el bloqueo produce exactamente la misma secuencia de votos que una réplica amnésica. La corrección obvia es persistir el estado de safety antes de enviar el voto. DiemBFT aísla ese estado en un módulo de safety separado, que lleva la ronda más alta votada y el QC de referencia para decidir si es seguro votar. [3]

Figura 1

Secuencia ilustrativa de un bug de pérdida de estado

Fuentes:

[1]

Cómo leer esta figura

El diagrama muestra una línea de tiempo con cuatro marcas. En t1 la réplica R1 vota A en la vista 5 y fija su lockedQC. En t2 ocurre un crash con reinicio sin estado persistido. En t3 lockedQC vuelve a su valor inicial. En t4, en la vista 6, R1 vota A' y rompe safety.

Descargar SVGDescargar .tex

Código TikZ

Abrir `.tex` en otra pestaña

Bugs de liveness: particiones, líderes y rondas perdidas

No todos los errores que encuentra Twins rompen safety. El mismo generador produce escenarios en los que nadie firma nada contradictorio y, aun así, el sistema deja de avanzar. [1] Un patrón típico: una partición deja a parte de las réplicas correctas bloqueadas en un QC que el resto no conoce, el siguiente líder construye sobre un certificado más viejo y una fracción de las réplicas lo rechaza. Si ningún lado reúne $n - f$ votos, la ronda muere, y si el patrón se repite en las rondas siguientes, el sistema se estanca.

Por eso Twins mira liveness además de safety: no basta con que nadie confirme bloques en conflicto, también hay que comprobar que las réplicas correctas siguen confirmando. [1] Para que la prueba sea justa, el veredicto de liveness tiene sentido cuando el escenario deja de partir la red, porque con particiones permanentes ningún protocolo bajo sincronía parcial promete progreso. Un bug de este tipo suele apuntar al Pacemaker o a la información que viaja en el cambio de vista: si el highQC de las réplicas no llega al líder siguiente, el líder no puede proponer algo que todas las réplicas correctas acepten. [2]

Ojo con la interpretación. Que Twins no encuentre un error dentro de los límites explorados no demuestra que el protocolo sea correcto; demuestra que ningún escenario de ese espacio lo rompe. Twins complementa una prueba formal y la revisión de diseño, no las sustituye.

Siguiente lectura

Para repasar las reglas de bloqueo que Twins pone a prueba, vuelve a QC, highQC y three-chain. Si quieres ver el diseño de producción sobre el que se implementó Twins, continúa con DiemBFT, Jolteon y Ditto.