Haciendo Stellar

Haciendo la comunidad de Stellar Network más grande de hablahispana

Haciendo la comunidad de Stellar Network
más grande de hablahispana

Verificación del Protocolo Starbridge con Ivy

1 de noviembre de 2022

‍Introducción

El protocolo Starbridge es un protocolo que sirve de puente entre 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, el diseño del protocolo Starbridge plantea retos únicos. Hasta que Soroban esté completamente disponible en la mainnet, no podemos confiar en un contrato inteligente para procesar las solicitudes de retiro en Stellar. En este blog, explicamos cómo el protocolo Starbridge hace uso de las características existentes del protocolo Stellar para procesar la retirada en Stellar, y cómo utilizamos el verificador Ivy para validar que esta parte del protocolo es segura. 

Antes de empezar, hay que tener en cuenta que, para simplificar las cosas, pasamos por alto o incluso omitimos completamente algunos detalles importantes. Nuestro objetivo no es ofrecer una referencia completa de Starbridge, sino explicar algunos aspectos interesantes del protocolo. 

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

La anatomía de una transferencia simple 

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

Cada token nativo de Ethereum soportado 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 indica a continuación. (1), el usuario deposita su 1 ETH en el contrato inteligente puente en Ethereum, que mantiene los fondos en custodia. A continuación, (2) el usuario solicita a los validadores del puente una transacción pre-firmada en Stellar que acuñe 1 wETH en Stellar y lo transfiera a la cuenta del usuario en Stellar. (3) Los validadores del puente comprueban que el depósito del usuario es definitivo en Ethereum, y si es así, (4) devuelven al usuario la transacción solicitada y pre-firmada. (5) Finalmente, el usuario ejecuta la transacción en Stellar, obteniendo como resultado 1 wETH.

En el otro sentido, 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). A continuación, el usuario pide a los validadores del puente que firmen un certificado de que los fondos han sido efectivamente quemados. Por último, el usuario llama al contrato inteligente Starbridge en Ethereum, proporcionando el certificado como prueba de que puede obtener legítimamente 1 ETH. El contrato inteligente Starbridge deposita entonces 1 ETH en la cuenta del usuario en Ethereum.

El problema de las transacciones prefirmadas

El uso de transacciones prefirmadas plantea un problema: una transacción de Stellar puede fallar por diversas razones, por ejemplo, cuando el número de secuencia de la transacción no es igual al número de secuencia de la cuenta de origen más uno, o cuando la cuenta receptora no tiene una línea de confianza con la cuenta emisora. Así, un usuario podría obtener una transacción pre-firmada de los validadores del puente y, sin embargo, no poder retirar sus fondos en Stellar porque la transacción pre-firmada falla. Si esto ocurriera, los fondos del usuario quedarían atrapados en el contrato puente en Ethereum. 

No queremos que los fondos de los usuarios se queden atascados en el contrato inteligente del puente en Ethereum, y por ello Starbridge permite a los usuarios solicitar nuevas transacciones de retirada 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.

La reemisión de las transacciones de retirada y el reembolso de los 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. El equipo de Starbridge ha ideado una forma sorprendentemente sencilla de soportar estas características utilizando el protocolo existente de Stellar. A continuación explicamos cómo funciona a alto nivel.

Reemitir la operación de retirada y permitir devoluciones

Consideremos un usuario que deposita 1 ETH en el contrato inteligente Starbridge en Ethereum en el momento t0 (dado por la marca de tiempo del bloque de Ethereum en el que se ejecuta el depósito del usuario). Los validadores del puente consideran una solicitud de retirada válida entre el tiempo t0 y t0+Δ, llamado período de retirada, donde Δ es un parámetro configurable que es acordado por todos los validadores del puente.

Durante el periodo de retirada, el usuario puede ponerse en contacto con los validadores del puente y solicitar una transacción pre-firmada que deposite 1 wETH en su cuenta en Stellar. Es importante que esta transacción pre-firmada deposite la cantidad correcta de tokens wETH en la cuenta del usuario (en este caso, 1 wETH), que tenga un tiempo máximo t<t0+Δ, y que tenga 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. (Nótese que, debido al retraso de la red, no podemos garantizar que los validadores de Starbridge conozcan el ledger más reciente externalizado en Stellar; como veremos más adelante, esto compromete la seguridad de Starbridge). 

