(P1) El cofundador de Ethereum, Vitalik Buterin, afirmó que la verificación formal asistida por IA podría eliminar la gran mayoría de las vulnerabilidades de código, una declaración que surge justo cuando otro protocolo DeFi perdió 11,6 millones de dólares debido a un exploit en su puente de Ethereum.
(P2) "Si se realiza una verificación formal de extremo a extremo, no solo se está demostrando que alguna descripción del protocolo es segura en teoría, sino que la pieza específica de código que ejecuta el usuario es segura en la práctica", escribió Buterin en una publicación de blog publicada el lunes. Argumentó que este enfoque podría eliminar más del 99% de las consecuencias negativas del código defectuoso.
(P3) Los comentarios de Buterin sobre la seguridad del código cobraron relevancia tras un reporte de exploit en el puente de Ethereum de Verus Protocol. Las firmas de seguridad on-chain Blockaid y PeckShield informaron que un atacante utilizó un mensaje de transferencia cross-chain falsificado para drenar activos, que luego fueron convertidos en 5.402 Ether, con un valor de más de 11,4 millones de dólares.
(P4) El incidente subraya los riesgos financieros de los errores de software en el ecosistema cripto. Buterin cree que la verificación formal es esencial para asegurar la próxima generación de la infraestructura de Ethereum, particularmente para componentes complejos y críticos como las firmas resistentes a la computación cuántica, los STARK y los ZK-EVM.
Según Blockaid, el incidente del puente Verus fue causado por la falta de una validación del monto de origen, una falla que podría haberse identificado y solucionado con aproximadamente 10 líneas de código Solidity. La firma de seguridad señaló que la estructura del ataque se asemejaba a los exploits de 2022 de Nomad Bridge (190 millones de dólares) y Wormhole (325 millones de dólares), donde instrucciones fraudulentas engañaron a los puentes para que enviaran fondos de sus reservas.
En su publicación, Buterin describió un futuro en el que las herramientas de IA ayuden a los desarrolladores a escribir tanto código altamente eficiente como las pruebas matemáticas para verificar su corrección. Se refirió a esta combinación como una potencial "forma final del desarrollo de software". Este método se considera una defensa poderosa contra un futuro en el que la IA avanzada también podría usarse para descubrir y ejecutar ciberataques a una escala sin precedentes.
Aunque es un firme defensor, Buterin advirtió que la verificación formal "no es una panacea", ya que no puede eliminar todos los riesgos de seguridad, como los derivados de suposiciones iniciales erróneas o vulnerabilidades de hardware. Sin embargo, argumentó que es excepcionalmente adecuada para los complejos sistemas criptográficos que sustentarán la futura hoja de ruta de Ethereum, haciendo que el código casi libre de errores sea una expectativa realista.
Este artículo es solo para fines informativos y no constituye asesoramiento de inversión.
