En junio de 2016, había mucho entusiasmo porque “The DAO”, construido sobre la cadena de bloques Ethereum, estaba a punto de convertirse en el primer fondo de inversión descentralizado y totalmente digital del mundo.
Pero en cuestión de semanas, se convirtió en el modelo de los hacks de DeFi después de que los atacantes le robaron 50 millones de dólares en éter.
Para descifrar The DAO, el atacante aprovechó la llamada vulnerabilidad de reentrada, una vulnerabilidad de concurrencia en la que se llama a un método de un contrato inteligente específico mientras otro método aún se está ejecutando, y The DAO es solo una parte del desarrollo a largo plazo del contrato inteligente. El primero sufre tales errores.
Los sucesores destacados incluyen Uniswap/Lendf.Me, a quien le robaron 25 millones de dólares en 2020, CREAM, a quien le robaron 18 millones de dólares en 2021, y Fei, a quien le robaron 80 millones de dólares en 2022.
La razón por la que estos errores persisten es que pueden implicar interacciones de código inesperadas repartidas por todo el contrato inteligente, a veces incluso en contratos inteligentes completamente diferentes. La cantidad de dichas interacciones de código puede ser muy grande, lo que dificulta que los humanos detecten y eliminen contratos inteligentes no deseados. código requerido.
Además, estas interacciones suelen ser difíciles de probar de forma automática y sistemática.
TLA+: El Exterminador
Ingrese a la Lógica Temporal de Acciones (TLA+), un lenguaje para especificar y validar sistemas complejos. TLA+ no solo encuentra errores sino que también verifica su existencia.
¿Cómo es esto posible?, te preguntarás. TLA+ viene con un conjunto de herramientas para una verificación formal ligera en forma de la llamada verificación de modelo. A través de la verificación del modelo, explora exhaustivamente todas las posibles interacciones simultáneas del modelo de código (las mismas áreas que son difíciles de probar) y encuentra errores.
Imagine un exterminador que ilumina cada rincón para exponer y eliminar plagas no deseadas que se esconden en esos rincones oscuros que a menudo se pasan por alto o se ignoran. Es importante destacar que una vez creado el modelo de código, la verificación del modelo casi no requiere intervención humana para su ejecución, lo que la hace muy rentable.
Para ilustrarlo con algunos números inventados: si las prácticas estándar de la industria, como las pruebas y las revisiones de seguridad, eliminan el 80% de los errores, y la verificación formal "pesada" elimina el 99%, el uso de TLA+ elimina el 90% con solo una pequeña cantidad de esfuerzos de verificación pesados.
TLA+ e Internet Computadoras
Nuestro equipo de ingeniería utiliza TLA+ para analizar todos los aspectos de la informática de Internet, incluidos los contratos inteligentes críticos para la seguridad que se ejecutan en la plataforma. Aunque Ethereum y las computadoras de Internet tienen diferentes modelos de ejecución, pueden aparecer errores de reentrada en contratos inteligentes en ambas cadenas de bloques.
De hecho, debido a su alto rendimiento, las computadoras de Internet permiten múltiples llamadas simultáneas a un único contrato inteligente, lo que requiere que los autores de contratos inteligentes tengan más cuidado para eliminar interacciones simultáneas no deseadas. Dado que la seguridad es fundamental para el éxito de las computadoras en Internet, TLA+ se utiliza en muchos contratos inteligentes para detectar errores durante la fase de desarrollo.
Recientemente se realizó un contenedor de análisis TLA+ (contratos inteligentes para computadoras en Internet) en el recientemente lanzado Chain-Key Bitcoin (ckBTC), cuyos resultados compartiré a continuación.
contrato inteligente ckBTC
Para hablar sobre el análisis TLA+ de ckBTC, comencemos con una descripción general de alto nivel de ckBTC. ckBTC es un token nativo de computadora de Internet respaldado de forma segura por Bitcoin (BTC) en una proporción de 1:1.
El libro mayor de ckBTC es un contrato inteligente de contenedor en la cadena de bloques informática de Internet que rastrea cuánto ckBTC posee cada usuario final. Este mismo libro de contabilidad permite a los usuarios finales transferir su ckBTC a otros usuarios finales de forma más rápida y económica que transferir BTC en la red Bitcoin.
Para convertir ckBTC a BTC y viceversa, los usuarios finales interactúan con un contrato inteligente diferente, el ckBTC minter.
En un nivel alto, la operación de conversión de BTC a ckBTC se ve así:
Pasos para obtener ckBTC:
1. El usuario final primero transfiere algunos BTC a una dirección de depósito de Bitcoin específica del usuario, todas las direcciones de depósito están completamente controladas por el código del contenedor inteligente ckBTC minter debido a la firma ECDSA de la clave de cadena, que crea un nuevo UTXO propiedad del depósito. DIRECCIÓN;
2. El usuario final notifica al contrato inteligente ckBTC mint sobre el UTXO recién depositado solicitando a la menta que actualice el saldo del usuario;
3. Luego, el contrato inteligente de minter utiliza la integración de Bitcoin de las computadoras de Internet para recuperar todos los UTXO propiedad de la dirección de depósito controlada por minter pero específica del usuario. Luego, el minter selecciona nuevos UTXO de la red de Bitcoin enviándoles verificaciones cruzadas. su lista de contabilidad interna de UTXO que ha procesado;
4. Finalmente, el minter le indica al libro mayor que acuñe nuevos ckBTC para todos los UTXO nuevos en una proporción de 1:1 y, una vez completado, agrega los UTXO recién descubiertos a la lista de UTXO procesados.
Descargo de responsabilidad: El proceso anterior omite el proceso KYT (Conozca su transacción) por simplicidad.
El contrato inteligente de ckBTC se encuentra con TLA+
La imagen de alto nivel presentada arriba en realidad oculta un problema sutil de concurrencia, y la buena noticia es que podemos detectar el problema utilizando el kit de herramientas TLA+.
Pero antes de que TLA+ pueda detectar algo, primero debemos proporcionarle dos cosas:
Crear un modelo de nuestro sistema usando el lenguaje TLA+
Especificar las propiedades de TLA+ que esperamos que implemente el sistema.
Este modelo es una versión simplificada pero aún completamente definida del sistema, que en nuestro caso incluye el contrato inteligente minter, pero también todas las demás partes relevantes del sistema, es decir, el contrato contable y la red Bitcoin.
Para cada componente, modelamos su estado y cómo las acciones relevantes que un usuario final podría realizar (es decir, transferir BTC o ckBTC, depositar BTC o realizar diferentes acciones expuestas por el minter) cambian el estado.
Todos estos elementos están algo simplificados en el modelo, con partes en las que se centra el análisis (por ejemplo, el código minter) modeladas con más detalle, mientras que otras partes (por ejemplo, la red Bitcoin) se modelan con menos detalle; de hecho, un modelo TLA+ Es similar a una especificación de diseño detallada de un sistema.
Intuitivamente, la característica principal que queremos implementar es garantizar que nuestro ckBTC sea totalmente compatible. En otras palabras, ningún usuario final debería poder “gastar dos veces” su BTC depositado para obtener más ckBTC del que depositó.
Pero para analizar tal propiedad, tenemos que hacer que esta intuición sea muy precisa expresándola formalmente en el lenguaje TLA+. Nuestra definición formal es que el suministro total de ckBTC (es decir, la suma de todos los saldos de ckBTC del usuario final, tal como se almacena en el libro mayor de ckBTC) no excede la cantidad total de BTC controlada por el contenedor de acuñación (es decir, el valor de todos UTXO propiedad de una dirección de depósito).
Detectar y resolver problemas
Una vez que hayamos creado el modelo y las propiedades, el kit de herramientas TLA+ puede analizar el modelo. Para ejecutar el análisis, primero definimos la configuración para ejecutar el análisis. Por ejemplo, nuestra configuración para ckBTC solo incluye dos usuarios finales diferentes y una pequeña cantidad del suministro total de Bitcoin (por ejemplo, 5 satoshis).
Aunque este escenario es muy limitado, los estudios empíricos muestran que la gran mayoría de los problemas en los sistemas informáticos se pueden encontrar en un pequeño número de entidades. La pequeña configuración permite que el análisis explore sistemáticamente todas las posibles secuencias de acción definidas por el modelo y verifique si las propiedades prescritas se mantienen en dicha secuencia.
Además, el análisis se ejecuta de forma completamente automática, es decir, no requiere ninguna intervención humana y, si estas propiedades no se cumplen, nos proporciona la secuencia exacta de operaciones que viola esa propiedad.
Por ejemplo, el análisis puede revelar que podemos violar nuestra propiedad "no ckBTC no seguro" en un escenario como el que se muestra a continuación:
aquí:
Los usuarios finales depositan BTC, igual que antes;
Sin embargo, ahora el usuario final le indica al minter ckBTC que actualice el saldo dos veces en rápida sucesión, y en una computadora con Internet estas actualizaciones pueden interactuar con otros contratos inteligentes simultáneamente;
Dos actualizaciones que se ejecutan simultáneamente solicitan a la red Bitcoin todos los UTXO depositados por el usuario final, y ambas reciben en respuesta el mismo UTXO depositado en el paso 1. Dado que el UTXO aún no está en la lista de "procesados", ambas actualizaciones piensan que el UTXO es nuevo;
Ambas actualizaciones indican al libro mayor que acuñe la cantidad correspondiente de ckBTC en el paso 4.
Por lo tanto, al final del paso 4, estamos en un estado donde el suministro de ckBTC es el doble de la suma de los UTXO en las direcciones de depósito, lo que viola nuestra propiedad de "no ckBTC sin soporte".
Tenga en cuenta que este error solo ocurre porque las actualizaciones del saldo del usuario final se ejecutan simultáneamente; en realidad, es un error reentrante del mismo estilo que el que derribó The DAO.
Una forma de resolver este problema es evitar que las actualizaciones de saldo se ejecuten en paralelo para el mismo usuario final. Podemos hacer esto haciendo que Minter almacene al usuario final en una lista de usuarios "bloqueados" cuando comienza la actualización de saldo y los mantenga allí. durante la duración de la lista de actualización para lograr esto.
Si el usuario final intenta iniciar otra actualización de saldo simultánea, la actualización primero verificará y encontrará a este usuario final específico en la lista de usuarios bloqueados y luego cancelará.
Tenga en cuenta que aquí estamos simplificando ligeramente el ataque: el bloqueo es en realidad un patrón bastante común para los contratos inteligentes de IC, y los acuñadores de ckBTC lo han implementado desde el principio. Sin embargo, el bloqueo ejecutado incorrectamente abre la puerta a los ataques anteriores, que TLA+ es capaz de detectar.
Además, encontramos algunos casos extremos que violaban "no ckBTC no compatible" y otras propiedades importantes, y una vez que aplicamos todas las correcciones, TLA+ pudo verificar y confirmar que no había más violaciones de propiedad en nuestra configuración definida.
¿Debería utilizar TLA+ para sus contratos inteligentes?
¡Absolutamente! Vale, vale, tal vez debería dar una respuesta más matizada, que nuestro equipo de I+D utiliza para contratos inteligentes críticos en ordenadores de Internet siempre que se trate de una concurrencia no trivial.
Por ejemplo, el análisis de TLA+ descubrió errores sutiles de concurrencia en Internet Computer Governance y Ledger Containers que se pasaron por alto en revisiones de seguridad manuales anteriores y que podrían haber dado lugar a problemas, casos y puntos importantes: TLA+ al descubrir problemas tan espinosos fue una auténtica maravilla.
Por supuesto, hay un precio que pagar en términos de adquirir el conocimiento y luego construir el modelo, pero empíricamente el precio es razonable, especialmente dada la naturaleza de alto riesgo de la seguridad de blockchain.
Uno no debe dejarse intimidar por el lenguaje TLA+ en sí; a pesar del nombre intimidante, acceder a sus potentes funciones es bastante sencillo. De hecho, una hoja de trucos de TLA+ que describa casi todas las características de TLA+ podría caber aproximadamente en una página:
mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
Es más, el esfuerzo necesario para construir el modelo es comparable a las revisiones de seguridad manuales estándar. Por ejemplo, para una máquina de acuñar ckBTC, una persona tardaría un total de aproximadamente 3 semanas en comprender el diseño, crear el modelo inicial y las propiedades.
El modelo TLA+ resultante es mucho más simple que la implementación, tanto porque es más simple que el código como por la naturaleza de alto nivel de TLA+. El modelo para el minter ckBTC requiere alrededor de 250 líneas de código en comparación con las miles de líneas de implementación de Rust. Quizás sea sorprendente que una de las partes más difíciles en términos de esfuerzo sea especificar las propiedades requeridas, ya que a menudo uno encuentra lagunas en las especificaciones intuitivas.
Una vez que se completa el modelo, el análisis (verificación del modelo) se completa automáticamente. El análisis puede tardar mucho en ejecutarse; por ejemplo, para ckBTC, tardó más de 20 horas en completarse. Finalmente, otro beneficio de TLA es que el modelado y el análisis se pueden realizar en la fase de diseño antes de implementar el código, lo que ayuda a eliminar grandes refactorizaciones debido a errores de diseño posteriores.
Donde TLA+ es inútil
En el lado negativo, TLA+ es menos útil para programas secuenciales complejos, a diferencia de programas concurrentes, y tampoco es bueno para manejar protocolos criptográficos complejos, para los cuales existen otras herramientas (por ejemplo, Tamarin) que son más útiles.
Finalmente, está la cuestión de mantener sincronizados el modelo TLA+ y la implementación real, ya que a medida que el código de implementación evoluciona con el tiempo, es posible que ya no se ajuste al modelo, lo que puede ser difícil de detectar sin soporte de herramientas.
De hecho, nuestro equipo de I+D está intentando resolver este problema. ¡Espero que podamos compartir algunas herramientas con usted pronto!
Espero que esta descripción general haya despertado su interés en usar TLA+ para sus propios contratos inteligentes críticos y, si es así, permanezcan atentos: pronto habrá una publicación de seguimiento con un tutorial más detallado sobre cómo usar TLA+ para contratos inteligentes. Y se adjunta un modelo TLA+ real desarrollado por nuestro equipo de I+D.
Contenido IC que te interesa
Progreso tecnológico | Información del proyecto | Eventos globales
Recopile y siga el canal IC Binance
Manténgase actualizado con la información más reciente