Verificando el Protocolo Starbridge con Ivy

El protocolo Starbridge es un protocolo para conectar Stellar y Ethereum. En otras palabras, permite a los usuarios intercambiar tokens nativos en una cadena por una versión envuelta de esos tokens en la otra cadena, y viceversa. Dado que Stellar aún no admite contratos inteligentes, diseñar el protocolo Starbridge plantea desafíos únicos. Hasta que Soroban esté completamente operativo en mainnet, no podemos depender de un contrato inteligente para procesar solicitudes de retiro en Stellar. En esta publicación de blog, explicamos cómo el protocolo Starbridge hace uso de las características existentes del protocolo Stellar para procesar retiros en Stellar, y cómo usamos el verificador Ivy para validar que esta parte del protocolo es segura.

Antes de comenzar, ten en cuenta que, para simplificar, omitimos o incluso omitimos por completo algunos detalles importantes. Nuestro objetivo no es ofrecer una referencia exhaustiva de Starbridge, sino explicar algunos aspectos interesantes del protocolo.

Para entender esta publicación de blog, necesitas estar familiarizado con las características básicas del protocolo Stellar (como emisores de tokens, cuentas multi-firma, números de secuencia y límites de tiempo de transacción). Si necesitas un repaso, dirígete a los Documentos de Stellar (notablemente, Operaciones y Transacciones y Emisión de Activos). Además, para una introducción al proyecto Starbridge en sí, vea esta publicación anterior del blog de SDF.

Un puente Starbridge consiste en un contrato inteligente en Ethereum, un conjunto de validadores de puente (que son servidores independientes en Internet, destinados a ser operados por un conjunto diverso de organizaciones confiables), y una cuenta multi-firma en Stellar, la cuenta del puente, que es controlada por los validadores del puente.

Cada token nativo de Ethereum admitido por el puente, por ejemplo ETH, tiene un token correspondiente en Stellar, por ejemplo wETH (donde wETH significa ETH envuelto), que es emitido por la cuenta del puente.

Para transferir 1 ETH de Ethereum a Stellar, un usuario procede como se muestra a continuación. (1), el usuario deposita su 1 ETH en el contrato inteligente del puente en Ethereum, que mantiene los fondos en custodia. Luego, (2) el usuario solicita a los validadores del puente una transacción de Stellar pre-firmada que acuña 1 wETH en Stellar y lo transfiere a la cuenta del usuario en Stellar. (3) Los validadores del puente verifican que el depósito del usuario es definitivo en Ethereum, y si es así, (4) devuelven la transacción pre-firmada solicitada al usuario. (5) Finalmente, el usuario ejecuta la transacción en Stellar, obteniendo 1 wETH como resultado.

En la otra dirección, un usuario puede intercambiar 1 wETH en Stellar por 1 ETH en Ethereum de la siguiente manera. Primero, el usuario quema 1 wETH (por ejemplo, enviándolo a una dirección bloqueada para siempre). Luego, el usuario solicita a los validadores del puente que firmen una declaración que los fondos han sido efectivamente quemados. Finalmente, el usuario llama al contrato inteligente de Starbridge en Ethereum, proporcionando la declaración como prueba de que pueden obtener legítimamente 1 ETH. El contrato inteligente de Starbridge luego deposita 1 ETH en la cuenta del usuario en Ethereum.

Usar transacciones pre-firmadas plantea un problema: una transacción de Stellar puede fallar por varias razones, por ejemplo, cuando el número de secuencia de la transacción no es igual al número de secuencia de la cuenta fuente más uno, o cuando la cuenta receptora no tiene una línea de confianza hacia la cuenta emisora. Por lo tanto, un usuario podría obtener una transacción pre-firmada de los validadores del puente pero, sin embargo, ser incapaz de retirar sus fondos en Stellar porque la transacción pre-firmada falla. Si eso sucediera, los fondos del usuario permanecerían atascados en el contrato del puente en Ethereum.

No queremos que los fondos de los usuarios queden atascados en el contrato inteligente del puente en Ethereum, y por lo tanto Starbridge permite a los usuarios solicitar nuevas transacciones de retiro pre-firmadas de los validadores del puente, incluso si ya han obtenido una para el mismo depósito, o solicitar un reembolso de su depósito de ETH en Ethereum.

