Magnetar подтверждает корректность программ для вычислений общего назначения с помощью доказательств

Вычисления с доказательством

Любой результат работы компьютера вызывает вопрос: действительно ли программа выполнилась так, как заявлено, и выдала правильный ответ? Сейчас проверка часто требует доверять оператору, поставщику, контрагенту или агенту, а доверие подкрепляют договорами, аудитом и журналами.

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

Результат можно проверять по приложенному доказательству, а не по тому, кто его выдал. ИИ-агент, действующий от чьего-то имени, мог бы подтверждать, что каждое его действие соответствует заданным правилам. Финансовые организации могли бы доказывать корректность обработки транзакций, не раскрывая их. Для этого создание доказательства должно стать такой же обычной частью работы, как запуск программы.

Три главные задачи

Доказательства с нулевым разглашением придумали в 1980-х годах. Примерно тогда же появились идеи, позволяющие доказывать выполнение программ. Но широкому применению мешали три задачи, которые трудно было решить одновременно.

Эффективность. Исторически создание доказательства требовало в миллионы раз больше вычислений, чем запуск самой программы. Исследования постепенно снизили эту нагрузку, но самые быстрые системы добивались скорости ценой уступок в других областях.

Универсальность и удобство. Во многих системах разработчикам приходится вручную переписывать программу в виде криптографической схемы — фиксированного арифметического описания конкретных вычислений. Такая работа занимает месяцы. Любое изменение приложения требует новой схемы, а при переводе программы в это представление часто возникают ошибки безопасности. Универсальный подход позволяет доказывать выполнение обычного процессора — тогда можно подтвердить работу любой скомпилированной программы без переписывания. До недавнего времени за такую универсальность приходилось платить скоростью или безопасностью.

Безопасность. Надёжность доказательства зависит от криптографии, на которой оно построено. Многие системы используют эллиптические кривые, которые сможет взломать достаточно мощный квантовый компьютер. Microsoft решает эту проблему в рамках программы Quantum Safe: компания переводит продукты и сервисы на постквантовую криптографию и недавно перенесла целевой срок на 2029 год.

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

Более десяти лет исследований

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

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

В 2019 году появилась система доказательств с нулевым разглашением Spartan. Она вернулась к протоколу суммирования и позволила использовать его для универсальных программ без доверенной настройки. Spartan можно строить на разных криптографических компонентах; эта гибкость позже позволила создать систему, основанную только на хеш-функциях. Затем серия работ добавила остальные необходимые части:

Каждая из этих работ решила часть задачи. Magnetar объединяет их результаты.

Как работает Magnetar

Magnetar — виртуальная машина с доказательствами с нулевым разглашением, или zkVM. Она продвигает решение всех трёх задач: скорости, универсальности и безопасности.

Система доказывает выполнение программ на RISC-V — открытой архитектуре процессоров с развитыми компиляторами для всех распространённых языков. Разработчик пишет программу на Rust, Go или C, компилирует её привычным способом, а Magnetar доказывает выполнение в исходном виде. Бизнес-правила, дата-пайплайн или интерпретатор Ethereum Virtual Machine (EVM) — это обычная программа; инженеры, которые уже её поддерживают, могут доказывать её выполнение без переписывания. Создание доказательств перестаёт требовать узкой специализации.

Magnetar доказывает от 7,2 до 8,7 млн инструкций процессора в секунду на ноутбуке. На 15 бенчмарках — от хеширования до перевода токенов внутри небольшого интерпретатора EVM — она в среднем в 10–39 раз быстрее самых быстрых существующих zkVM на том же устройстве. В бенчмарке с переводом токенов Magnetar более чем в 300 раз быстрее двух других систем.

Оптимизированная версия Magnetar обрабатывает 9,5–12,8 млн циклов в секунду. Для неё каждый приведённый выше показатель ускорения примерно в 1,3 раза выше. Доказательства проверяются примерно за 12 миллисекунд.

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

Хеш-функции — одни из наиболее тщательно изученных криптографических инструментов. На них также основаны безсостоянийные хеш-подписи, которые NIST стандартизировал как консервативный постквантовый вариант. Если система должна оставаться надёжной ещё много десятилетий, использование только стандартных хеш-функций позволяет не включать в план переход на другую криптографию.

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

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

Источник: microsoft.com

В технической статье описаны устройство Magnetar, анализ безопасности и результаты измерений.

Дальнейшие планы

Magnetar позволяет строить доказательства с нулевым разглашением и проверяемые вычисления на уже используемой организациями криптографии, с подходящей для практики скоростью и на обычном коде. Цель — сделать криптографическое доказательство регулярным результатом вычислений. Microsoft Research ожидает, что технологические руководители будут меньше спрашивать, практичны ли доказательства выполнения программ, и больше — какие результаты следует проверять, а не принимать на веру.

Публикации

Авторы

Области исследований

Связанные лаборатории