La auditoría de Miden de Trail of Bits detectó una falla en Falcon después de que los agentes crearan las herramientas faltantes

Trail of Bits dedicó seis meses a prepararse para la auditoría de Miden y luego encontró una falla de alta gravedad con herramientas que sus agentes de IA habían creado desde cero. La auditoría de Miden de Trail of Bits implicó mucho más que apuntar un modelo al código fuente. Sus agentes crearon un servidor LSP, un descompilador, un motor de análisis estático y un modelo en Lean antes de que comenzara la revisión formal.

Esa preparación reveló un valor insuficientemente restringido que, según los informes, podía permitir a un probador malicioso falsificar firmas Falcon y vaciar las cuentas afectadas. Los analizadores también identificaron más de 400 ubicaciones en las que podía mejorarse la validación de tipos. Mientras tanto, el esfuerzo de verificación formal produjo 95 pruebas de corrección verificadas por máquina y descubrió dos errores que las pruebas unitarias existentes no habían detectado.

La competencia importante no es entre agentes de IA y auditores humanos. Es entre la revisión directa de código con IA y la construcción asistida por agentes de la infraestructura que posibilita revisar código complejo. Trail of Bits siguió dependiendo de supervisión humana, revisión manual de teoremas y criterio convencional de seguridad. Los agentes cambiaron qué proyectos de apoyo resultaban económicamente viables.

La auditoría de Miden de Trail of Bits comenzó seis meses antes

El trabajo decisivo empezó antes de que los auditores recibieran un objetivo terminado para inspeccionar.

El equipo de Miden contactó a Trail of Bits a finales de 2025, según el detallado relato de la auditoría de Miden de la firma. Miden quería que se revisaran partes de su máquina virtual de conocimiento cero antes del lanzamiento. Una sección abarcaba una biblioteca central que contenía primitivas criptográficas escritas en Miden Assembly, o MASM.

Una máquina virtual de conocimiento cero, a menudo abreviada como zkVM, demuestra que un programa se ejecutó correctamente sin exigir que cada verificador repita ese cálculo. Miden utiliza una arquitectura de máquina de pila. Las instrucciones consumen valores de una pila y vuelven a colocar sus resultados en ella.

Esa arquitectura importa porque las entradas y salidas suelen ser implícitas en el código MASM. Un revisor debe seguir cómo cada instrucción modifica la pila y trasladar ese estado entre ramas, bucles y llamadas a procedimientos. Las señales familiares del código fuente pueden desaparecer.

MASM también carecía de gran parte de las herramientas que los auditores normalmente esperan. Había poco soporte para editores, ningún servidor de lenguaje maduro adaptado a la revisión y análisis automatizado limitado para la biblioteca central. Trail of Bits sabía que la implementación aún no estaba completa en funcionalidades, pero también sabía que la revisión sería seis meses después.

La firma utilizó ese intervalo para construir su propio entorno de revisión. Claude produjo un prototipo inicial del servidor de lenguaje en cuestión de días, según Trail of Bits. El resultante servidor de lenguaje MASM ofrece navegación, descubrimiento de referencias, documentación al pasar el cursor, diagnósticos de sintaxis, descripciones de instrucciones e información sobre efectos de pila.

Estas funciones parecen comodidades ordinarias para desarrolladores. En un lenguaje ensamblador desconocido, pasan a formar parte del método de seguridad. La navegación ayuda a los auditores a seguir un valor a través de los límites entre procedimientos. Los efectos de pila integrados reducen la reconstrucción manual repetida. Los diagnósticos exponen supuestos antes de que se conviertan en hallazgos.

Trail of Bits amplió después el proyecto hacia la descompilación, el análisis estático, las herramientas de línea de comandos y el modelado formal. Claude se ocupó de tareas de planificación e implementación, mientras que Codex participó en la revisión de código. Los agentes también intercambiaron roles, lo que dio al trabajo generado una pasada de revisión separada.

No fue un proceso de generación de una sola vez. Tras implementar una función, el equipo pidió a los agentes que descompilaran procedimientos aleatorizados y compararan los resultados con el MASM original. Las regresiones se convirtieron en pruebas y el modelo pasó a trabajar contra esas pruebas.

