Casper FFG (Ethereum): El gadget de finalidad amigable

Una cadena con regla de bifurcación al estilo Nakamoto nunca dice "esto ya no cambia": cada bloque nuevo hace menos probable una reorganización, pero no la vuelve imposible. Los protocolos BFT clásicos dicen exactamente lo contrario. En PBFT, una réplica ejecuta una petición cuando ve un certificado de $2f + 1$ mensajes coincidentes entre $3f + 1$ réplicas, y esa decisión ya no se revierte mientras haya a lo sumo $f$ réplicas defectuosas. [3]

Casper the Friendly Finality Gadget, de Vitalik Buterin y Virgil Griffith, intenta quedarse con lo mejor de ambos mundos. No reemplaza al mecanismo que produce bloques: se monta encima como una capa de finalidad de prueba de participación que elige, de forma irreversible, una única cadena canónica dentro del árbol de bloques. [1] El propio paper se describe como heredero de la tradición BFT de PBFT y menciona a Tendermint como el primer trabajo que reutilizó algoritmos BFT para prueba de participación. [1]

La palabra "gadget" importa. Casper FFG aporta safety, pero su liveness depende del mecanismo de propuesta elegido: si un atacante controla por completo quién propone bloques, Casper sigue impidiendo finalizar dos checkpoints en conflicto, aunque el atacante puede impedir que se finalice algo nuevo. [1]

Checkpoints, votos y enlaces de supermayoría

Para no razonar sobre cada bloque, Casper FFG trabaja sobre el árbol de checkpoints. En la versión del paper, la génesis es un checkpoint y también lo es todo bloque cuya altura sea múltiplo exacto de 100; la altura de checkpoint $h(c)$ cuenta cuántos checkpoints hay entre $c$ y la raíz. [1] Los autores explican la elección como un compromiso: más distancia entre checkpoints reduce el costo del algoritmo, pero alarga el tiempo hasta el consenso. [1]

Cada validador tiene un depósito, y todas las fracciones del protocolo se miden por depósito, no por número de validadores: "dos tercios de los validadores" significa un conjunto cuya suma de depósitos es dos tercios del total. [1] Es la versión ponderada del conteo de réplicas de PBFT.

Un voto contiene cuatro datos firmados: un checkpoint fuente $s$, un checkpoint destino $t$ y sus alturas $h(s)$ y $h(t)$. El destino debe descender de la fuente; si no, el voto es inválido. [1] Sobre esos votos se definen cuatro conceptos:

• Enlace de supermayoría $a \to b$: al menos dos tercios del depósito publicaron votos con fuente $a$ y destino $b$. Un enlace puede saltarse checkpoints, es decir, $h(b) > h(a) + 1$ está permitido. [1]
• Conflicto: dos checkpoints están en conflicto si ninguno es ancestro del otro.
• Justificado: un checkpoint $c$ está justificado si es la raíz o si existe un enlace de supermayoría $c' \to c$ desde un checkpoint $c'$ ya justificado.
• Finalizado: un checkpoint $c$ está finalizado si es la raíz o si está justificado y existe un enlace de supermayoría $c \to c'$ hacia un hijo directo, con $h(c') = h(c) + 1$. [1]

La analogía con PBFT no es decorativa. El paper de Gasper presenta justificación y finalización como conceptos análogos a las fases de prepare y commit de PBFT. [2] Justificar es reunir una supermayoría que apunta a un checkpoint; finalizar es ver una segunda supermayoría que lo usa como fuente para el checkpoint inmediatamente siguiente. Igual que en PBFT, un solo quórum no alcanza: hace falta un quórum que construya sobre otro.

Figura 1

Justificar y finalizar checkpoints con enlaces de supermayoría

Fuentes:

[1]

Cómo leer esta figura

Cuatro checkpoints en fila: Génesis, C1, C2 y C3, y una rama rival C2 prima que sale de C1. Dos arcos azules marcan enlaces de supermayoría de Génesis a C1 y de C1 a C2. Génesis y C2 están justificados, C1 está finalizado porque su hijo directo C2 se justificó desde él, y C3 solo está propuesto.

Descargar SVGDescargar .tex

Código TikZ

Abrir `.tex` en otra pestaña

Las dos reglas de slashing

