Security-фирма Trail of Bits опубликовала отчёт об аудите zero-knowledge виртуальной машины Miden: за шесть месяцев подготовки агенты Claude и Codex построили с нуля четыре инструмента — LSP-сервер, декомпилятор, статический анализатор и формальную модель исполнителя на Lean. Эти инструменты нашли более 400 мест в публичном API без валидации типов и критическую уязвимость, позволявшую злонамеренному пруверу подделывать подписи Falcon и опустошать любой Miden-аккаунт с Falcon-ключом. Формальная верификация дала 95 машинно-проверенных доказательств корректности, а все четыре инструмента открыты на GitHub.

image
image

Что произошло

18 сентября 2026 года Trail of Bits опубликовала отчёт об аудите zkVM Miden, где подробно описана агентная подготовительная фаза проверки. За шесть месяцев агенты Claude и Codex построили с нуля четыре инструмента для языка Miden Assembly: LSP-сервер masm-lsp, декомпилятор masm-decompiler, созданный более чем сотней AI-коммитов, движок статического анализа masm-analysis на базе абстрактной интерпретации и формальную модель исполнителя виртуальной машины masm-lean на Lean. В связке эти инструменты нашли более 400 мест в публичном API, где значения не проходят валидацию типов, и критическую уязвимость в процедуре mod_12289: невалидированное значение remainder, подаваемое прувером через advice stack, позволяло злоумышленнику в роли прувера подделывать подписи Falcon и опустошать любой Miden-аккаунт с Falcon-ключом. Формальная верификация дала 95 машинно-проверенных доказательств корректности, покрывших всю бинарную арифметику core-библиотеки, и выявила два бага, пропущенных unit-тестами: неверный rotr на входах больше простого числа Goldilocks при shift, кратном 32, и потерю значений стека в wrapping_mul при 256-битном умножении.

Контекст

MASM — язык без экосистемы: у него не было ни IDE, ни LSP, ни линтеров, то есть базовой инфраструктуры, на которую опирается любой аудит кода. Исторически именно стоимость построения такого набора инструментов под один конкретный язык делала полноценную подготовку к аудиту запредельно дорогой, поэтому для экзотических рантаймов её обычно не проводили. Второй элемент контекста — zk-специфичная граница доверия: в zero-knowledge системах прувер подаёт часть входных данных через advice stack, и значение, принятое на этой границе без проверки, становится каналом атаки, а не просто неаккуратностью в коде. Третий элемент — методология: Claude использовался для планирования и разработки, Codex для код-ревью, а находки автоматически деградировали в regression-тесты, так что результат заземлён в детерминированные артефакты — статический анализатор, формальную модель исполнителя и тесты. Показательно, что формальные доказательства и unit-тесты поймали непересекающиеся классы дефектов: верификация дополняет тесты, а не дублирует их.

Почему это важно для индустрии

Для отрасли это сдвиг в экономике аудита безопасности. Кастомный tooling под экзотический язык, который раньше был неподъёмно дорог, теперь собирается за месяцы силами небольшой команды: агентные side-проекты вроде декомпилятора или Lean-модели обходятся в стоимость токенов плюс экспертное время на постановку задач и ревью. Это подрывает ценовой ров крупных аудит-фирм и открывает нишу вертикальных AI-security продуктов; ожидаются первые коммерческие офферы формата «AI-augmented audit» и давление на прайс аудитов экзотических языков. Второе следствие — переход от разового аудита к непрерывной верификации: Miden уже внедрил статический анализатор для проверки будущих обновлений core-библиотеки, превратив его в детерминированный гейт в CI. Если тренд удержится, proof-покрытие арифметики уровня core-библиотек может стать гигиеническим минимумом для криптографических виртуальных машин, а конкуренция между аудит-фирмами сместится к качеству агентных пайплайнов и экспертизы поверх них.

Почему это важно для пользователей

Для читателя это практический рецепт, а не новость про чужой успех. Все четыре инструмента открыты на GitHub: masm-lsp, masm-decompiler, masm-analysis и masm-lean можно изучить, применить к собственным zk- или WASM-проектам и повторить паттерн для своего языка без экосистемы. Сами агенты Claude и Codex доступны любому разработчику, поэтому связка, в которой один агент ведёт планирование и разработку, а второй делает код-ревью, воспроизводима без доступа к закрытым технологиям. Кейс подтверждает, что такая связка находит дефекты уровня потери средств, а не только замечания по стилю кода.

Что пока неизвестно / ограничения

Формула «стоит только токенов» требует оговорки: шесть месяцев подготовки — это время экспертов Trail of Bits, которые ставили агентам задачи, направляли их и ревьюили результаты, а из отчёта не следует, что связка Claude и Codex воспроизводится без сопоставимой экспертной нагрузки. Методологические метрики не раскрыты: в публикации нет стоимости в токенах и деньгах, доли человеческого надзора, частоты отказов агентов и уровня ложных срабатываний статического анализатора. Наконец, речь не о готовом продукте, а о наборе открытых компонентов: перенос методики на другой язык потребует собственной инженерной работы и экспертного времени на проверку находок.

Источники

Автор

Look at AI, редакция