Ese ciclo de retroalimentación es central en la historia. Los agentes no fueron tratados como autoridades cuyo resultado mereciera confianza automática. Operaban dentro de un sistema de verificación en expansión que contenía pruebas, etapas de revisión, analizadores y, posteriormente, un verificador de pruebas.

Por tanto, la auditoría comenzó con una pregunta distinta de la habitual. Trail of Bits no preguntó únicamente si un agente podía encontrar vulnerabilidades. Preguntó qué instrumentos ausentes impedían a los auditores, incluidos los agentes, comprender el código en primer lugar.

Ese cambio de alcance creó las condiciones para los hallazgos posteriores. También presionó a los equipos de seguridad que comercializan la revisión con IA principalmente como un escaneo más rápido del código fuente. El enfoque de Trail of Bits exigió más preparación, pero convirtió esa preparación en infraestructura técnica reutilizable.

El descompilador se volvió más valioso que su resultado

El descompilador importó sobre todo porque su representación interna dio a otros análisis un lugar fiable donde operar.

Descompilar MASM no consistía simplemente en sustituir instrucciones de ensamblador por expresiones legibles. La mayoría de los procedimientos de la biblioteca central carecían de firmas declaradas, por lo que las herramientas a menudo tenían que inferir sus entradas y salidas a partir del contexto. Los procedimientos tampoco contaban con una convención de llamada uniforme.

Los bucles generaban otro problema. Un bucle while de MASM no tiene que preservar la misma forma de pila entre iteraciones. Su condición puede desplazarse a otra posición de la pila, frustrando los intentos simples de asignar nombres estables a las entradas de las instrucciones.

Las ramas condicionales también pueden producir efectos de pila distintos. Si una rama añade un elemento y otra elimina uno, el descompilador no puede fusionar ciegamente sus estados. Los errores en la inferencia de efectos de pila pueden propagarse entonces a cada procedimiento que llama al código afectado.

Trail of Bits respondió limitando su promesa. Su descompilador MASM se dirige a un subconjunto bien definido en lugar de afirmar una recuperación perfecta para cada procedimiento. Esa decisión priorizó la corrección por encima de una cobertura superficial.

El descompilador se convirtió en el mayor esfuerzo de herramientas del proyecto. Trail of Bits informa de más de 100 commits generados por IA a lo largo de varios meses. Sin embargo, el pseudocódigo terminado no fue su resultado más trascendental.

El proyecto creó una representación intermedia, o IR, que expresaba las entradas y salidas de los procedimientos como expresiones analizables. Una IR es una versión estructurada del código diseñada para su transformación o análisis. Una vez que las instrucciones MASM existían en esa forma, el equipo podía aplicar técnicas consolidadas de flujo de datos y análisis estático.

El analizador podía preguntar si los valores suministrados por el probador se validaban antes de usarse. Podía rastrear si el código imponía los tipos esperados, como enteros de 32 bits o valores booleanos. También podía determinar si las variables locales se inicializaban en todas las posibles rutas de ejecución.

Trail of Bits utilizó interpretación abstracta para parte de este trabajo. La interpretación abstracta evalúa categorías de valores posibles en lugar de ejecutar un programa con una entrada concreta. Un valor podría representarse como un entero válido de 32 bits, un booleano o un valor desconocido.

El análisis se repite hasta alcanzar un estado estable en el que no aparece información nueva. Cuando se diseña de forma sólida, sobreaproxima lo que pueden hacer las ejecuciones reales. Esto puede producir falsos positivos, pero no debería excluir silenciosamente un comportamiento real cubierto por el modelo.

Esto ilustra por qué la auditoría de Miden de Trail of Bits difiere de una demostración genérica de programación con IA. No se confió en el descompilador generado por agentes para declarar seguro el código. Ayudó a construir un sustrato sobre el cual podían ejecutarse análisis explícitos e inspeccionables.

El flujo de trabajo también generó beneficios para los humanos. Los procedimientos descompilados facilitaron revisar el flujo de control y de datos de alto nivel dentro del editor. Las anotaciones de pila redujeron la carga mental de seguimiento. Las interfaces de línea de comandos pusieron las mismas capacidades a disposición de los procesos de revisión automatizada.

