-
Buterin señaló en un artículo anterior que, al programar con IA, “la seguridad total es imposible”.
-
El CTO de Ledger cree que la IA está “derrumbando la barrera de entrada” para los hackers.
Vitalik Buterin argumentó que la técnica de verificación formal de código asistida por inteligencia artificial (IA) representa la respuesta al problema que la propia IA introduce en la ciberseguridad, y que ese proceso puede producir software más seguro que el escrito por humanos sin ese respaldo matemático.
La tesis de Buterin, publicada hoy 18 de mayo en su blog personal, aparece como réplica directa a quienes sostienen que la IA, al facilitar el descubrimiento automatizado de vulnerabilidades, haría imposible la confianza en el código sin depender de grandes organizaciones.
Según el cofundador de Ethereum, se trata de un desafío transitorio, no estructural. El estado de equilibrio al que apunta, afirmó, sería «más favorable al defensor que lo que teníamos antes».
La propuesta: dos objetos, una prueba
El argumento central de Buterin es que la verificación formal (la demostración matemática de que un programa se comporta exactamente como promete) puede comprobarse de forma automática.
Según su planteo, un modelo de IA puede escribir código en lenguaje ensamblador de bajo nivel, optimizado para velocidad, y simultáneamente generar la prueba matemática que acredita su equivalencia con una versión legible por humanos. El resultado serían dos objetos separados: uno optimizado para eficiencia, otro para comprensión, unidos por una demostración verificable. El usuario, señaló Buterin, puede verificar esa prueba una sola vez y ejecutar luego la versión rápida sin necesidad de auditar el código internamente.
En ese marco, Buterin mencionó proyectos activos dentro del ecosistema Ethereum que aplican ese enfoque:
- evm-asm: una implementación de la máquina virtual de Ethereum (EVM) escrita directamente en código ensamblador (el lenguaje más cercano al hardware, sin capas intermedias) y verificada formalmente.
- Arklib: un sistema orientado a construir una implementación verificada de STARK, una variante de pruebas de conocimiento cero (ZK), mecanismos criptográficos que permiten demostrar la corrección de un cálculo sin revelar sus datos.
- Esfuerzos similares sobre algoritmos de consenso tolerantes a fallas bizantinas, donde errores en pruebas escritas por humanos ya causaron problemas documentados.
Según Buterin, la fortaleza de ese enfoque reside en que la verificación cubriría el sistema de punta a punta, no solo sus partes por separado, lo que eliminaría la categoría de errores que aparecen en la interfaz entre subsistemas.
Vitalik Buterin reconoce desafíos en su propia propuesta
Sin embargo, el propio Buterin reconoció los límites del enfoque. La verificación formal no prueba que el software sea «correcto» en el sentido que un usuario le daría al término: solo prueba que el código es compatible con las propiedades matemáticas que el desarrollador decidió especificar.
Si esas propiedades están incompletas, o si el desarrollador omite especificar algo crítico, la prueba pasa y el fallo queda intacto. Tampoco cubre comportamientos del hardware, como los ataques de canal lateral por análisis de consumo eléctrico, que exponen claves privadas mediante la observación de patrones físicos externos al código.
Como reportó KriptoNoticias, Buterin ya había señalado en un artículo anterior que, al programar con IA, «la seguridad total es imposible», aunque estimó que en muchos casos concretos es posible verificar afirmaciones específicas que eliminen más del 99% de las consecuencias negativas de un fallo.
Los casos que alimentan el lado opuesto
En mayo pasado, el Google Threat Intelligence Group (GTIG) reportó lo que describió como el primer caso documentado de una vulnerabilidad de «día cero» (un fallo sin parche disponible al momento de su uso) desarrollada con asistencia de IA, como lo notificó KriptoNoticias.
Según Google, el exploit permitía evadir la autenticación en dos pasos de una herramienta de administración de sistemas de código abierto, y los indicios en el código apuntaban a la participación de un modelo de lenguaje.
En febrero, el protocolo de finanzas descentralizadas Moonwell registró una pérdida de USD 1,7 millones después de que un contrato inteligente generado con asistencia de IA fijó el precio del activo cbETH en USD 1,12 frente a su valor de mercado real de más de USD 2.200. La diferencia permitió explotar las garantías mal valuadas antes de que el equipo detectara la anomalía.
Según analistas, el error pasó todas las revisiones humanas previas a su implementación, lo que sitúa la responsabilidad en el proceso de supervisión, no solo en el modelo.
Charles Guillemet, director de tecnología de Ledger, advirtió recientemente que la IA está «derrumbando la barrera de entrada» para los atacantes. Conforme a su planteamiento, convertir la diferencia entre dos versiones de un binario en un exploit funcional (proceso que antes demandaba días de trabajo especializado) ahora puede completarse en horas, mientras la mayoría de los usuarios aún no instaló el parche correspondiente.
La posición de Buterin y la de Guillemet apuntan a diagnósticos distintos sobre el mismo fenómeno: la primera sostiene que la verificación formal convierte la IA en una herramienta neta para el defensor; la segunda, que la velocidad con que la IA reduce el costo de atacar supera por ahora la velocidad con que la industria puede responder.
