Расширенная формальная проверка доказательств с нулевым разглашением: как доказать память с нулевым разглашением

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

Хотя мы показали процесс проверки инструкции zkWasm и представили предварительные концепции соответствующего проекта, читателям, знакомым с формальной проверкой, может быть больше интересно понять проверку zkVM с другими меньшими системами ZK или другими типами уникальных байт-кодов виртуальных машин. на. В этой статье мы подробно обсудим некоторые технические моменты, возникающие при проверке подсистемы памяти zkWasm. Память — самая уникальная часть zkVM, и ее обработка имеет решающее значение для всех других проверок zkVM.

Формальная проверка: виртуальная машина (VM) и виртуальная машина ZK (zkVM)

Наша конечная цель — проверить корректность zkWasm, что аналогично теореме корректности обычных интерпретаторов байт-кода (VM, таких как интерпретатор EVM, используемый узлами Ethereum). То есть каждый шаг выполнения интерпретатора соответствует допустимому шагу, основанному на операционной семантике языка. Как показано на рисунке ниже, если текущее состояние структуры данных интерпретатора байт-кода — SL, и это состояние помечено как состояние SH в спецификации высокого уровня машины Wasm, то когда интерпретатор переходит в состояние SL', происходит должно быть соответствующее легальное состояние высокого уровня SH', а спецификация Wasm предусматривает, что SH должен перейти в SH'.

Аналогично, в zkVM есть аналогичная теорема корректности: каждая новая строка в таблице выполнения zkWasm соответствует допустимому шагу, основанному на операционной семантике языка. Как показано на рисунке ниже, если текущее состояние строки структуры данных в таблице выполнения — SR, и это состояние выражается как состояние SH в высокоуровневой спецификации машины Wasm, то состояние следующей строки таблицы выполнения SR' должно соответствовать состоянию высокого уровня SH', а спецификация Wasm предусматривает, что SH должен перейти к SH'.

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

Во-первых, как мы заявляли в предыдущем сообщении в блоге, средство доказательства zk, по сути, представляет собой целочисленную операцию по модулю больших простых чисел, тогда как спецификация Wasm и обычный интерпретатор обрабатывают 32-битные или 64-битные целые числа. Большая часть реализации zkVM предполагает это, поэтому при проверке также необходимо выполнить соответствующую обработку. Однако это «локальная» проблема: каждая строка кода усложняется из-за арифметических операций, которые ей приходится обрабатывать, но общая структура кода и доказательства не меняется.

Еще одно важное отличие заключается в том, как обрабатываются структуры данных динамического размера. В обычном интерпретаторе байт-кода память, стек данных и стек вызовов реализованы как изменяемые структуры данных. Аналогично, спецификация Wasm представляет память как тип данных с методами get/set. Например, интерпретатор EVM Geth имеет тип данных Memory, который реализован как массив байтов, представляющий физическую память, и записывается и считывается с помощью методов Set 32 ​​и GetPtr. Чтобы реализовать инструкцию сохранения памяти, Geth вызывает Set 32 ​​для изменения физической памяти.

func opMstore(pc *uint 64, интерпретатор *EVMInterpreter, область *ScopeContext) ([]byte, error) {

// извлекаем значение из стека

mStart, val :=scope.Stack.pop(),scope.Stack.pop()

scope.Memory.Set 32(mStart.Uint 64(), val)

вернуть ноль, ноль

}

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

Однако с zkVM ситуация усложняется.

Таблица памяти zkWasm и уровень абстракции памяти

В zkVM в таблице выполнения есть столбцы для данных фиксированного размера (аналогично регистрам в ЦП), но ее нельзя использовать для обработки структур данных динамического размера, которые реализуются путем поиска вспомогательных таблиц. Таблица выполнения zkWasm имеет столбец EID со значениями 1, 2, 3... и две вспомогательные таблицы, таблицу памяти и таблицу переходов, которые используются для представления данных памяти и стека вызовов соответственно.

Ниже приведен пример реализации программы вывода средств:

int баланс, сумма;

пустая функция () {

баланс = 100;

  сумма = 10;

баланс -= сумма; // отзывать

}

Содержание и структура таблицы выполнения достаточно просты. Он имеет 6 шагов выполнения (EID от 1 до 6), каждый шаг имеет строку, в которой указан его код операции (код операции) и, если инструкция представляет собой чтение или запись в память, ее адрес и данные:

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

Эта система памяти сильно отличается от обычного интерпретатора VM: таблица памяти не является изменяемой памятью, которая постепенно обновляется, а содержит историю всех обращений к памяти на протяжении всей трассировки выполнения. Чтобы упростить работу программиста, zkWasm предоставляет уровень абстракции, реализованный с помощью двух удобных функций ввода. Они есть:

alloc_memory_table_lookup_write_cell

и

Alloc_memory_table_lookup_read_cell

Его параметры следующие:

Например, код, реализующий инструкции по хранению памяти в zkWasm, содержит вызов функции write alloc:

let Memory_table_lookup_heap_write1 = распределитель

    .alloc_memory_table_lookup_write_cell_with_value(

"сохранить разрешение записи 1",

ограничение_строитель,

Ид,

переместить |____| Constant_from!(LocationType::Heap as u 64),

двигаться |мета| load_block_index.expr(meta),   // адрес

переместить |____| Constant_from!( 0),             // 32-битный

переместить |____| Constant_from!( 1),             // (всегда) включено

    );

пусть store_value_in_heap1 = Memory_table_lookup_heap_write1.value_cell;

Функция alloc отвечает за обработку ограничений поиска между таблицами и арифметических ограничений, связывающих текущий eid с записями таблицы памяти. Благодаря этому программисты могут обращаться с этими таблицами как с обычной памятью, а значение `store_value_in_heap1` присваивается адресу `load_block_index` после выполнения кода.

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

mtable_lookup_write(строка 1.eid, строка 1.store_addr, строка 1.store_value)

                       ⇐ (row 1.eid= 1 ∧ row 1.store_addr=balance ∧ row 1.store_value= 100 ∧ ...)

mtable_lookup_write(строка 2.eid, строка 2.store_addr, строка 2.store_value)

                      ⇐ (row 2.eid= 2 ∧ row 2.store_addr=amount ∧ row 2.store_value= 10 ∧ ...)