Hay una lección más amplia para los equipos que evalúan agentes de programación. El artefacto generado más valioso puede no ser el que ven los usuarios. Un descompilador de alcance parcial puede justificar su coste si su analizador, su modelo de flujo de control y su IR habilitan varias comprobaciones de mayor valor.

Esa conclusión también cambia la forma en que los equipos deberían preservar el contexto del proyecto. Los prompts de los agentes, los casos de regresión, las decisiones arquitectónicas y los comentarios de los revisores se convierten en insumos duraderos de ingeniería. Una base de conocimiento consultable puede ayudar a mantener esos materiales disponibles durante proyectos de seguridad prolongados.

La revisión directa con IA suele comenzar con el código objetivo y buscar defectos. Trail of Bits usó en cambio agentes para modificar la superficie de revisión. El siguiente resultado mostró por qué esa distinción importaba.

Una comprobación ausente llegó a la autenticación Falcon

Un único resto no validado supuestamente convirtió un auxiliar aritmético en una vía para falsificar autenticación.

Durante la auditoría, los análisis estáticos identificaron más de 400 ubicaciones únicas en las que podía mejorarse la validación de tipos. Trail of Bits afirma que todas eran accesibles desde la API pública de la biblioteca central. Muchas surgieron porque los procedimientos expuestos públicamente podían llamarse sin los supuestos que esperaban sus autores originales.

Un procedimiento público no puede depender de forma segura de que cada llamador proporcione un valor del tipo previsto. En un sistema de pruebas, es especialmente importante distinguir entre un valor proporcionado por el probador y un valor restringido por la prueba. Simplemente introducir datos en un cálculo no establece que representen el entero o booleano declarado.

El hallazgo de alta gravedad se centró en mod_12289, un procedimiento que reduce un valor de 64 bits módulo 12.289. El probador proporcionaba un cociente y un resto mediante un mecanismo de advice. Los valores de advice son sugerencias de ejecución calculadas fuera de la VM, utilizadas a menudo para evitar trabajo costoso dentro de la VM.

El cociente recibió una comprobación que confirmaba que encajaba en la representación esperada de 64 bits. El resto no recibió una validación equivalente antes de entrar en u32overflowing_sub, una instrucción de resta de 32 bits.

Trail of Bits afirma que un atacante podía variar el cociente y el resto sin dejar de satisfacer las restricciones de la resta. Esto permitía que mod_12289 devolviera algo distinto del resto matemáticamente correcto.

El alcance del error fue más allá de un resultado aritmético incorrecto. El procedimiento servía de apoyo para la verificación de firmas Falcon. Falcon es un esquema de firma digital poscuántica y Miden utilizaba una variante en la autenticación de cuentas.

Según Trail of Bits, un probador malicioso podía explotar el valor insuficientemente restringido para falsificar una firma Falcon y vaciar una cuenta controlada por un par de claves Falcon. Esta es la afirmación técnica de la firma, no un exploit reproducido de forma independiente presentado en el artículo público.

La gravedad se deriva del modelo de ejecución de Miden. El diseño de la Miden VM admite entradas no deterministas proporcionadas durante la generación de pruebas. Estas entradas pueden mejorar la eficiencia, pero el programa debe restringirlas cuidadosamente.

Un verificador no infiere la intención del desarrollador. Comprueba si la prueba presentada satisface las restricciones codificadas. Si esas restricciones aceptan un resto no válido, la prueba puede seguir siendo válida incluso cuando la relación aritmética declarada sea falsa.

Esta es la inversión central. Las pruebas de conocimiento cero pueden establecer la ejecución fiel de un sistema especificado, pero no pueden reparar una especificación incompleta. Una prueba criptográfica de un programa insuficientemente restringido puede aportar confianza en la propiedad equivocada.

El contexto independiente de una auditoría de contratos de Miden posterior refuerza el punto general. OpenZeppelin describió las transacciones de Miden como válidas cuando existe una prueba correspondiente, lo que convierte cada comprobación MASM en parte de las restricciones que un probador debe satisfacer.

Ese encargo independiente cubrió un alcance de repositorio distinto y no debe confundirse con la revisión de Trail of Bits. Sin embargo, ambos relatos muestran por qué la lógica de autenticación, las entradas controladas por el probador y las suposiciones on-chain requieren un tratamiento explícito.