Como hemos explicado antes, la transacción pre-firmada devuelta por los validadores de Starbridge puede 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, se aplican las mismas restricciones que las anteriores en cuanto al tiempo máximo y el 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 que 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. Suponiendo que los validadores de Starbridge hayan recibido 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, que el usuario puede enviar a Stellar para obtener su 1 wETH. Este escenario de ejemplo se representa a continuación.

After the withdrawal period has ended (i.e. when a Stellar ledger with close time tc>t0+Δ is externalized), all pre-signed transactions requested by the user become invalid because their max-time is equal to t0+Δ. At this point, Starbridge validators start granting refund requests to the user by returning, at the user’s request, a signed message attesting that they agree to the refund. The user can then call the bridge smart contract on Ethereum, providing the signed refund requests as proof that the refund is legitimate. The smart-contract checks the signatures and, if they are valid, deposits 1 ETH back into the user’s account. Crucially, the bridge validators only sign a refund request if the last externalized ledger they know of has a close time greater than the end of the withdrawal period and no corresponding withdrawal was executed by the user in any past ledger. 

Una vez finalizado el periodo de reintegro (es decir, cuando se externaliza un ledger de Stellar con tiempo de cierre tc>t0+Δ), todas las transacciones pre-firmadas solicitadas por el usuario pasan a ser inválidas porque su tiempo máximo es igual a t0+Δ. En este punto, los validadores de Starbridge comienzan a conceder solicitudes de reembolso al usuario devolviendo, a petición de éste, un mensaje firmado que atestigua que está de acuerdo con el reembolso. El usuario puede entonces llamar al contrato inteligente de puente en Ethereum, proporcionando las solicitudes de reembolso firmadas como prueba de que el reembolso es legítimo. El contrato inteligente comprueba las firmas y, si son válidas, deposita 1 ETH en la cuenta del usuario. Es fundamental que los validadores del puente sólo firmen una solicitud de reembolso si el último ledger externalizado que conocen tiene una hora de cierre mayor que el final del periodo de retirada y no se ha ejecutado ninguna retirada correspondiente por parte del usuario en ningún ledger anterior.

Hay algunas cosas interesantes que señalar sobre este proceso: 

  • Los validadores de Starbridge no necesitan sincronizarse entre sí (sólo tienen que ponerse de acuerdo en Δ): procesan las solicitudes de los usuarios de forma independiente.
  • Los validadores de Starbridge deben ingerir los ledgers de Stellar y los bloques de Ethereum, pero podrían, temporalmente, no conocer el último ledger cerrado por Stellar o el último bloque producido por Ethereum. Esto puede hacer que las peticiones y retiradas de los usuarios fallen temporalmente, pero no comprometerá la seguridad del puente. 
  • Los validadores de Starbridge pueden incluso bloquearse y reiniciarse desde un estado en blanco (por ejemplo, porque su disco duro ha fallado y ha sido sustituido), e inmediatamente empezar a procesar nuevas solicitudes de retirada sin tener que preocuparse por lo que firmaron antes de bloquearse. En otras palabras, los validadores del puente son casi apátridas, ya que sólo necesitan recordar sus claves; el resto puede reconstruirse siempre a partir del estado de la cadena de Stellar y Ethereum.

¿Es seguro el protocolo Starbridge?

Ahora, una pregunta importante es: ¿cómo estamos seguros de que no hay una forma inteligente para que un usuario malicioso subvierta el protocolo y retire su wETH dos veces? ¿O de retirar su wETH y obtener un reembolso en Ethereum? En otras palabras, ¿cómo estamos seguros de que un usuario inteligente no puede robar del puente? 

Intuitivamente, a) la clara separación entre el periodo de retirada y el periodo de reembolso debería impedir que un depósito de ETH se retire en Stellar como wETH y también se reembolse en Ethereum, y b), las dobles retiradas deberían evitarse por el hecho de que los validadores del puente sólo firman las transacciones de retirada 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 conocimiento. 

Sin embargo, es notoriamente fácil pasar por alto un caso de esquina y convencerse de que un algoritmo distribuido incorrecto es correcto. Por ejemplo, se descubrió que el famoso algoritmo Chord (que implementa una tabla hash distribuida) era incorrecto más de 10 años después de su publicación; para entonces, se había convertido en uno de los trabajos más citados de la informática, pero nadie se dio cuenta del error. Hay muchos otros ejemplos como éste. 

