Vitalik Buterin ha rechazado la afirmación de que los hackers de IA cada vez más capaces harán que la ciberseguridad sea efectivamente imposible de ganar, argumentando el 17 de septiembre que las herramientas de verificación avanzadas podrían eventualmente dar a los defensores una ventaja estructural.
Resumen
- El 90% del patrimonio neto de Buterin permanece en criptomonedas, según su propia declaración del 17 de septiembre.
- La verificación formal asistida por IA podría ayudar a demostrar que el software cumple con propiedades de seguridad definidas, según el argumento de Buterin.
- El equipo de seguridad de Ethereum ya utiliza agentes de IA para inspeccionar el código del protocolo y reproducir vulnerabilidades de forma independiente.
- Los investigadores de Ethereum ahora tratan la verificación formal como una herramienta transversal en varias líneas de investigación de protocolos a largo plazo.
- Anthropic dice que la IA de frontera puede acelerar los ataques, mientras que sus modelos han identificado miles de fallos.
Buterin escribió en su publicación del 17 de septiembre en X que no está de acuerdo con la opinión cada vez más común de que "el hacking con IA significa que la ciberseguridad está condenada". Dijo que las personas que continúan manteniendo criptomonedas están apostando implícitamente a que los sistemas digitales seguros pueden sobrevivir a ataques automatizados más fuertes, y añadió que aproximadamente el 90% de su propio patrimonio neto permanece en criptomonedas.
Su argumento se centra en la verificación formal, una técnica que utiliza especificaciones y pruebas matemáticas para determinar si el software se comporta de acuerdo con propiedades predefinidas. Buterin utilizó la demostración avanzada de teoremas matemáticos como analogía, diciendo que una IA suficientemente capaz podría ayudar a demostrar que "este programa es seguro" incluso cuando el software en sí es complejo.
Buterin dice que la verificación formal puede favorecer a los defensores
El argumento de Buterin no trata la seguridad de la IA como una carrera en la que los investigadores defensivos simplemente encuentran errores antes que los atacantes. Su publicación describe en cambio un modelo en el que los desarrolladores definen las propiedades que un sistema debe cumplir, y luego utilizan herramientas de prueba automatizadas para establecer que la implementación las obedece.
La propia documentación de verificación formal de Ethereum describe la técnica en términos más limitados. Dice que la verificación formal puede demostrar matemáticamente que un contrato inteligente cumple con una especificación formal, ofreciendo garantías más sólidas que las pruebas ordinarias para las propiedades incluidas en esa especificación.
La misma documentación de Ethereum identifica una limitación importante detrás de los comentarios de Buterin. Una prueba establece que el software cumple con la especificación que se está verificando; no prueba automáticamente que los desarrolladores definieron correctamente todas las propiedades de seguridad. Las especificaciones mal elegidas o incompletas pueden dejar comportamientos fuera de la prueba.
Buterin hizo la misma distinción en su publicación. Argumentó que definir "seguridad" de forma demasiado estrecha puede omitir rutas de ataque que involucran áreas como protocolos, servidores, bases de datos, capas de red, cachés u otros componentes de soporte. Su dirección propuesta es, por lo tanto, verificar más del sistema completo en lugar de etiquetar un pequeño grupo de módulos como críticos para la seguridad.
Buterin ya había descrito la verificación formal asistida por IA como una posible "forma final" del desarrollo de software. Sus comentarios anteriores aplicaban el enfoque a áreas como el consenso de Ethereum, los sistemas de conocimiento cero y la criptografía resistente a la computación cuántica.
Ethereum ya está probando la seguridad asistida por IA
Los investigadores de Ethereum ya están utilizando la IA en el trabajo de seguridad, aunque los sistemas actuales aún están lejos de la prueba automática de la seguridad de todo el sistema.
El equipo de Seguridad del Protocolo de la Fundación Ethereum informó en julio que agentes de IA coordinados habían encontrado defectos reales en sistemas utilizados por Ethereum. Un hallazgo confirmado involucró un fallo de acceso remoto en la implementación de red Gossipsub de Rust libp2p.
La falla se convirtió en CVE-2026-34219. El registro de la Base de Datos Nacional de Vulnerabilidades de EE. UU. indica que las versiones anteriores a la 0.49.4 podían bloquearse remotamente mediante un mensaje PRUNE manipulado que provocaba un desbordamiento aritmético durante el manejo del retroceso de Gossipsub. La versión 0.49.4 solucionó el problema.
El equipo de seguridad de la Fundación dijo que el descubrimiento de vulnerabilidades no fue la parte más difícil del flujo de trabajo de IA. Los investigadores descubrieron que los agentes de IA generaban con frecuencia informes convincentes que involucraban rutas de ejecución inalcanzables, fallos solo de depuración o pruebas formales que técnicamente pasaban mientras demostraban una propiedad más débil de lo previsto.
La reproducción independiente siguió siendo un requisito antes de que el equipo aceptara un hallazgo. La Fundación dijo que se necesitaban verificaciones automatizadas y revisión humana porque un agente podía producir una prueba de aspecto válido que no lograba restringir el comportamiento del software que los investigadores realmente querían probar.
La experiencia de la Fundación se describió como un problema de triaje: la IA podía generar grandes cantidades de vulnerabilidades candidatas, pero los investigadores aún tenían que determinar si cada problema era alcanzable y significativo en producción.
La verificación formal entra en la hoja de ruta del protocolo de Ethereum
La Fundación Ethereum ha hecho por separado de la verificación formal parte de su programa actual de investigación de protocolos. En su actualización de prioridades del protocolo del 7 de septiembre, la Fundación dijo que la verificación formal serviría como herramienta transversal en sus áreas de investigación plurianuales restantes. El documento abarca el trabajo sobre privacidad, estado, desarrollo de zkEVM, seguridad post-cuántica y otros componentes del protocolo hasta 2029.
La misma hoja de ruta dice que se espera que el desarrollo de un zkEVM de capa 1 impulse las herramientas de verificación formal, los flujos de trabajo y los componentes criptográficos verificados. Los investigadores de Ethereum están trabajando hacia un sistema en el que los validadores eventualmente verifiquen pruebas de ejecución sucintas en lugar de re-ejecutar independientemente cada bloque.
Un proyecto separado de la Fundación Ethereum lanzado en agosto ya está combinando agentes de IA con pruebas verificadas por máquina. El proyecto better.codes permite a los investigadores dirigir sistemas de IA hacia un problema de solidez criptográfica formalizado en Lean, mientras que el kernel de Lean comprueba si las pruebas enviadas satisfacen un enunciado de teorema fijo.
El informe de financiación del segundo trimestre de la Fundación enumera más trabajos que combinan modelos de lenguaje grandes con métodos formales. Los proyectos incluyen ETHeorem para verificar implementaciones de clientes de Ethereum contra especificaciones, SPECA y LeanAgent para trabajo automatizado de cumplimiento de protocolos, y verificación formal que involucra infraestructura zkVM de RISC-V.
La hoja de ruta técnica actualizada de Ethereum otorga a la verificación formal un papel junto con la privacidad, las pruebas de conocimiento cero y la protección post-cuántica. Los comentarios de Buterin del 17 de septiembre, por lo tanto, continúan una dirección de investigación existente en lugar de anunciar una nueva actualización o una bifurcación programada. Su publicación no nombró un nuevo EIP, una fecha de despliegue ni una regla obligatoria que requiera que cada programa de Ethereum se someta a verificación formal.
La evidencia actual de IA también muestra una capacidad ofensiva más fuerte
La investigación reciente en ciberseguridad respalda la preocupación de que la IA está haciendo a los atacantes más capaces, incluso mientras se amplía el uso defensivo. Anthropic dijo en suinforme de inteligencia de amenazas de septiembre que había observado a actores maliciosos usando IA para automatizar la investigación de vulnerabilidades, el desarrollo de exploits y campañas multiobjetivo. La compañía dijo que algunos operadores mantenían flujos de trabajo automatizados que podían realizar investigación de vulnerabilidades de forma continua.
Una investigación anterior de Anthropic encontró evidencia similar a escala. Su panel de divulgación coordinada dijo que, para el 26 de agosto, la compañía había divulgado 2.300 vulnerabilidades descubiertas por IA en 392 proyectos de código abierto, con 421 parcheadas en origen en ese momento.
Anthropic ha descrito la misma tecnología como útil para la defensa. Su iniciativa Project Glasswing informó haber utilizado modelos de frontera con empresas de seguridad y proveedores de software para localizar fallas de severidad alta y crítica antes de que los actores maliciosos pudieran explotarlas.
El lado ofensivo sigue siendo medible. El estudio de Anthropic de junio examinó 832 cuentas asociadas con actividad cibernética maliciosa desde marzo de 2025 hasta marzo de 2026 y encontró actores de amenazas que utilizan IA en múltiples etapas de las operaciones cibernéticas. Buterin ya había rechazado un argumento separado de que los riesgos de seguridad impulsados por la IA podrían dañar gravemente la confianza en Bitcoin. Dijo que los problemas de la capa de red a menudo podrían abordarse mediante actualizaciones de software y de la infraestructura de minería, mientras describía como altamente improbable que se produjeran rupturas reales de los hashes de Bitcoin o de su mecanismo de prueba de trabajo.
El informe de Anthropic de septiembre dijo que sus investigadores habían identificado operadores que utilizaban canalizaciones de exploits construidas con IA contra dispositivos de seguridad y objetivos gubernamentales, y que algunas campañas produjeron vulnerabilidades previamente desconocidas que los atacantes validaron en sus propios entornos de prueba.