Las más de 400 ubicaciones de validación de tipos también deben interpretarse con cuidado. No se describieron como 400 vulnerabilidades explotables. Representaban lugares donde la validación podía mejorar, con un problema de alta gravedad reportado entre ellos.

Esta distinción importa porque el análisis estático suele detectar condiciones que requieren evaluación. Un analizador sólido puede informar intencionalmente más casos de los que finalmente se convierten en defectos de seguridad. Su valor reside en localizar sistemáticamente supuestos que merecen inspección.

Para los equipos de seguridad, el resultado cuestiona un atajo habitual: usar un agente para resumir funciones sospechosas sin modelar primero las reglas de valores del lenguaje objetivo. Un modelo puede explicar qué parece hacer el código. El analizador puede preguntar si cada ejecución permitida respeta realmente el tipo requerido.

El hallazgo de Falcon surgió de combinar ambas capacidades. Los agentes aceleraron la construcción, mientras que la semántica estática convirtió una intuición sobre datos controlados por el probador en una comprobación repetible.

Las pruebas en Lean encontraron lo que las pruebas unitarias pasaron por alto

La verificación formal no sustituyó las pruebas, pero obligó al equipo a expresar el comportamiento con suficiente precisión para revelar dos fallos no comprobados.

Trail of Bits siguió adelante con el modelado formal incluso después de crear las herramientas de edición y análisis estático. La pregunta era deliberadamente distinta: si un procedimiento de biblioteca no contenía un defecto evidente, ¿podía el equipo demostrar que su implementación coincidía con el comportamiento aritmético previsto?

La firma construyó un ejecutor mínimo de Miden VM en Lean. Lean es un demostrador interactivo de teoremas cuyo pequeño núcleo de confianza verifica si una prueba enviada se sigue de sus definiciones y supuestos. Claude también ayudó a crear un traductor de procedimientos MASM a representaciones de Lean.

Varios agentes trabajaron después en paralelo en pruebas de procedimientos. El modelo MASM Lean resultante contiene semántica ejecutable de la VM, procedimientos traducidos, soporte compartido para pruebas y teoremas individuales de corrección.

El repositorio enumera 95 pruebas de procedimientos verificadas: 31 para operaciones de 64 bits, 36 para operaciones de 128 bits, 17 para operaciones de 256 bits y 11 para operaciones de palabras. En conjunto, cubren las partes de aritmética binaria descritas por Trail of Bits.

No eran pruebas de que cada parte de Miden fuera segura. Abordaban propiedades de corrección definidas para procedimientos concretos. Ese límite es esencial porque un demostrador de teoremas verifica el teorema que se le proporciona, no la intención no expresada en la mente de un desarrollador.

Trail of Bits afirma que los revisores humanos se centraron por ello en auditar los enunciados de los teoremas. Si un agente demostraba un teorema que omitía una precondición crítica o expresaba un resultado incorrecto, la aceptación del núcleo por sí sola no haría que el software fuera correcto.

A alto nivel, muchos teoremas seguían un patrón reconocible. Dada una pila con entradas específicas, ejecutar un procedimiento debería terminar y dejar el resultado matemáticamente esperado en la parte superior. Los valores de pila no relacionados y propiedad del llamador deberían permanecer en las ubicaciones esperadas.

Esta presión de especificación expuso dos defectos que las pruebas unitarias existentes no detectaron. El primero afectaba a un procedimiento de rotación a la derecha de 64 bits llamado rotr. Se comportaba incorrectamente para entradas grandes por encima del primo Goldilocks cuando la cantidad de rotación era múltiplo de 32.

El primo Goldilocks define el campo utilizado por la VM, por lo que los valores cercanos o superiores a ese límite requieren una representación cuidadosa. Durante el trabajo de prueba, el teorema deseado no podía demostrarse sin añadir un supuesto que excluyera el caso problemático de desplazamiento.

Una prueba fallida no es automáticamente evidencia de un error de código. El teorema, el modelo o los lemas de apoyo también pueden estar equivocados. En este caso, la revisión manual de la obstrucción llevó al equipo al caso límite de la implementación.

