vnTinyRAM

Продолжение руководств по zkSNARK

Недавно было опубликовано несколько руководств по современному уровню доказательств с нулевым разглашением. Кристиан Рейтвайсснер начал с поста в блоге Ethereum (pdf-версия). Но лучшая статья — это отличный пост в блоге Виталика Бутерина QAPs: От нуля до героя. Статья Виталика начинается с базового понимания математики на уровне старшей школы и направлена на создание доказательства того, что вы знаете ответ на простое уравнение (x³ + x + 5 = 35), но не раскрываете ответ (x = 3). Он великолепно написан, с диаграммами и примерами на каждом этапе.

Но доказывать, что вы знаете решения игрушечных уравнений, бессмысленно, не так ли? Как часто вы сталкиваетесь с такой проблемой в реальном мире? Я собираюсь сделать безумное предположение, что ответа никогда не будет.

В этой статье я объясню еще одну часть алгоритмов BCGTV zkSNARK — часть, которая преобразует реальные программы, решающие реальные задачи, в системы ограничений ранга 1. Я предполагаю, что вы сначала прочитали и (по крайней мере частично) поняли руководство Виталика. Однако этот будет менее сложным с математикой.

Зачем конвертировать программы в ограничения?

Но прежде чем я начну, давайте сделаем краткий обзор — почему мы должны заботиться о zkSNARK или о том, как для начала преобразовывать программы в уравнения?

Я не буду много писать о вариантах использования в этой статье, это тема для другого раза. Достаточно сказать, что доказательства с нулевым разглашением могут быть интегрированы в системы распределенного реестра, подобные Биткойну, для повышения их конфиденциальности, а также что они полезны и в других областях. Один мне кажется интересным — раскрытие анонимных подмножеств документов электронного паспорта как способ решения проблем Сибиллы в открытых p2p-сетях. Многосторонние вычисления также имеют много интересных вариантов использования в финансовой системе для совместного расчета полезной статистики.

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

Схемы

Для программиста естественный способ выразить доказательство — это обычная компьютерная программа, написанная на обычном языке, таком как C. Программа принимает секретные данные в качестве входных данных, возможно, также некоторые общедоступные данные («общедоступные» здесь означает совместно используемые с верификатор), проверяет их различными способами и возвращает либо ноль, либо единицу, чтобы указать успех или неудачу. Таким образом можно было бы выразить множество полезных доказательств.

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

Булевы схемы внешне напоминают электронные схемы: логические элементы — это AND, NOT, XOR и так далее. Арифметические схемы — это альтернативный способ выразить многочлены и использовать элементы сложения и умножения:

Эта схема вычисляет:

X₂(X₁ + X₂)(X₂ + 1)

Должно быть ясно, как преобразовать взад и вперед из этого вида представления в «сплющенную» форму, описанную в руководстве Виталика.

Хорошая вещь в мышлении в терминах вентилей и проводов состоит в том, что мы можем легко определить расширения от вентилей высокого уровня до более простых типов, и это помогает нам абстрагироваться от базовых примитивов. В статье Пиноккио: почти практически проверяемое вычисление (Парно, Джентри, Хауэлл и Райкова, 2013) объединенная исследовательская группа Microsoft / IBM объясняет, что, хотя их базовые схемы являются арифметическими, они также определяют разделенный вентиль , который преобразует входное число в двоичное представление, которое затем позволяет вам использовать логические элементы И, ИЛИ и И-НЕ для реализации таких вещей, как оператор ≥ — точно так же, как при проектировании физической электронной схемы. Конечно, есть также вентиль слияния, который преобразует набор двоичных проводов обратно в арифметический провод. Виталик кратко упоминает об этой технике, но Gentry et al. прямо изложите трансформации:

NAND(a,b) = 1 − ab AND(a,b) = ab OR(a,b) = 1 − (1 − a)(1 − b)

Вычитание здесь может быть реализовано как умножение на -1, а затем сложение. Обратите внимание, что в реальной схеме все вычисления выполняются по модулю большого числа (порядок конечного поля, но вам не нужно знать, что такое конечное поле прямо сейчас). Таким образом, все числа положительны: -1 — это просто порядок полей минус один. Не сильно отличается от обычной двоичной арифметики.

NAND является «универсальным вентилем» и может использоваться для создания любого вида вычислений — например, XOR может быть построен из 4 NAND:

Мы можем представить себе определение других полезных ворот, которые расширяются до более крупных комбинаций.

Оказывается, этого достаточно для компиляции языка, который очень похож на C, на самом деле, вы можете преобразовать подмножество C непосредственно в такие схемы, затем из схем в простые уравнения, из уравнений в ограничения ранга 1 и оттуда к QAP и, наконец, из QAP вы можете построить доказательство с нулевым разглашением. Документ Pinnochio не только описывает, как это сделать, но также содержит открытый исходный код для простого компилятора C-to-QAP. Это всего около 3500 строк Python.