mtable_lookup_read(строка 3.eid, строка 3.load_addr, строка 3.load_value)

                      ⇐ ( 2

mtable_lookup_read(строка 4.eid, строка 4.load_addr, строка 4.load_value)

                      ⇐ ( 1

mtable_lookup_write(строка 6.eid, строка 6.store_addr, строка 6.store_value)

                      ⇐ (row 6.eid= 6 ∧ row 6.store_addr=balance ∧ row 6.store_value= 90 ∧ ...)

Структура формальной проверки должна соответствовать абстракциям, используемым в проверяемом программном обеспечении, чтобы доказательство могло следовать той же логике, что и код. Для zkWasm это означает, что нам необходимо проверить схему таблицы памяти и функции «выделить ячейку чтения/записи» как модуль, который взаимодействует как переменная память. При наличии такого интерфейса проверка каждой схемы инструкций может выполняться аналогично обычному интерпретатору, а дополнительная сложность ЗК инкапсулируется в модуле подсистемы памяти.

При проверке мы реализовали идею о том, что «таблицу памяти фактически можно рассматривать как изменяемую структуру данных». То есть напишите функцию `memory_at type`, которая полностью сканирует таблицу памяти и строит соответствующее отображение адресных данных. (Диапазон значений переменной `type` здесь представляет собой три различных типа данных памяти Wasm: куча, стек данных и глобальные переменные.) Затем мы доказываем, что ограничения памяти, генерируемые функцией alloc, эквивалентны использованию set и получаем Функции изменения данных, произведенные соответствующим сопоставлением адресных данных. Мы можем доказать:

• Для каждого eid, если выполняются следующие ограничения

Memory_table_lookup_read_cell значение смещения типа eid

но

get (memory_at eid type) offset = Некоторое значение

• И если выполняются следующие ограничения

Memory_table_lookup_write_cell значение смещения типа eid

но

тип Memory_at (eid+ 1) = заданное значение смещения (memory_at eid type)

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

Механизм подсчета записи в память zkWasm

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

Если взять в качестве примера программу вывода средств, злоумышленник имеет возможность внедрить ложные данные в баланс счета, подделав операцию записи в память стоимостью 110 долларов перед операцией вывода средств. Этого процесса можно добиться, добавив строку данных в таблицу памяти и изменив значения существующих ячеек в таблице памяти и таблице выполнения. Это приведет к «бесплатному» выводу средств, поскольку после операции баланс счета все равно останется на уровне 100 долларов США.

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

Приведенное выше логическое утверждение несколько расплывчато, и в процессе механизированного доказательства его необходимо уточнить. Во-первых, нам нужно пересмотреть утверждение леммы о записи в память, упомянутое выше. Мы определяем функцию mops_at eid type для подсчета записей таблицы памяти с заданным eid и типом (большинство инструкций создают 0 или 1 запись в eid). Полная формулировка теоремы имеет дополнительное условие, утверждающее отсутствие ложных записей в таблице памяти:

Если выполняются следующие ограничения

 (значение смещения типа memory_table_lookup_write_cell eid)

И установлены следующие новые ограничения

 (mops_at тип eid) = 1 

но

 (memory_at(eid+ 1) type) = заданное значение смещения (memory_at eid type)

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

Чтобы доказать это, мы используем нисходящий подход для ограничения количества записей таблицы памяти, соответствующих данной инструкции, который включает в себя три шага. Сначала мы оцениваем количество записей, которые должны быть созданы для инструкций в последовательности выполнения, в зависимости от типа инструкции. Называем ожидаемое количество записей от i-го шага до конца выполнения `instructions_mops i` и соответствующее количество записей в таблице памяти от i-й инструкции до конца исполнения `cum_mops (eid i) `. Анализируя ограничения поиска каждой инструкции, мы можем доказать, что она создает не меньше записей, чем ожидалось, что приводит к выводу, что каждый отслеживаемый сегмент [i... numRows] создает не меньше записей, чем ожидалось:

Лемма cum_mops_bound': forall n i,

  0 ≤ я ->

  я + Z.of_nat n = etable_numRow ->

  MTable.cum_mops (etable_values ​​eid_cell i) (max_eid+ 1) ≥ Instructions_mops' i n.

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

Лемма cum_mops_equal': forall n i,

    0 ≤ я ->

    я + Z.of_nat n = etable_numRow ->

    MTable.cum_mops (etable_values ​​eid_cell i) (max_eid+ 1) ≤ Instructions_mops' i n ->

    MTable.cum_mops (etable_values ​​eid_cell i) (max_eid+ 1)  = Instructions_mops' i n.

Теперь приступайте к третьему шагу. Наша теорема корректности утверждает, что для любого n значения cum_mops и Instructions_mops всегда согласованы от строки n до конца таблицы:

Лемма cum_mops_equal: для всех n,

    0 <= Z.of_nat n <etable_numRow ->

  MTable.cum_mops (etable_values ​​eid_cell (Z.of_nat n)) (max_eid+ 1) = Instructions_mops (Z.of_nat n)

Проверка завершается подведением н. Первая строка в таблице — это ограничение равенства zkWasm, указывающее, что общее количество записей в таблице памяти правильное, т. е. cum_mops 0 = Instructions_mops 0 . Для следующих строк индуктивная гипотеза говорит нам:

cum_mops n = инструкции_mops n

и мы надеемся доказать

cum_mops (n+ 1) = Instruction_mops (n+ 1)

Обратите внимание здесь

cum_mops n = mop_at n + cum_mops (n+ 1)

и

инструкции_mops n = инструкции_mops n + инструкции_mops (n+ 1)

Следовательно, мы можем получить

mops_at n + cum_mops (n+ 1) = Instruction_mops n + Instruction_mops (n+ 1)

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

mops_at n ≥ инструкция_mops n.

Так что можно сделать вывод

cum_mops (n+ 1) ≤ Instructions_mops (n+ 1)

Здесь нам нужно применить вторую лемму выше.

(Используя аналогичную лемму для проверки таблицы переходов, можно доказать, что каждая инструкция вызова может точно создать запись в таблице переходов, поэтому этот метод доказательства в целом применим. Однако нам все еще нужна дополнительная работа по проверке, чтобы доказать, что возврат Корректность Возвращенный eid инструкции отличается от eid вызывающей инструкции, создавшей кадр вызова, поэтому нам также необходимо дополнительное инвариантное свойство, чтобы объявить, что значение eid увеличивается в одном направлении во время последовательности выполнения.)

Такое подробное описание процесса доказательства типично для формальной проверки и является причиной того, что проверка конкретного фрагмента кода часто занимает больше времени, чем его написание. Но стоит ли оно того? В данном случае это того стоило, потому что во время доказательства мы обнаружили критическую ошибку в механизме подсчета таблицы переходов. Эта ошибка была подробно описана в предыдущей статье. Короче говоря, более старые версии кода учитывали как инструкции вызова, так и возврата, и злоумышленник мог создать ложный переход, добавив дополнительные инструкции возврата в последовательность выполнения записей в таблице, освобождая место. . Хотя неправильный механизм подсчета может удовлетворять интуитивному представлению о том, что каждая инструкция вызова и возврата учитывается, возникают проблемы, когда мы пытаемся усовершенствовать это интуитивное представление до более точной формулировки теоремы.

Сделайте процесс доказательства модульным

Из приведенного выше обсуждения мы видим, что существует циклическая зависимость между доказательством схемы каждой инструкции и доказательством столбца счетчика таблицы выполнения. Чтобы доказать правильность схемы инструкций, нам нужно рассуждать о записи в память, то есть нам нужно знать количество записей таблицы памяти по определенному EID, и нам нужно доказать, что операции записи в память засчитываются в таблица выполнения верна; и это. Также необходимо доказать, что каждая инструкция выполняет хотя бы минимальное количество операций записи в память.

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

Теорема opcode_mops_correct_local_get : forall i,

  0 <= я ->

  etable_values eid_cell i > 0 ->

  opcode_mops_correct LocalGet i.

Теорема LocalGetOp_correct : для всех i st y xs,

  0 <= я ->

  etable_values enabled_cell i = 1 ->

  mops_at_correct i ->

  etable_values (ops_cell LocalGet) i = 1 ->

  state_rel i st ->

  wasm_stack st = xs ->

  (etable_values offset_cell i) > 1 ->

  nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Некоторые y ->

  state_rel (i+ 1) (update_stack (incr_iid st) (y : xs)).

Первое утверждение теоремы

opcode_mops_correct LocalGet i

В развернутом виде это означает, что инструкция создает по крайней мере одну запись таблицы памяти в строке i (число 1 указано в спецификации кода операции LocalGet zkWasm).

Вторая теорема представляет собой теорему о полной корректности инструкции, в которой цитируется

mops_at_correct я 

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

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

Подведем итог

Построчная проверка схем zkVM принципиально не отличается от проверки приложений ZK в других областях, поскольку обе они требуют аналогичных рассуждений об арифметических ограничениях. С точки зрения высокого уровня, проверка zkVM требует многих из тех же формальных методов проверки, которые используются в интерпретаторах и компиляторах языков программирования. Основное отличие здесь — состояние виртуальной машины с динамическим размером. Однако влияние этих различий можно свести к минимуму, тщательно структурировав структуру проверки в соответствии с уровнем абстракции, используемым в реализации, позволяя реализовать каждую инструкцию как независимый модуль на основе интерфейса get-set, как в обычном химическом интерпретаторе. проверка.