El segundo error apareció en el procedimiento wrapping_mul de 256 bits. Trail of Bits afirma que eliminaba de la pila valores propiedad del llamador antes de devolver el control. Las pruebas ordinarias del resultado de la multiplicación podían aprobarse sin comprobar la preservación del estado circundante de la pila.

Ese defecto muestra por qué importan las postcondiciones precisas. Un procedimiento puede calcular la respuesta numérica correcta mientras vulnera su contrato de llamada. En una máquina de pila, dañar el estado adyacente puede afectar a la ejecución posterior incluso cuando el elemento superior parece correcto.

Las pruebas unitarias siguen desempeñando un papel central. Se ejecutan rápidamente, protegen contra regresiones conocidas y cubren comportamientos de integración que quizá aún no cuentan con un modelo formal. El esfuerzo en Lean proporcionó un tipo distinto de garantía sobre propiedades expresamente declaradas.

La ventaja clave fue composicional. Los agentes podían producir intentos de prueba a escala, mientras que el núcleo de Lean rechazaba derivaciones no válidas. Los humanos no tenían que confiar en la seguridad expresada en prosa por un modelo. Debían examinar las definiciones y confirmar que los teoremas aceptados representaban las garantías previstas.

Este es un límite de control más sólido que pedir a otro modelo de lenguaje que determine si el código generado parece correcto. No elimina el juicio humano, pero desplaza ese juicio hacia las especificaciones y los supuestos.

Para los líderes de ingeniería, el caso sugiere una división práctica del trabajo. Los agentes pueden generar andamiaje repetitivo de pruebas, traductores y lemas candidatos. Los especialistas humanos deciden qué debe demostrarse e investigan por qué fallan las afirmaciones importantes.

El resultado no hace fiables las auditorías autónomas

El proyecto respalda la ingeniería de auditoría asistida por agentes, no la certificación de seguridad sin supervisión.

Trail of Bits plantea directamente el cambio económico. Unos años antes, le habría resultado difícil justificar meses de herramientas exploratorias para un solo encargo. Estos proyectos paralelos tenían resultados inciertos y eran difíciles de vender antes de que su valor fuera visible.

La firma sostiene que los agentes redujeron suficientemente el coste de la exploración como para cambiar ese cálculo. Los experimentos fallidos cuestan cada vez más tokens y tiempo de supervisión, en lugar de una asignación completa de trabajo de ingeniería especializado.

Esta afirmación merece una lectura cuidadosa. Aun así transcurrieron seis meses antes de la auditoría, y solo el decompilador acumuló más de 100 commits generados por IA. El relato público no ofrece una comparación controlada de horas de personal, costes totales de modelos o rendimiento de detección de defectos frente a un encargo convencional.

Tampoco establece que los agentes puedan construir herramientas equivalentes para todos los lenguajes inusuales. MASM ofrecía propiedades favorables para el análisis y el modelado formal. La Miden VM cuenta con un conjunto compacto de instrucciones, y muchas operaciones evitan efectos secundarios complejos.

Incluso dentro de este objetivo favorable, el decompilador no podía cubrir con seguridad todos los procedimientos. Trail of Bits redujo su subconjunto admitido porque los efectos de pila inconsistentes y las firmas ausentes hacían inviable una decompilación completa y fiable.

El flujo de trabajo de Lean tenía otra limitación. Las pruebas verificadas por el núcleo establecen únicamente el teorema declarado bajo la semántica modelada. Una instrucción mal traducida, un modelo incompleto de la VM o un teorema débil pueden mantener una brecha entre el comportamiento demostrado y el despliegue real.

La revisión humana se mantuvo visible durante todo el proceso. Los auditores revisaron código generado por agentes, convirtieron regresiones en pruebas, inspeccionaron enunciados de teoremas y analizaron pruebas fallidas. Claude y Codex alternaron entre desarrollo y revisión, en lugar de operar como una autoridad no observada.

Esto hace más precisa la comparación principal. La revisión directa por IA pide a un modelo que reconozca vulnerabilidades en una representación existente. Los agentes de creación de herramientas ayudan a los expertos a construir una representación en la que las restricciones ausentes, los tipos no válidos y las postcondiciones incorrectas se hagan explícitos.