La regla de oro de PBFT es que una réplica correcta no envía dos mensajes contradictorios para la misma vista y número de secuencia. [3] Casper FFG reduce todo su contrato de comportamiento a dos prohibiciones sobre pares de votos, que el paper llama los dos mandamientos de Casper. [1]

Escritas con la notación del paper, para dos votos $v_1 = (s_1, t_1)$ y $v_2 = (s_2, t_2)$ del mismo validador:

$\text{(I) doble voto:}\quad v_1 \neq v_2 \;\land\; h(t_1) = h(t_2)$

$\text{(II) voto envolvente:}\quad h(s_1) < h(s_2) < h(t_2) < h(t_1)$

La primera regla es la versión de Casper de "no votar dos cosas distintas en la misma ronda". La segunda es más sutil: prohíbe que un voto largo "salte por encima" de otro voto del mismo validador. Es la regla que protege a un checkpoint finalizado frente a una cadena alternativa que intente saltárselo, porque cualquier enlace que lo puentee terminaría encerrando el enlace de finalización.

Un detalle de diseño que conviene notar: versiones anteriores de Casper tenían dos tipos de mensaje y cuatro condiciones, y los autores las redujeron a un tipo de mensaje y dos condiciones a propósito, para que las violaciones fueran independientes del estado de la cadena. [1] Esa independencia es lo que permite que cualquiera, con dos firmas en la mano, demuestre la falta.

Cuando alguien detecta una violación, la evidencia puede incluirse en la cadena como transacción; en el paper, el validador pierde todo su depósito y quien envía la evidencia recibe una pequeña recompensa. [1] El capítulo siguiente de la serie, sobre el castigo financiero, desarrolla qué significa exactamente esa evidencia y por qué convierte un ataque en un hecho demostrable.

Figura 2

Las dos condiciones de slashing de Casper FFG

Fuentes:

[1]

Cómo leer esta figura

Panel izquierdo: un eje de alturas con dos votos que terminan en la misma altura h, uno desde h menos 2 y otro desde h menos 1. Panel derecho: el voto 1 va de h de s1 a h de t1 y envuelve al voto 2, que va de h de s2 a h de t2, con h de s1 menor que h de s2 menor que h de t2 menor que h de t1.

Descargar SVGDescargar .tex

Código TikZ

Abrir `.tex` en otra pestaña

Accountable safety: por qué un tercio queda expuesto

La propiedad central se llama accountable safety: dos checkpoints en conflicto no pueden finalizarse a menos que al menos un tercio de los validadores, por depósito, viole una de las dos condiciones. [1] Es una garantía distinta de la de PBFT. PBFT dice "si hay a lo sumo $f$ fallas, no hay conflicto". Casper dice "si hay conflicto, puedo señalar a los culpables y probarlo".

El origen del "un tercio" es la misma aritmética de quórums que en BFT clásico. Si dos conjuntos de votantes $V_1$ y $V_2$ reúnen cada uno al menos $\tfrac{2}{3}$ del depósito total $N$, su intersección pesa al menos

$w(V_1 \cap V_2) \ge \tfrac{2}{3}N + \tfrac{2}{3}N - N = \tfrac{1}{3}N.$

En PBFT, el argumento busca una réplica correcta en esa intersección. En Casper, la intersección misma es la prueba: cada validador que está en ambos conjuntos firmó dos votos que, juntos, violan la condición I o la II. Gasper formaliza esta idea como p-slashable: un estado es $(1/3)$-slashable si validadores con al menos un tercio del depósito pueden ser castigados de forma demostrable por alguien que observa la red. [2] Y sus autores subrayan que ser $(1/3)$-slashable es una garantía más fuerte que limitarse a suponer que menos de un tercio es bizantino. [2]

La prueba del paper sigue ese esquema. Suponiendo que menos de un tercio viola las reglas, dos enlaces de supermayoría distintos no pueden compartir altura de destino, y tampoco puede uno encerrar al otro; de ahí se deduce que existe a lo sumo un checkpoint justificado por altura. [1] Con eso, un checkpoint finalizado $a_m$ y otro en conflicto $b_n$ más alto obligan a que la cadena de justificaciones de $b_n$ contenga un enlace que salta desde antes de $a_m$ hasta después de su hijo $a_{m+1}$, lo que encierra el enlace de finalización $a_m \to a_{m+1}$ y viola la condición II. [1]

Plausible liveness y la regla de bifurcación