Однако алгоритмы zkSNARK, реализованные в libsnark, не используют этот компилятор. Они используют гораздо более сложную технику. Очевидно, где-то есть загвоздка. В чем подвох?

Улов

Пинночио из милосердия относится к языку, который он позволяет программистам использовать как «подмножество» C. Вот некоторые вещи, отсутствующие в этом подмножестве:

Мутабельное состояние
… Без которого, конечно, не будет выделения памяти
У вас есть один скалярный тип: int, поэтому не стоит ожидать многого от строк или значений с плавающей запятой.
Арифметика указателей, включая возможность динамически индексировать массивы (т. Е. Индексировать их чем-то, что не является константой) или использовать указатели на указатели.
Циклы, зависящие от данных
Более или менее любая функция, не связанная с простыми манипуляциями с целыми числами.

Само собой разумеется, что вы никак не можете получить доступ к операционной системе.

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

int success = 0; _unroll = 5; for (int i = 0; i < input->num_things; i++) { if (input->thing[i] == 42) success = 1; }

сначала будет преобразован во что-то вроде этого:

int success1 = 0; int success2; int n = input->num_things; if (0 < n && input->thing[0] == 42) success2 = 1; if (1 < n && input->thing[1] == 42) success2 = 1; if (2 < n && input->thing[2] == 42) success2 = 1; if (3 < n && input->thing[3] == 42) success2 = 1; if (4 < n && input->thing[4] == 42) success2 = 1;

Обратите внимание, что переменная success была переименована: поскольку вы не можете изменить какое-либо состояние, переназначение переменной приводит к ее незаметному переименованию. Также _unrollin Pinnochio C — это волшебная переменная, которую компилятор понимает изначально.

Это подмножество, хотя и небольшое, все же достаточно для выполнения некоторых тривиальных вычислений, таких как SHA256. Но вы можете забыть взять любой C, написанный для обычного использования, и скомпилировать его вот так.

Перемотка вперед

В этой статье рассказывается, как перейти от обычных программ C к арифметическим схемам. Виталик рассказал, как перейти от схем к форме «квадратичной арифметической программы», а затем вычислить решение такой QAP.

Здесь есть совершенно другая теория о том, как перейти от решения для QAP к небольшому доказательству постоянного размера и постоянного времени, которое можно проверить. Я пропущу это здесь. Давайте на мгновение махнем рукой и скажем, как только у вас есть QAP от вашей программы, вы можете сделать некоторую магию и получить действительно крошечную структуру данных, которую можно использовать для проверки того, что программа определенно приняла введенные ею данные.

Вычисления RAM

Схемная модель вычислений, даже когда она частично скрыта простым компилятором C, очень ограничена. На самом деле мы хотим писать программы для чего-то похожего на обычный компьютер с процессором и памятью.

Это называется модель вычислений RAM. В этом контексте RAM не означает оперативную память, как вы можете себе представить, это означает машину с произвольным доступом и относится к ЦП с регистрами. Регистры — это не так много места для хранения: банки памяти также необходимы, чтобы позволить нам запускать что-то, приближенное к реальному C, поэтому в этой статье я буду использовать RAM в значении машина с регистрами и памятью. Терминология немного отличается от той, к которой вы привыкли, потому что многое из этого вытекает из изучения вычислительной сложности и унаследовало ее жаргон. Чтобы получить то, что мы хотим, нам нужен способ преобразовать программу, предназначенную для ОЗУ, в кучу схем.

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

Решение простое: мы просто собираемся смоделировать выполнение ЦП с помощью уравнений. Множество уравнений.

В серии статей Бен-Сассон, Кьеза, Генкин, Тромер и Вирза (BCGTV) представляют небольшой виртуальный ЦП под названием vnTinyRAM и показывают, как преобразовывать программы, которые нацелены на него, в схемы. В статье Краткое неинтерактивное нулевое знание для архитектуры фон Неймана представлена машина фон Неймана, которая представляет собой компьютер, в котором код и данные находятся в одной и той же памяти и могут обрабатываться одинаково. Если вы хотите прочитать эту статью, обратите внимание, что ошибка в ней была обнаружена и исправлена, что демонстрирует, почему потребуется некоторое время, пока лежащие в основе математические вычисления не будут широко изучены и достаточно надежны для использования в производственной среде. В 2014 году команда расширила свои методы в статье Масштабируемость нулевого знания с помощью циклов эллиптических кривых.

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

Поскольку vnTinyRAM является виртуальным, его легко перенастроить для использования регистров разного размера: он может быть 16- или 32-разрядным, в зависимости от ваших потребностей. Добавить новый набор инструкций, подобный этому, к обычным компиляторам довольно просто.

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

