Trail of Bits построила ИИ-инструменты для аудита Miden VM и нашла критический баг
В конце 2025 года команда проекта Miden обратилась к security-фирме Trail of Bits с просьбой провести аудит части своей zero-knowledge VM перед запуском. Ревью охватывало core-библиотеку с криптографическими примитивами, написанную на собственном низкоуровневом ассемблере Miden assembly (MASM), языке стековой машины, для которого почти не существовало инструментов разработки: ни подсветки синтаксиса, ни LSP-сервера, ни линтеров.
Зная, что у неё есть около шести месяцев до начала ревью, команда Trail of Bits решила потратить это время на создание инструментария с помощью ИИ-агентов, а не сидеть в ожидании кода. За полгода агенты (в основном Claude, для планирования и разработки, и Codex, для код-ревью) построили с нуля: LSP-сервер и расширение для VS Code с подсветкой синтаксиса, переходом к определению и подсказками по процедурам; декомпилятор для MASM, потребовавший более 100 ИИ-сгенерированных коммитов за несколько месяцев (декомпиляция стековой машины на MASM сложна из-за неявных сигнатур процедур, нестандартной calling convention и того, что циклы и ветвления не обязаны быть stack-neutral); движок статического анализа, построенный поверх внутреннего представления декомпилятора и использующий абстрактную интерпретацию для отслеживания, какие значения на стеке проверены, а какие нет; и модель самой VM-исполнялки в Lean, формальном proof assistant.
Во время самого аудита эти инструменты помогли найти более 400 уникальных мест, где валидацию типов можно было улучшить, и одну уязвимость высокой степени серьёзности. Баг находился в процедуре mod_12289, которая берёт 64-битное число по модулю 12289: частное от prover'а проверялось как корректное 64-битное значение, а вот остаток перед передачей в 32-битную инструкцию u32overflowing_sub не проверялся вовсе. Подбирая частное и остаток так, чтобы они всё ещё проходили проверки вычитания, аудиторы показали, что mod_12289 можно заставить вернуть неверный остаток. Вредоносный прувер мог использовать это, чтобы подделывать подписи Falcon и выводить средства с любого аккаунта Miden, защищённого ключевой парой Falcon.
Отдельно команда проверила, можно ли формально доказать корректность процедур core-библиотеки, если багов в них нет. Агенты автоматически транслировали процедуры MASM в Lean и параллельно строили доказательства для как можно большего числа процедур; поскольку ядро Lean само проверяет корректность доказательств, аудиторам оставалось вручную проверять только формулировки теорем. В итоге эта работа дала 95 машинно проверенных доказательств корректности, покрывших все компоненты бинарной арифметики библиотеки, и попутно выявила два незаметных бага, которые не ловил обычный набор unit-тестов: некорректное поведение 64-битного циклического сдвига rotr на больших входах, когда сдвиг кратен 32, и потерю значений со стека в 256-битном умножении wrapping_mul.
Авторы поста подчёркивают, что такие «побочные» инструментальные проекты ещё год-два назад было бы трудно обосновать перед клиентом заранее: результат непредсказуем, а неудача стоила бы дорого. С агентами, способными вести подобные проекты при лёгком присмотре, неудачный побочный проект теперь стоит только токены. Команда Miden уже приняла движок статического анализа для защиты будущих обновлений своей core-библиотеки.
Ключевые факты
- В конце 2025 года команда Miden обратилась к Trail of Bits для аудита core-библиотеки своей zero-knowledge VM, написанной на собственном ассемблере MASM
- Перед началом ревью Trail of Bits полгода использовала ИИ-агентов Claude и Codex, чтобы с нуля построить LSP-сервер, декомпилятор (более 100 ИИ-коммитов), движок статического анализа и формальную модель VM в Lean
- Статический анализ нашёл более 400 мест с недостаточной валидацией типов и одну уязвимость высокой степени серьёзности, в процедуре mod_12289 не проверялся остаток, что позволяло подделывать подписи Falcon и выводить средства со счетов Miden
- Формальные доказательства в Lean (95 штук) покрыли всю бинарную арифметику библиотеки и попутно нашли два бага (в rotr и wrapping_mul), которые пропускали обычные unit-тесты
- Команда Miden внедрила разработанный для аудита движок статического анализа для защиты будущих обновлений своей библиотеки
Почему это важно
Пост показывает не просто «ИИ нашёл баги», а смену экономики аудита: полугодовой side-проект по созданию инструментов для незнакомого языка (MASM) стал оправдан именно потому, что агенты способны вести его с лёгким присмотром. Раньше такие исследовательские вложения было сложно продать клиенту заранее из-за непредсказуемого результата; теперь неудачный эксперимент стоит лишь токены, а не месяцы штатного времени.
Кому это важно
Прежде всего security-аудиторам и командам, работающим с криптографическим кодом на нестандартных языках и виртуальных машинах без готовой инфраструктуры разработки. Также полезно разработчикам zero-knowledge систем вроде Miden: пример показывает, как можно заранее готовить формальную верификацию критичных компонентов ещё до полноценного аудита.
Как это применить
Trail of Bits распределила роли между агентами: Claude отвечал за планирование и разработку (LSP-сервер, декомпилятор, движок анализа, Lean-модель), Codex, за код-ревью. Для контроля регрессий агенты декомпилировали случайные процедуры из библиотеки и сравнивали результат с оригиналом; найденные расхождения превращались в регрессионные тесты. Для формальной верификации агенты параллельно строили доказательства теорем в Lean, а аудиторы вручную проверяли только правильность формулировок теорем, полагаясь на автоматическую проверку самих доказательств ядром Lean.
Можно ли доверять
Материал опубликован самой Trail of Bits в собственном блоге, компания описывает свою же работу, что не отменяет ценности деталей, но стоит учитывать заинтересованность в демонстрации возможностей фирмы. Автор текста не назван (пост написан от первого лица множественного числа с одной личной репликой без подписи), а в источнике не сказано, был ли высокосерьёзный баг в mod_12289 исправлен до запуска Miden и запущена ли VM на момент публикации.
Риски и подводные камни
Найденная уязвимость была реальной и серьёзной: неаккуратная валидация остатка в модульной операции позволяла подделывать подписи Falcon и потенциально выводить средства со счетов, защищённых такими ключами. При этом сами авторы отмечают ограничения метода, декомпилятор MASM заведомо не может корректно разобрать все процедуры из-за неявных сигнатур, нестандартной calling convention и стек-эффектов, зависящих от ветвлений и итераций циклов, поэтому анализ намеренно ограничен подмножеством кода, которое можно декомпилировать надёжно.
«На что нам потратить время и токены, чтобы ревью выявило как можно больше багов в кодовой базе?»
— Trail of Bits