Trail of Bits использовала AI для создания инструментов и нашла уязвимость в Miden VM
Security auditing in the age of (good enough) AI
Trail of Bits подготовила аудит Miden zkVM, потратив шесть месяцев на создание с нуля силами AI-агентов LSP-сервера, декомпилятора, движка статического анализа и модели исполнителя на Lean. Инструменты выявили более 400 мест для улучшения валидации типов и критическую уязвимость в процедуре mod_12289, позволявшую подделать подписи Falcon и украсть средства. Формальная верификация дала 95 машинно-проверенных доказательств корректности и два скрытых бага.
Злоумышленник-прувер мог воспользоваться этим, чтобы подделать подписи Falcon и опустошить любой Miden-аккаунт, контролируемый парой ключей Falcon.