Такую трассировку легко создать, эмулируя этот крошечный ЦП в программном обеспечении на реальном компьютере и записывая каждый шаг. Затем уловка состоит в том, чтобы написать схему, которая может проверять правильность таких трассировок, и использовать эту схему для построения доказательства с нулевым разглашением, что мы знаем действительную трассировку для комбинации программы и наших личных данных (то, что мы пытаемся доказывать прочее). Итак, мы собираемся составить наши доказательства из большего количества доказательств. Доказательство действительности трассировки можно разбить на три части:

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

Мы можем представить схему, которая без особых проблем проверяет первую — такие инструкции, как ADD или MULL, преобразуются непосредственно в вентили. Более сложные инструкции, такие как UDIV (деление), похоже, не переводятся напрямую: у нас есть только ворота сложения и умножения! Но мы можем хитроумно обойти эту проблему, потребовав, чтобы фактический ответ был предоставлен на ленте вспомогательных советов, упомянутых ранее, а затем умножая их, прежде чем принять ответ. Этот трюк с использованием проверенных «советов» уменьшает размер необходимых схем и значительно ускоряет работу, а также упрощает код. Содержание этого «совета» контролируется доказывающим, который, конечно, может пытаться обманом заставить нас поверить во что-то ложное. Таким образом, ЦП не может многое предполагать о том, что там есть, но если проверка ответа требует меньше работы, чем его вычисление, мы выигрываем.

Реализация памяти

Математические уравнения не могут запоминать вещи: они всегда дают один и тот же ответ при одних и тех же входных переменных. Это создает проблему для моделирования банка памяти с их помощью.

Чтобы решить эту проблему, мы расширяем данные, помещаемые в состояния ЦП, записанные в трассировке выполнения. Давайте переопределим состояние процессора, чтобы оно означало:

Отметка времени, измеряемая в циклах (шагах) ЦП.
Корень дерева Меркла над содержимым внешней памяти.
Текущий счетчик программы и набор регистров
Флаг, обозначающий, приняла ли программа входные данные (т. Е. Решила, что то, что вы пытаетесь доказать, истинно)

Поскольку корень дерева Меркла — это всего лишь один хэш, состояние процессора может быть небольшим фрагментом данных постоянного размера независимо от того, сколько оперативной памяти используется. Когда ЦП требует, чтобы часть данных была загружена из памяти, это предоставляется в виде дополнительных советов на ленте рекомендаций вместе с путем аутентификации (ветвь Меркла), который показывает, что это значение действительно было правильно сохранено в памяти. Ветвь Меркла — это набор одноуровневых хэшей, необходимых для работы от листа дерева до корня с вычислением узлов на этом пути. По сути, это небольшое специальное доказательство того, что данный элемент был в дереве, когда он был вычислен.

Когда ЦП желает сохранить данные, он может выполнить загрузку и сохранение, чтобы запросить путь аутентификации старого значения, а затем использовать его для вычисления нового корня с учетом обновленного местоположения. Таким образом устанавливается связь между каждым шагом в трассировке выполнения.

Некоторые читатели уже знакомы с деревьями Меркла. Версия, описанная в статье Scalable Zero Knowledge, отличается от «обычных» деревьев тем, что в них не используется стандартный алгоритм хеширования, такой как SHA-256. Вместо этого они используют настраиваемую хэш-функцию, устойчивую к коллизиям, основанную на проблеме суммы подмножества, поскольку она гораздо более эффективно реализована в арифметических схемах того типа, который они используют.

Перезагрузка ЦП

Проснувшийся читатель заметит, что мы, похоже, ничего не добились: мы пошли по этому пути, потому что вы не можете создавать циклы в схемах, и все же ЦП постоянно зацикливается при выполнении программы. Застрявший?! Не совсем!

В более ранних версиях этих методов было простое решение — как в примере с Pinnochio C, просто разверните процессор! В этой версии алгоритма при генерации универсальной схемы ЦП вы должны были выбрать размер регистра и максимальное время выполнения. Сгенерированная схема затем будет выполнять программы до этого предела. Схема, которая проверяет каждый шаг в трассировке ЦП, будет дублироваться снова и снова, с выходами одного шага, подключенными к входам следующего. Это привело к огромным вычислительным затратам. Кроме того, в более ранних работах не использовался подход дерева Меркла для аутентификации памяти: вместо этого они использовали проблемы маршрутизации по сетям Бенеша, что было намного сложнее.

В статье Scalable Zero Knowledge эта проблема решена с помощью излюбленного приема всех компьютерных ученых: рекурсии.

