Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code

El estudio "Broken by Default" demuestra mediante verificación formal con el solver Z3 que el 55,8% del código generado por siete modelos de IA líderes contiene vulnerabilidades de seguridad matemáticamente probadas, revelando que las herramientas actuales de la industria pasan por casi el 98% de estos fallos y que las instrucciones de seguridad explícitas apenas reducen la tasa de errores.

Lo esencial

Imagina que has contratado a un arquitecto de inteligencia artificial muy famoso para que diseñe los planos de tu nueva casa. Este arquitecto es increíblemente rápido, sabe mucho y puede dibujar miles de habitaciones en segundos. Pero, hay un problema: el arquitecto ha aprendido a dibujar copiando de libros antiguos que tenían errores.

Este documento, titulado "Roto por Defecto" (Broken by Default), es como una inspección de seguridad extremadamente rigurosa que realizaron dos expertos para ver si los planos de este arquitecto son seguros.

Aquí tienes la explicación sencilla, paso a paso:

1. El Experimento: ¿Qué hicieron?

Los investigadores pidieron a 7 de los arquitectos de IA más avanzados del mundo (como GPT-4o, Claude, Gemini, etc.) que escribieran código para tareas delicadas: guardar contraseñas, manejar dinero o proteger datos.

• La prueba: Les dieron 500 tareas diferentes (como "escribe un programa que guarde 100 números en una caja").
• La cantidad: Generaron 3,500 piezas de código en total.
• La herramienta mágica: En lugar de revisar el código con los ojos (que es lento y a veces se nos escapan cosas), usaron un "detective matemático" llamado Z3. Imagina que Z3 es un super-ordenador que no solo busca errores, sino que demuestra matemáticamente si un error puede hacer explotar la casa. Si Z3 dice "sí, esto explota", entonces explota. No es una sospecha, es una prueba.

2. Los Resultados: ¡Es un desastre!

Los resultados fueron alarmantes. De cada 100 piezas de código que generaron las IAs:

• Más de la mitad (55.8%) tenían agujeros de seguridad graves.
• El "mejor" arquitecto (Gemini 2.5 Flash) falló en casi la mitad de sus intentos.
• El "peor" (GPT-4o) falló en el 62% de los casos.
• Ninguna IA obtuvo una calificación de "A" o "B". Todas reprobaron.

La analogía de la puerta:
Imagina que pides a la IA que construya una puerta blindada. La IA te entrega una puerta que parece perfecta por fuera, pero si empujas la manija con la fuerza exacta (un número específico que el detective matemático encontró), la puerta se desmorona y deja entrar a cualquier ladrón.

3. ¿Por qué fallan? (El problema de la "Memoria")

Los investigadores descubrieron que el problema no es que las IAs sean "tontas", sino que han aprendido de los malos hábitos de internet.

• La mayoría del código que existe en internet tiene errores de cálculo (como calcular mal el tamaño de una caja para guardar cosas).
• La IA aprendió que "así se hace" y lo repite automáticamente.
• El error más común: Olvidar poner un "freno de emergencia" cuando se calculan números grandes. Es como intentar meter 100 elefantes en un coche pequeño; la IA simplemente lo hace sin pensar que el coche se romperá.

4. ¿Funciona si les decimos "¡Sé seguro!"?

Los investigadores probaron algo muy simple: le dijeron a las IAs, "Por favor, escribe código seguro y revisa los números".

• Resultado: Apenas mejoraron un poquito (de un 64% de errores a un 60%).
• La lección: Decirle a la IA "sé bueno" es como decirle a un niño que no coma azúcar mientras le das un plato lleno de dulces. El hábito de copiar los errores es tan fuerte que las instrucciones de seguridad no logran cambiarlo.
• Nota importante sobre esta prueba: Esta pequeña mejora se midió en un subconjunto más pequeño de 50 instrucciones (una versión preliminar del estudio), no en las 500 tareas completas. Aunque la tendencia es clara, este experimento específico se realizó a menor escala para validar la idea antes de escalarla.

5. ¿Y los antivirus y revisores de código actuales?

Aquí viene la parte más sorprendente. Los investigadores compararon su "detective matemático" (Z3) con 6 de las mejores herramientas de seguridad que usan las empresas hoy en día (como CodeQL, Semgrep, etc.).

• El resultado: Las herramientas tradicionales se perdieron el 97.8% de los errores que la IA cometió.
• La analogía: Es como usar un detector de metales para buscar agujeros en una pared de vidrio. El detector de metales (las herramientas actuales) funciona bien para buscar clavos (errores obvios), pero no ve los agujeros invisibles en el vidrio (errores matemáticos complejos). Las IAs están creando agujeros que las herramientas actuales ni siquiera saben que existen.

6. La Paradoja: Saben el error, pero lo cometen

Hicieron una prueba final: le mostraron a la IA el código que ella misma había escrito y le preguntaron: "¿Ves algún error aquí?".