Reemitir transacciones de retiro y reembolsar depósitos complica las cosas: Starbridge ahora tiene que asegurarse de que un depósito de ETH a) no pueda ser retirado como wETH dos veces y b) no pueda ser retirado como wETH en Stellar y reembolsado en Ethereum al mismo tiempo. El equipo de Starbridge ideó una manera sorprendentemente simple de admitir esas características usando el protocolo Stellar existente. Ahora explicamos cómo funciona a un alto nivel.

Considera a un usuario depositando 1 ETH en el contrato inteligente de Starbridge en Ethereum en el tiempo t0 (según lo dado por el timestamp del bloque de Ethereum en el que se ejecuta el depósito del usuario). Los validadores del puente consideran una solicitud de retiro válida entre el tiempo t0 y t0+Δ, llamado el período de retiro, donde Δ es un parámetro configurable que es acordado por todos los validadores del puente.

Durante el período de retiro, el usuario puede contactar a los validadores del puente y solicitar una transacción pre-firmada depositando 1 wETH en su cuenta en Stellar. Importante, esta transacción pre-firmada debe depositar la cantidad correcta de tokens wETH en la cuenta del usuario (aquí, 1 wETH), debe tener un max-time t<t0+Δ, y debe tener un número de secuencia igual a s+1, donde s es el número de secuencia más reciente de la cuenta del usuario según los validadores de Starbridge. (Nota que, debido al retraso de la red, no podemos garantizar que los validadores de Starbridge conocerán sobre el último ledger externalizado en Stellar; como veremos a continuación, esto no compromete la seguridad de Starbridge.)

Como explicamos antes, la transacción pre-firmada devuelta por los validadores de Starbridge podría fallar una vez enviada a Stellar. Esto no es un problema, porque el usuario puede solicitar una nueva transacción pre-firmada tantas veces como quiera. Sin embargo, las mismas restricciones aplican al max-time y número de secuencia de la transacción.

Por ejemplo, si la primera transacción pre-firmada tiene el número de secuencia 2 (lo cual estaría bien si la cuenta del usuario tiene el número de secuencia 1), pero, para cuando el usuario la envía a Stellar, el número de secuencia de su cuenta aumenta a 2 y la transacción falla, el usuario puede solicitar una nueva transacción pre-firmada con el número de secuencia 3. Asumiendo que los validadores de Starbridge recibieron el último ledger externalizado (en el que la cuenta del usuario tiene el número de secuencia 2), pre-firmarán la transacción con el número de secuencia 3, la cual el usuario puede enviar a Stellar para obtener su 1 wETH. Este escenario de ejemplo se muestra a continuación.

‍

Después de que el período de retiro ha terminado (es decir, cuando un ledger de Stellar con tiempo de cierre tc>t0+Δ es externalizado), todas las transacciones pre-firmadas solicitadas por el usuario se vuelven inválidas porque su max-time es igual a t0+Δ. En este punto, los validadores de Starbridge comienzan a otorgar solicitudes de reembolso al usuario devolviendo, a petición del usuario, un mensaje firmado atestiguando que están de acuerdo con el reembolso. El usuario puede entonces llamar al contrato inteligente del puente en Ethereum, proporcionando las solicitudes de reembolso firmadas como prueba de que el reembolso es legítimo. El contrato inteligente verifica las firmas y, si son válidas, deposita 1 ETH de nuevo en la cuenta del usuario. Crucialmente, los validadores del puente solo firman una solicitud de reembolso si el último ledger externalizado que conocen tiene un tiempo de cierre mayor que el final del período de retiro y ningún retiro correspondiente fue ejecutado por el usuario en ningún ledger pasado.

Hay algunas cosas interesantes a notar sobre este proceso:

