Trail of Bits usa IA para auditar la VM de conocimiento cero de Miden

Fuentes: Trail of Bits uses AI to audit Miden's zero-knowledge VM

Trail of Bits ha documentado cómo utilizó agentes de inteligencia artificial para desarrollar herramientas de auditoría personalizadas antes de revisar el código de la Miden VM, una máquina virtual de conocimiento cero. Durante seis meses, el equipo construyó desde cero un servidor LSP, un descompilador, un motor de análisis estático y un modelo formal en Lean para verificar la corrección del código. Estas herramientas identificaron vulnerabilidades críticas, como la posibilidad de que un probador malicioso forjara firmas de Falcon y robara fondos de los titulares de la cuenta. Además, el trabajo con Lean generó 95 pruebas de corrección verificadas por máquina. El proyecto se centró en la biblioteca central de Miden, escrita en un lenguaje de ensamblaje personalizado llamado MASM, que carecía de herramientas de desarrollo estándar. La complejidad del lenguaje, basado en una arquitectura de máquina de pila, dificultó la decompilación y el análisis estático, requiriendo inferencia de firmas y efectos de pila. La colaboración entre agentes de IA y humanos permitió crear un entorno de revisión robusto, demostrando que la IA no solo revisa código, sino que también construye la infraestructura necesaria para una auditoría profunda y segura.