Сгенерированная схема vnTinyRAM реализует ровно один цикл процессора. В качестве входных данных он принимает предыдущее состояние ЦП, а также доказательство того, что предыдущее состояние было действительным. Он также принимает предполагаемое следующее состояние. Поскольку схема проверяет предыдущее доказательство и что переход действителен, подача схемы через алгоритмы SNARK выдает обновленное доказательство, которое затем может быть снова отправлено обратно в универсальную схему для запуска следующего тактового цикла.

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

Это форма передачи данных, имеющая множество интересных применений, помимо непосредственной проблемы доказательства следа выполнения ЦП.

Доказательства проверка доказательств проверка доказательств

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

По сложным причинам, я не буду здесь вдаваться в подробности, вы не можете просто закодировать проверочные вычисления непосредственно как набор ворот. Это было бы идеально, но, как вкратце упомянул Виталик в конце своего руководства, все вышеперечисленные вычисления не выполняются с использованием обычных чисел, которые мы учили в школе (ха-ха, это было бы слишком просто). Они происходят в контексте эллиптических кривых. Чтобы проверить значения внутри доказательства очевидным образом, вам понадобится эллиптическая кривая, которую математически невозможно построить. Тупик.

Вы также можете использовать трюк с разделением вентилей, чтобы преобразовать все значения доказательства в двоичные, а затем сделать это, как это сделал бы обычный ЦП, но это создало бы невероятно огромное количество вентилей и сделало бы все это непрактичным (мы настаиваем на границы практичности уже). Тоже тупик.

Итак, нам нужен еще один трюк, и он хитрый. Мы ищем пару эллиптических кривых. Доказательство первого цикла ЦП происходит с использованием первой эллиптической кривой и проверяется другой аналогичной схемой, использующей вторую. Затем второй цикл выводит доказательство, снова используя первую эллиптическую кривую. Таким образом, используемая кривая чередуется вперед и назад. Это позволяет избежать проблемы невозможности, а также избежать массового взрыва косвенности.

Если вы увлекаетесь криптовалютами, возможно, вы знаете эллиптическую кривую secp256k1. Ну есть много разных кривых. Семейство кривых, которые нам нужны для этого трюка с чередованием, называются кривыми Мияджи / Накабаяши / Такано или для краткости кривыми MNT. К сожалению, эллиптические кривые не лежат просто так, ожидая своего открытия. Они должны быть получены путем дорогостоящих вычислений. Команда BCGTV сделала это — за небольшую плату в 25 416 основных дней — и нашла пару кривых с необходимыми им свойствами. Параметры кривой указаны в их статье, поэтому больше никому не придется выполнять этот поиск.

Производительность и предостережения

У описанных выше алгоритмов есть интересное свойство: они требуют выполнения действительно обширных вычислений, но их нужно выполнить только один раз. После расчета схемы ЦП это универсальная схема, которую можно использовать для любой программы, использующей набор команд vnTinyRAM. Поскольку повторение ЦП занимает постоянное количество времени для каждого цикла, мы можем измерить, насколько быстро работает эта «проверка ЦП».

Готовы к этому?

На четырехъядерном компьютере каждый шаг будет стоить около 9 секунд. Это дает тактовую частоту 0,1 Гц. Достаточно сказать, что в ближайшее время вы не докажете, что Crysis работает.

Ясно, что впереди еще долгий путь. Но поскольку предыдущие методы даже не масштабировались линейно, это по-прежнему представляет собой огромный прогресс.

Осталась еще одна большая проблема. Я упомянул, что расчет универсальной схемы нужно производить один раз. Это не совсем так. Проблема заключается в той части, которую мы передали до сих пор. Задача преобразования решения QAP в быстро проверяемый zkSNARK включает использование «ключа подтверждения» и «ключа проверки», которые получены из некоторых случайных данных, выбранных тем, кто вычисляет схему. К сожалению, знания этих случайных данных достаточно для подделки доказательств. Это означает, что процесс настройки является слабым местом: как узнать, что случайные данные, использованные для инициализации алгоритмов, действительно были уничтожены? Независимо от того, сколько театра вы на это бросаете, в конце концов, вы не можете знать наверняка.

В 2016 году исследования переместились в сторону нового типа SNARK, который находится в так называемом «мире PCP» и не имеет этой проблемы. PCP — это вероятностно проверяемые доказательства, о которых мы поговорим в другой раз.

Заключение

Я надеюсь, что эта статья основывается на введении Виталика в основную математику в полезной форме. Нам нужно больше объяснений, чтобы закончить рассказ:

Перевод удовлетворенного QAP на фактическое доказательство с нулевым разглашением.
PCP и как их можно использовать по-разному по сравнению с используемыми libsnark алгоритмами.
Криптография на основе пар и способы их использования.

Это темы на другой день.

Благодарим Эрана Тромера и Эли Бен-Сассона за вычитку этой статьи.

Источник: ledsshop.ru