• Los validadores de Starbridge no necesitan sincronizarse entre sí (solo necesitan estar de acuerdo en Δ): procesan las solicitudes de los usuarios independientemente de los demás.
• Los validadores de Starbridge deben ingerir ledgers de Stellar y bloques de Ethereum, pero podrían, temporalmente, no saber sobre el último ledger cerrado por Stellar o el último bloque producido por Ethereum. Esto podría causar que las solicitudes de los usuarios y los retiros fallen temporalmente, pero no comprometerá la seguridad del puente.
• Los validadores de Starbridge incluso pueden fallar y reiniciar desde un estado en blanco (por ejemplo, porque su disco duro falló y fue reemplazado), e inmediatamente comenzar a procesar nuevas solicitudes de retiro sin tener que preocuparse por lo que firmaron antes de fallar. En otras palabras, los validadores del puente son casi sin estado, necesitando solo recordar sus claves; el resto siempre puede ser reconstruido a partir del estado de la cadena de Stellar y Ethereum.

Ahora, una pregunta importante es: ¿cómo estamos seguros de que no hay una manera ingeniosa para que un usuario malicioso subvierta el protocolo y retire su wETH dos veces? ¿O que retire su wETH y también obtenga un reembolso en Ethereum? En otras palabras, ¿cómo estamos seguros de que un usuario ingenioso no puede robar del puente?

Intuitivamente, a) la clara separación entre el período de retiro y el período de reembolso debería prevenir que un depósito de ETH sea retirado en Stellar como wETH y también reembolsado en Ethereum, y b), los retiros dobles deberían ser prevenidos por el hecho de que los validadores del puente solo firman transacciones de retiro cuyo número de secuencia corresponde al último número de secuencia de la cuenta del usuario del que los validadores del puente han tenido noticia.

Sin embargo, es notoriamente fácil pasar por alto un caso límite y convencerse de que un algoritmo distribuido incorrecto es correcto. Por ejemplo, el famoso algoritmo Chord (que implementa una tabla hash distribuida) fue encontrado incorrecto más de 10 años después de su publicación; para ese momento, se había convertido en uno de los trabajos más citados en ciencias de la computación, pero nadie notó el error. Hay muchos otros ejemplos como este.

Dado que una implementación de Starbridge puede tener que asegurar millones de dólares en valor, nos gustaría asegurarnos de que no pasamos por alto ningún caso límite y que el protocolo realmente hace imposible robar fondos del puente. Para este propósito, creamos un modelo formal del protocolo y lo verificamos usando el verificador Ivy.

Una cosa importante a notar es que no verificamos la implementación de Starbridge (es decir, el código escrito en Go y Solidity). En su lugar, desarrollamos por separado un modelo del código, en el lenguaje Ivy, y verificamos ese modelo. Esto nos permite verificar que no hay errores de diseño en las partes del protocolo que modelamos, pero no excluye errores de implementación.

En el resto de la publicación del blog, repasaremos brevemente el modelo y la prueba de seguridad, que están disponibles en la carpeta docs/modelo-formal del repositorio de Starbridge.

Podemos pensar en el modelo como un programa, escrito en el lenguaje Ivy, que simula la transferencia de tokens de Ethereum a Stellar. Para simplificar, modelamos una única transferencia de Ethereum a Stellar, y asumimos que hay un único validador del puente.

Para escribir un modelo en Ivy, creamos variables que representan el estado de las diferentes partes en el protocolo, especificamos su estado inicial, y describimos cuáles son las posibles acciones que las partes pueden tomar. Cada acción consiste en precondiciones (palabra clave require) seguidas por un pequeño fragmento de código que actualiza el estado de la simulación en un paso atómico.

Por ejemplo, la variable bridge_ledger_time representa el tiempo de cierre del último libro contable visto por el validador del puente, la variable executed(t, tx) es una función booleana que indica si la transacción t se ejecutó en el libro contable que cerró en el tiempo t, y refunded es un booleano que indica si el validador del puente firmó una solicitud de reembolso.

Dadas esas variables de estado, la siguiente acción modela al validador del puente firmando una solicitud de reembolso:

1 acción reembolso = {
2 require bridge_ledger_time > end_withdraw_period;
3 require forall T,TX . T <= bridge_ledger_time
4 -> ~executed(T, TX);
5 refunded := true;
6 }