Safety sin progreso es trivial: un protocolo que nunca finaliza nada nunca se contradice. Por eso el paper prueba también plausible liveness: pase lo que pase antes, si al menos dos tercios siguen el protocolo, siempre es posible finalizar un checkpoint nuevo sin que ningún validador viole una condición de slashing. [1] La palabra "plausible" es honesta: el teorema dice que nadie queda acorralado, no que la finalización ocurra en un tiempo acotado.

La idea de la prueba es elegir bien el siguiente destino. Si $a$ es el checkpoint justificado más alto y $b$ el destino más alto por el que alguien votó, un descendiente de $a$ con altura $h(b) + 1$ puede justificarse sin violar ninguna regla, y luego finalizarse con un enlace hacia su hijo directo. [1]

De esa prueba sale la regla de bifurcación que propone el paper: seguir la cadena que contiene el checkpoint justificado de mayor altura. Los autores advierten que la regla "construir sobre la cadena más larga" puede dejar a Casper atascado, sin poder justificar nada salvo que algunos validadores sacrifiquen su depósito. [1] En otras palabras, el gadget no es completamente independiente de la capa de abajo: le exige una regla de bifurcación que respete lo ya justificado.

El paper también reconoce sus límites. Si más de un tercio deja de votar, no se forman enlaces de supermayoría y nada se finaliza; la propuesta para salir de ahí es un inactivity leak que drena gradualmente el depósito de quienes no votan. [1] Ese mecanismo tiene un precio: en una partición, cada lado puede recuperar la supermayoría en su propia cadena y finalizar checkpoints en conflicto sin que nadie viole una condición de slashing. [1]

Gasper: FFG sobre LMD GHOST

El paper original montaba Casper sobre la cadena de prueba de trabajo de Ethereum y anticipaba reemplazar ese mecanismo de propuesta por algo de prueba de participación. [1] Gasper es esa combinación: un protocolo que une Casper FFG como herramienta de finalidad con LMD GHOST como regla de bifurcación, presentado como una versión idealizada de la beacon chain que se proponía para Ethereum. [2]

Los cambios principales son tres:

1. Tiempo en slots y épocas. El tiempo se mide en slots y una época agrupa $C$ slots; el paper menciona valores tentativos de la especificación de entonces (12 segundos por slot y 64 slots por época), pero trata $C$ como parámetro. [2] Los checkpoints de FFG pasan a ser pares de frontera de época $(B, j)$, porque un mismo bloque puede hacer de frontera en más de una época cuando faltan bloques. [2]
2. Una attestation, dos votos. En cada slot, un comité vota por la cabeza de la cadena; esa attestation es a la vez un voto GHOST por un bloque y un voto FFG entre el último par justificado y el par de frontera actual. [2]
3. HLMD GHOST. La regla de bifurcación arranca desde el par justificado de época más alta y desde ahí desciende con LMD GHOST, eligiendo en cada bifurcación el hijo con más peso según el último voto de cada validador. [2] La parte FFG trabaja con información "congelada" al inicio de cada época, mientras la parte GHOST se actualiza con cada attestation. [2]

Las reglas de slashing se trasladan casi intactas: (S1) prohíbe dos attestations distintas en la misma época y (S2) prohíbe el voto envolvente sobre épocas de los pares fuente y destino. [2] Gasper demuestra que un validador honesto que sigue el protocolo nunca viola esas condiciones por accidente, y que si dos pares finalizados están en conflicto, la cadena es $(1/3)$-slashable. [2] Además, generaliza la finalización a $k$-finalización para absorber retrasos de attestations, aunque espera que casi siempre baste el caso $k = 1$, que coincide con la definición original de Casper. [2]

Con validadores que entran y salen, la garantía se debilita: si el protocolo rompe safety, se puede castigar de forma demostrable a algo menos de un tercio, siempre que el atacante no logre bifurcaciones muy largas. [2] Es la misma tensión que el paper de Casper ataca con el retardo de retiro y la regla de no revertir checkpoints finalizados frente a ataques de largo alcance. [1]

Siguiente lectura

La aritmética de un tercio que aparece aquí es la misma de Quórums en acción. Para comparar la noción de finalidad de Casper con la de un protocolo BFT de líder rotativo, sigue con Safety, liveness y responsiveness en HotStuff, y para otro gadget de finalidad montado sobre producción de bloques, con Substrate y la finalidad GRANDPA.