Microsoft Research представила Magnetar: доказательство работы программ на Rust, Go и C в 10-39 раз быстрее аналогов

Microsoft Research опубликовала в своём блоге рассказ о Magnetar, виртуальной машине с нулевым разглашением (zero-knowledge virtual machine, zkVM). Она доказывает выполнение программ для открытой процессорной архитектуры RISC-V: разработчик пишет программу на Rust, Go или C, компилирует её как обычно, и Magnetar доказывает её выполнение в том виде, как она написана.

Идея в том, что вместе с результатом программа выдаёт короткое криптографическое доказательство: эта программа на этих входных данных дала именно этот результат. Проверить его можно за миллисекунды, не запуская программу заново и не доверяя тому, кто её выполнял. Благодаря свойству нулевого разглашения доказательство не раскрывает входные данные, которые должны остаться приватными. В качестве возможных применений авторы поста называют ИИ-агента, который мог бы прикладывать доказательство того, что каждое его действие соответствовало заданной политике, и регулируемые финансовые организации, которые могли бы доказывать корректную обработку транзакций, не публикуя их.

По словам Microsoft Research, широкому применению мешали три нерешённые одновременно проблемы. Первая, эффективность: получение доказательства исторически требовало в миллионы раз больше вычислений, чем сама программа, а самые быстрые системы добивались скорости ценой компромиссов. Вторая, универсальность и удобство: многим системам нужно вручную переписывать программу в криптографическую схему (фиксированное арифметическое описание именно этого вычисления), что занимает месяцы, а любое изменение приложения требует новой схемы. Третья, безопасность: многие системы опираются на эллиптические кривые, которые может взломать достаточно мощный квантовый компьютер; постквантовые системы бывают основаны на решётках или на новых криптографических функциях, не прошедших десятилетий проверки, а часть из них, на недоказанных гипотезах о кодах, исправляющих ошибки. Microsoft в этой связи упоминает свою программу Quantum Safe Program и цель перевести продукты и сервисы на постквантовую криптографию к 2029 году (срок недавно приблизили).

Заявленные характеристики Magnetar. Скорость: 7,2-8,7 млн процессорных инструкций в секунду на ноутбуке. На 15 тестовых программах, от криптографического хеширования до переводов токенов внутри небольшого интерпретатора виртуальной машины Ethereum (EVM), система в среднем в 10-39 раз быстрее самых быстрых существующих zkVM на том же компьютере, а на тесте с переводом токенов более чем в 300 раз быстрее двух других систем. Оптимизированная версия обрабатывает 9,5-12,8 млн циклов в секунду, что, по тексту, повышает каждое из приведённых ускорений примерно в 1,3 раза. Доказательства проверяются примерно за 12 миллисекунд.

Безопасность: Magnetar зависит только от стандартной хеш-функции вроде SHA-256 или SHA-3. Ему не нужны эллиптические кривые, решётки, специализированные хеш-функции, доверенная настройка (trusted setup) и недоказанные гипотезы о кодах, исправляющих ошибки.

Проверка доказательства Magnetar состоит в основном из вычисления стандартных хеш-функций и арифметики в двоичных полях, тех самых операций, которые система эффективно доказывает. Поэтому проверка доказательства для неё обычная рабочая нагрузка. Это позволяет доказывать вычисления любого размера по частям, а затем объединять части, и доказывать долгоживущие системы вроде реестра или блокчейна.

Пост также рассказывает о более чем десятилетней предыстории: Spartan (2019) вернул подход sum-check к универсальным программам без доверенной настройки; Phalanx (2021) использовал повторяемость тактов процессора и ускорил доказательство примерно на порядок по сравнению со Spartan, на этой идее построено описание процессора в Magnetar; Brakedown (2021) дал первый вариант Spartan на стандартных хеш-функциях; работы Nova, HyperNova, NeutronNova, Neo и SuperNeo научили сворачивать частичные результаты; Spice, Lasso, Nebula, Twist and Shout и Jolt удешевили доказательство операций с памятью и целого процессора; Vega применил эту линию к цифровой идентификации (доказательство фактов из государственного удостоверения менее чем за десятую долю секунды); BinarySpartan перенёс Spartan в двоичные поля. Полное описание конструкции, анализ безопасности и измерения, по словам авторов, даны в техническом отчёте.