La línea 2 dice que el tiempo de cierre del último libro contable conocido por el validador del puente debe ser estrictamente mayor que el final del período de retiro (en otras palabras, el período de retiro ha terminado). La línea 3 dice que ninguna transacción de retiro fue ejecutada para cuando el período de retiro terminó (nota que ~ significa negación en Ivy). Finalmente, la línea 4, la refunded variable se actualiza a true para significar que el validador del puente firmó la solicitud de reembolso.

Especificamos las otras posibles acciones de manera similar. Por ejemplo, a continuación está la acción correspondiente a la firma del puente de una solicitud de retiro (nota que succ es la relación sucesora en números de secuencia). Esta acción hace uso de una nueva variable, pending(tx), que indica si la transacción tx ha sido firmada por el validador del puente y está lista para ser ejecutada en Stellar.

1 acción sign_withdraw(tx:withdraw_t) = {
2 require T <= bridge_ledger_time -> ~executed(T, TX);
3 require tx.max_time <= end_withdraw_period;
4 require tx.seqnum <= bridge_receiving_seqnu
| seqnum_t.succ(bridge_receiving_seqnum, tx.seqnum);
5 pending(tx) := true;
6 }

Las otras acciones en el modelo son new_ledger, que modela la red de Stellar cerrando un nuevo libro contable, process_ledgers, que modela al validador del puente aprendiendo sobre nuevos libros contables cerrados de Stellar, y restart, que modela al validador del puente reiniciando desde un estado en blanco.

Ahora podemos expresar que el puente es seguro usando las siguientes dos propiedades de corrección:

1 invariante forall T,TX . ~(refunded & exists T, TX. executed(T,TX))
2 invariante forall T1,TX1,T2,TX2 .
3 executed(T1, TX1) & executed(T2, TX2)
4 -> T1 = T2 & TX1 = TX2

En la línea 1, afirmamos que no es posible que el depósito del usuario haya sido tanto reembolsado en Ethereum como retirado en Stellar. En la línea 2, afirmamos que como máximo una transacción de retiro puede ser ejecutada. Juntas, esas dos propiedades implican que un usuario nunca puede gastar doblemente, sin importar cuántas transacciones de retiro soliciten y sin importar el momento de sus acciones.

Ahora que tenemos nuestro modelo y las propiedades que queremos verificar en mano, ¿cómo verificamos realmente que las propiedades se mantienen? Podríamos pedirle a Ivy que enumere las posibles secuencias de acciones que pueden ocurrir y verificar que las propiedades de corrección siempre se satisfacen. Desafortunadamente, hay un número infinito de combinaciones de acciones (eso es porque, por ejemplo, los números de secuencia son ilimitados en el modelo, y la duración del período de retiro es arbitraria). Podríamos considerar solo un conjunto fijo de números de secuencia (por ejemplo, 1, 2 y 3), y un período de retiro de longitud fija (por ejemplo, 42), etc., para obtener un conjunto finito de casos, y luego verificar que no ocurre un doble gasto dentro de esos límites enumerando todas las posibles secuencias de acciones. Sin embargo, no sabríamos si nos perdimos un problema que ocurre solo con al menos 4 números de secuencia, por ejemplo.

En cambio, Ivy nos permite verificar que no puede ocurrir un doble gasto en ningún caso posible, incluso si hay infinitamente muchos. Pero para eso, necesitamos ayudar a Ivy proporcionando un invariante inductivo. Un invariante inductivo es un predicado de estado P tal que a) P se mantiene en el estado inicial, y b) si P se mantiene y ejecutamos una acción arbitraria, entonces P se mantiene de nuevo. Juntos, a) y b) implican que P se mantendrá para siempre, independientemente de las acciones tomadas y de su orden.

Proporcionar un invariante inductivo hace el trabajo de Ivy mucho más simple: en lugar de tener que considerar secuencias de acciones largas y complicadas, Ivy ahora solo tiene que verificar las propiedades a) y b), lo que solo requiere razonar sobre un único paso del protocolo a la vez. En este caso, Ivy es capaz de verificar esto automáticamente para nosotros.

El archivo starbridge.ivy contiene una lista de invariantes que juntos forman un invariante inductivo e implican las propiedades de corrección.

¿Quieres profundizar más? El modelo y prueba de Ivy están disponibles en el repositorio de Starbridge, junto con una configuración de Docker que facilita la ejecución de Ivy.

‍