Ninguno de los enfoques debería funcionar por sí solo. Los modelos pueden plantear hipótesis que los analizadores estáticos no codifican. El análisis estático puede cubrir rutas de ejecución que un revisor probabilístico podría pasar por alto. La prueba formal puede entonces abordar propiedades seleccionadas con un estándar verificable por máquina.

El proceso también crea obligaciones de mantenimiento. Los analizadores sintácticos deben seguir los cambios del lenguaje. Los analizadores necesitan suites de regresión. Los modelos formales deben permanecer alineados con la semántica de la VM. Las herramientas generadas que quedan obsoletas pueden crear una falsa sensación de seguridad.

Trail of Bits informa que el equipo de Miden adoptó el motor de análisis estático para futuras actualizaciones de la biblioteca central. Esta es una señal importante porque lleva las herramientas más allá de una única instantánea de auditoría. El uso continuado pondrá a prueba si el analizador sigue siendo útil a medida que evolucionan el lenguaje y la biblioteca.

Las organizaciones que consideren un flujo de trabajo similar también deberían planificar la procedencia. Los equipos necesitan saber qué modelo generó un cambio, qué humano lo revisó, qué pruebas se ejecutaron y qué supuestos se incorporaron a una prueba. Un flujo de trabajo de ingeniería solo es tan revisable como los registros que se conservan a su alrededor.

Por tanto, la evidencia pública respalda una conclusión acotada. Los agentes hicieron viable un ambicioso programa de preparación para este encargo. La garantía de seguridad siguió procediendo del sistema combinado de expertos del dominio, pruebas, análisis explícitos y verificación de pruebas.

Ese sistema es más interesante que la afirmación de que una IA encontró un error. Ofrece un modelo concreto para usar agentes imperfectos sin tratar su confianza como evidencia.

Tres señales pondrán a prueba si este modelo de auditoría perdura

La siguiente prueba es si las herramientas de garantía creadas por agentes siguen siendo correctas, adoptadas y productivas después de los hallazgos principales.

La primera señal es la integración continuada del analizador MASM en el proceso de desarrollo de Miden. Trail of Bits afirma que el equipo de Miden adoptó el motor de análisis estático para futuros cambios en la biblioteca central. El uso rutinario en integración continua reforzaría el argumento de que las herramientas de auditoría pueden convertirse en infraestructura preventiva.

La medida importante no es cuántas advertencias emite. Es si los nuevos procedimientos públicos reciben la validación requerida antes del lanzamiento y si las actualizaciones del analizador siguen los cambios en la semántica de MASM. Los falsos positivos persistentes o los modelos obsoletos debilitarían el resultado.

La segunda señal es la ampliación y el mantenimiento de las 95 pruebas de Lean. Los procedimientos verificados adicionales demostrarían que el modelo inicial permite trabajo continuo en lugar de una demostración fija. Los cambios en el código aritmético existente también deberían activar actualizaciones o fallos de las pruebas.

Observe el límite entre el código traducido y las especificaciones revisadas manualmente. La automatización que aumente el número de pruebas sin fortalecer la cobertura de los teoremas no ofrecería la misma garantía. La documentación clara de los supuestos importará tanto como el total bruto.

La tercera señal es la replicación por otros equipos de auditoría y ecosistemas de lenguajes. Miden presentaba una combinación inusualmente adecuada: un lenguaje personalizado, herramientas inexistentes, semántica explícita de pruebas y meses de tiempo de preparación.

Un patrón repetido en diferentes zkVMs o lenguajes de bajo nivel respaldaría la afirmación económica más amplia de Trail of Bits. No lograr reproducirlo en sistemas con concurrencia, memoria compleja o grandes grafos de dependencias revelaría sus límites.

La auditoría de Miden de Trail of Bits ya ha producido más que un flujo de trabajo especulativo. Entregó una integración de editor, decompilador, analizador, modelo de VM, pruebas verificadas y hallazgos concretos de seguridad.

La cuestión duradera es si los equipos pueden mantener esos artefactos alineados con los sistemas que protegen. Los desarrolladores que evalúan la seguridad asistida por agentes deberían examinar los repositorios, revisar los supuestos modelados y preguntarse dónde los controles verificables por máquina sustituyen a la confianza en el modelo. Ese es el estándar que vale la pena llevar a la próxima auditoría.