В конце Microsoft Research выражает ожидание, что технологические руководители перестанут спрашивать, практичны ли доказательства выполнения, и будут решать, какие результаты проверять, а не принимать на веру.

Ключевые факты

• Magnetar, zkVM от Microsoft Research: доказывает выполнение RISC-V-программ, скомпилированных из Rust, Go или C, без ручного переписывания в криптографическую схему.
• По данным поста, на 15 тестовых программах система в среднем в 10-39 раз быстрее самых быстрых существующих zkVM на том же компьютере; на тесте с переводом токенов, более чем в 300 раз быстрее двух других систем.
• Базовая версия доказывает 7,2-8,7 млн инструкций в секунду на ноутбуке; оптимизированная, 9,5-12,8 млн циклов в секунду (около 1,3 раза к каждому ускорению); проверка доказательства занимает около 12 миллисекунд.
• Безопасность опирается только на стандартные хеш-функции (SHA-256, SHA-3): без эллиптических кривых, решёток, специальных хеш-функций, доверенной настройки и недоказанных гипотез о кодах.
• Все цифры взяты из блога самой лаборатории; названия конкурирующих систем и модель ноутбука в посте не указаны.

Почему это важно

Доказательства с нулевым разглашением известны с 1980-х годов, но, как пишет Microsoft Research, не стали универсальным инструментом из-за трёх проблем: высокой цены вычислений, необходимости переписывать программы в специальные схемы и зависимости от криптографии, которой нельзя доверять на десятилетия вперёд. Magnetar заявлен как система, которая продвигается по всем трём направлениям сразу: принимает обычный код, быстрее предшественников и использует только стандартные хеш-функции. Если заявленное подтвердится, проверяемые вычисления станут доступнее обычным инженерам. Это пока позиция лаборатории, а не независимый вывод.

Кому это важно

Прежде всего разработчикам и исследователям в области криптографии и проверяемых вычислений, а также командам, которым нужно доказывать корректность работы программы третьей стороне: блокчейн-проектам (в тестах участвует интерпретатор EVM), финансовым организациям и разработчикам ИИ-агентов. Последние два сценария в посте описаны лишь как возможные в будущем.

Как это применить

Согласно посту, разработчик пишет программу на Rust, Go или C, компилирует её как обычно, и Magnetar доказывает её выполнение через RISC-V. Сроки выхода, открытость кода, продуктовые планы и цены в тексте не названы. Лаборатория приглашает заинтересованных обсудить свои сценарии применения, а полные детали конструкции и измерений отсылает к техническому отчёту.

Можно ли доверять

Источник, блог самой Microsoft Research, и все цифры (ускорение в 10-39 раз, более 300 раз на одном тесте, 7,2-8,7 млн инструкций в секунду, проверка за 12 мс), её собственные. В посте не названы конкурирующие системы, не указана модель ноутбука и не уточнено, какое именно среднее лежит в основе диапазона 10-39 раз. Независимой или рецензируемой оценки в тексте не упоминается; технический отчёт указан, но его название и площадка не приведены. Ускорение и скорость 7,2-8,7 млн инструкций относятся к базовой версии, эффект оптимизации (около 1,3 раза) указан отдельно.

Риски и подводные камни

Диапазон ускорения получен на 15 тестовых программах, и выбор тестов и систем для сравнения определила сама лаборатория, поэтому на ваших задачах результат может отличаться. Исторически получение доказательства требовало в миллионы раз больше вычислений, чем сама программа; насколько сильно эти накладные расходы снижены у Magnetar в абсолютных терминах, из поста напрямую не следует. Применение к ИИ-агентам и финансам в тексте описано условно, а сроки, когда доказательства станут рутинными, не названы.

«Результату больше не нужно доверять из-за того, кто его выдал. Его можно проверить благодаря тому, что к нему приложено.»

— Блог Microsoft Research, пост о Magnetar