Dado que un despliegue 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 de esquina y que el protocolo realmente hace imposible robar fondos del puente. Para ello, creamos un modelo formal del protocolo y lo verificamos con el verificador Ivy

Una cosa importante a tener en cuenta 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 los errores de implementación.

Modelar con Ivy 

En el resto del blog, repasaremos brevemente el modelo y la prueba de seguridad, que están disponibles en la carpeta docs/formal-model 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 realizar. Cada acción consiste en condiciones previas (palabra clave require) seguidas de un pequeño trozo de código que actualiza el estado de la simulación en un paso atómico.

Por ejemplo, la variable bridge_ledger_time representa la hora de cierre del último ledger visto por el validador del puente, la variable executed(t, tx) es una función booleana que indica si la transacción t se ha ejecutado en el libro mayor que cerró a la hora 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 el validador del puente firmando una solicitud de reembolso: 

1 action refund = {

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 la hora de cierre del último ledger conocido por el validador del puente debe ser estrictamente mayor que el final del periodo de retirada (en otras palabras, el periodo de retirada ha terminado). La línea 3 dice que no se ha ejecutado ninguna operación de retirada en el momento en que ha finalizado el periodo de retirada (nótese que ~ significa negación en Ivy). Por último, en la línea 4, la variable refunded se actualiza a true para significar que el validador del puente firmó la solicitud de reembolso. 

Las demás acciones posibles se especifican de forma similar. Por ejemplo, a continuación se muestra la acción correspondiente al puente que firma una solicitud de retirada (nótese que succ es la relación de sucesión en los 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 action 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 del modelo son new_ledger, que modela la red Stellar cerrando un nuevo ledger, process_ledgers, que modela el validador del puente aprendiendo sobre nuevos ledgers de Stellar cerrados, y restart, que modela el validador del puente reiniciando desde un estado en blanco. 

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

1 invariant forall T,TX . ~(refunded & exists T, TX. executed(T,TX))

2 invariant forall T1,TX1,T2,TX2 . 

3     executed(T1, TX1) & executed(T2, TX2)

4         -> T1 = T2 & TX1 = TX2

Línea 1, afirmamos que no es posible que el depósito del usuario haya sido reembolsado en Ethereum y retirado en Stellar. Línea 2, afirmamos que como máximo se puede ejecutar una transacción de retirada. Juntas, estas dos propiedades implican que un usuario nunca puede gastar dos veces, independientemente del número de transacciones de retirada que solicite e independientemente del momento en que realice sus acciones.

Verificación 

Ahora que tenemos a mano nuestro modelo y las propiedades que queremos comprobar, ¿cómo verificamos realmente que las propiedades se cumplen? Podríamos pedirle a Ivy que enumere las posibles secuencias de acciones que pueden ocurrir y comprobar que las propiedades de corrección se satisfacen siempre. Desgraciadamente, hay un número infinito de combinaciones de acciones (esto se debe, por ejemplo, a que los números de las secuencias no están limitados en el modelo, y la duración del periodo de retirada es arbitraria). Podríamos considerar sólo un conjunto fijo de números de secuencia (por ejemplo, 1, 2 y 3), y un período de retirada de duración fija (por ejemplo, 42), etc., para obtener un conjunto finito de casos, y luego comprobar que no se produce ningún gasto doble dentro de esos límites enumerando todas las posibles secuencias de acciones. Sin embargo, no sabríamos si se nos escapa un problema que sólo se produce con al menos 4 números de secuencia, por ejemplo. 

En cambio, Ivy nos permite verificar que no puede haber ningún gasto doble en ningún caso posible, aunque haya infinitos. Pero para ello, necesitamos ayudar a Ivy proporcionando un invariante inductivo. Un invariante inductivo es un predicado de estado P tal que a) P se cumple en el estado inicial, y b) si P se cumple y ejecutamos una acción arbitraria, entonces P se vuelve a cumplir. Juntos, a) y b) implican que P se mantendrá siempre, independientemente de las acciones que se realicen y de su orden. 

Proporcionar un invariante inductivo hace que el trabajo de Ivy sea mucho más sencillo: en lugar de tener que considerar largas e intrincadas secuencias arbitrarias de acciones, Ivy ahora sólo tiene que comprobar las propiedades a) y b), lo que sólo requiere razonar sobre un único paso del protocolo cada vez. En este caso, Ivy es capaz de comprobar esto automáticamente por 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? El modelo y la 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.