• Resultado: La IA identificó el error el 78% de las veces.
• El problema: Saben que es un error cuando lo miran, pero siguen cometiendo el error cuando lo escriben. Es como un conductor que sabe que no debe ir a 200 km/h, pero cuando se sienta en el coche, lo hace automáticamente.

Conclusión: ¿Qué debemos hacer?

El mensaje final del documento es claro y directo:

1. No confíes ciegamente: El código que genera la IA viene "roto por defecto".
2. No basta con pedirlo: Decirle "hazlo seguro" no arregla el problema de raíz.
3. Necesitamos nuevos ojos: Las herramientas actuales no sirven para detectar estos errores específicos. Necesitamos métodos más avanzados (como el detective matemático que usaron ellos) o, mejor aún, revisión humana experta.

En resumen: Las IAs son geniales para escribir rápido, pero son como un niño que dibuja planos de casas sin saber de física: se ven bonitos, pero si intentas vivir en ellos, la casa se cae. Hasta que no aprendan a pensar como ingenieros de seguridad (y no solo como copiadores de internet), debemos tratar todo lo que escriban como si fuera un plano con bombas ocultas.

Resumen técnico

A continuación presento un resumen técnico detallado del artículo "Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code" (Roto por Defecto: Un Estudio de Verificación Formal de Vulnerabilidades de Seguridad en Código Generado por IA), basado en el documento proporcionado.

---

Resumen Técnico: "Broken by Default"

1. El Problema

La adopción masiva de asistentes de codificación con IA (como GitHub Copilot, ChatGPT, Claude y Gemini) en dominios sensibles a la seguridad ha creado una brecha crítica: la explotabilidad del código generado no ha sido cuantificada con rigor.

• Limitaciones de trabajos previos: Estudios anteriores se han basado en coincidencia de patrones estáticos (regex, AST) o inspección manual, las cuales no pueden establecer la explotabilidad definitiva de una vulnerabilidad.
• La hipótesis central: Existe una suposición de que las instrucciones de seguridad en los prompts o el uso de herramientas de análisis estático tradicionales son suficientes para mitigar riesgos. Este estudio cuestiona si los modelos de lenguaje (LLM) generan código inherentemente inseguro por defecto y si las herramientas actuales pueden detectarlo.

2. Metodología

El estudio emplea una metodología de verificación formal combinada con análisis empírico a gran escala.

• Dataset y Configuración:

  • Volumen: 3,500 artefactos de código generados a partir de 500 prompts de seguridad crítica.
  • Modelos Evaluados: 7 LLMs de vanguardia (GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B, Llama 4 Scout).
  • Categorías de Vulnerabilidad (CWE): 5 categorías principales (100 prompts cada una):
    • MEM (CWE-131/190): Gestión de memoria y desbordamiento de búfer.
    • INT (CWE-190/195): Aritmética de enteros y conversiones de tipo.
    • AUTH (CWE-916): Hashing de contraseñas y gestión de sesiones.
    • CRYPTO (CWE-327/330): Generación de claves y uso de números aleatorios.
    • INP (CWE-89/22/78): Inyección SQL y manejo de rutas.
  • Configuración: Todos los modelos se consultaron con temperature=0 (modo determinista) para garantizar la reproducibilidad.

• Pipeline de Análisis COBALT:

  • Utiliza el solver Z3 SMT (Satisfiability Modulo Theories) para codificar las condiciones de vulnerabilidad como fórmulas lógicas.
  • Diferenciador clave: En lugar de buscar patrones, Z3 intenta probar matemáticamente si existe un valor de entrada (testigo concreto) que satisfaga la condición de fallo (ej. desbordamiento de entero).
  • Clasificación:
    • Z3 SAT: Vulnerabilidad formalmente probada con un testigo de explotación concreto.
    • PATTERN MATCH: Vulnerabilidad estructural detectada pero sin prueba formal inmediata.
    • CLEAN: Sin vulnerabilidad.

• Validación en Tiempo de Ejecución:

  • Se seleccionaron hallazgos representativos para crear Proofs of Concept (PoC).
  • Se compiló el código con GCC AddressSanitizer (ASAN) para confirmar fallos de memoria en tiempo de ejecución (corrupción de memoria, desbordamiento de pila/heap).

• Experimentos Auxiliares:

  1. Ablación de Prompts Seguros: Comparación de prompts estándar vs. prompts con instrucciones explícitas de seguridad. Nota importante: Este experimento de ablación se realizó específicamente en un sub-corpus de 50 prompts (v1), no en el conjunto completo de 500 prompts del benchmark, un detalle crucial para la replicabilidad.
  2. Comparación de Herramientas Estáticas: Evaluación de 6 herramientas de la industria (Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL) contra los hallazgos de COBALT.
  3. Asimetría Generación-Revisión: Se pidió a los modelos que revisaran su propio código vulnerable generado para ver si podían identificar los errores.

3. Contribuciones Clave

1. Verificación Formal a Escala: Es el primer estudio que aplica la resolución SMT (Z3) sistemáticamente a miles de artefactos de IA para establecer la "verdad fundamental" (ground truth) de la explotabilidad, más allá de la heurística.
2. Pruebas de Explotabilidad Real: Validación de vulnerabilidades teóricas mediante ejecuciones reales que causan fallos de memoria (crashes) confirmados por ASAN.
3. Cuantificación de la Brecha de Detección: Demostración empírica de que las herramientas de análisis estático actuales son estructuralmente incapaces de detectar ciertos tipos de vulnerabilidades generadas por IA (específicamente desbordamientos en aritmética de asignación de memoria).
4. Identificación de la Asimetría Generación-Revisión: Evidencia de que los modelos poseen el conocimiento para detectar vulnerabilidades cuando se les pide revisar, pero fallan consistentemente al generar el código inicialmente.

4. Resultados Principales

• Tasas de Vulnerabilidad (Promedio General):

  • 55.8% de todos los artefactos contienen al menos una vulnerabilidad identificada por COBALT.
  • 1,055 hallazgos fueron formalmente probados como explotables mediante testigos Z3 SAT.
  • Calificación: Ningún modelo alcanzó una calificación mejor que "D".
    • Peor rendimiento: GPT-4o (62.4%, Calificación F).
    • Mejor rendimiento: Gemini 2.5 Flash (48.4%, Calificación D).
  • Categoría más crítica: Aritmética de enteros (INT) con una tasa de fallo del 87%, seguida por asignación de memoria (MEM) con 67%.

• Validación en Tiempo de Ejecución:

  • De 7 casos seleccionados para PoC, 6 produjeron fallos confirmados (desbordamiento de heap, lectura fuera de límites, inyección SQL funcional).
  • Ejemplo: Una contraseña de 6 caracteres fue recuperada en 0.01ms mediante un ataque de fuerza bruta a un hash SHA-256 débil generado por la IA.

• Experimento de Instrucciones de Seguridad (Ablación):

  • Al añadir instrucciones explícitas de seguridad ("escribe código seguro", "evita desbordamientos") en el sub-corpus de 50 prompts (v1), la tasa de vulnerabilidad promedio se redujo en solo 4 puntos porcentuales (de 64.8% a 60.8%).
  • Cuatro de cinco modelos permanecieron con calificación "F". Esto sugiere que los patrones inseguros están internalizados en la distribución previa de generación del modelo y no se corrigen con instrucciones superficiales.

• Comparación con Herramientas de la Industria:

  • Las 6 herramientas combinadas (Semgrep, Bandit, Cppcheck, Clang, FlawFinder, CodeQL) detectaron solo el 7.6% de los artefactos vulnerables.
  • Brecha Crítica: Las herramientas pasaron por alto el 97.8% de las vulnerabilidades formalmente probadas por Z3.
  • Causa: Las herramientas basadas en patrones o flujo de datos no pueden razonar aritméticamente sobre la posibilidad de desbordamiento en expresiones como malloc(n * sizeof(T)) sin un contexto de taint concreto, algo que Z3 resuelve mediante aritmética de vectores de bits.

• Asimetría Generación-Revisión:

  • Los modelos identificaron correctamente sus propias vulnerabilidades Z3-probadas en el 78.7% de los casos cuando se les pidió revisar el código.
  • Sin embargo, generaron esas mismas vulnerabilidades en el 55.8% de los casos durante la generación inicial. Esto indica que el problema no es la falta de conocimiento, sino la incapacidad de aplicar ese conocimiento de forma espontánea durante la generación.

5. Significado e Implicaciones

• El Código de IA es "Roto por Defecto": Los asistentes de codificación actuales introducen vulnerabilidades críticas en más de la mitad de los casos, especialmente en operaciones de memoria y enteros.
• Ineficacia de las Mitigaciones Actuales:
  • Las instrucciones de seguridad en los prompts son insuficientes (como se demostró en el experimento de ablación).
  • Las herramientas de análisis estático estándar (CodeQL, Cppcheck, etc.) son ciegas a las vulnerabilidades más comunes generadas por IA (desbordamiento de enteros en asignación de memoria).
• Necesidad de Verificación Formal: El estudio concluye que la verificación formal (SMT) es la única metodología capaz de establecer la explotabilidad real de los patrones de vulnerabilidad dominantes en el código generado por IA.
• Recomendaciones para Desarrolladores:
  1. Tratar el código generado por IA en C/C++ como código no revisado que requiere auditoría de seguridad explícita.
  2. No confiar en herramientas estáticas tradicionales para detectar desbordamientos en aritmética de asignación.
  3. Utilizar compiladores con sanitizadores (-fsanitize=address,undefined) en todos los sistemas generados por IA.
  4. Considerar la verificación formal como un componente obligatorio en pipelines de revisión de código críticos para la seguridad.

En resumen, el artículo demuestra que, a pesar de los avances en la capacidad de generación de código, los LLMs actuales carecen de la capacidad intrínseca para generar código seguro en dominios críticos sin intervención humana rigurosa o verificación formal, y que las herramientas de seguridad actuales no están preparadas para detectar estos fallos específicos.