В этой серии статей о расширенной формальной проверке доказательств с нулевым разглашением мы обсудили, как проверять инструкции ZK, а также провели углубленный анализ двух уязвимостей ZK.
Как показано в общедоступном отчете (https://skynet.certik.com/projects/zkwasm) и репозитории кода (https://github.com/CertiKProject/zkwasm-fv), каждая инструкция 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' машины Wasm следующая строка в таблице выполнения должна соответствовать состоянию высокого уровня SH', а спецификация Wasm предусматривает, что SH должен перейти к SH'.
Видно, что спецификация состояний высокого уровня и шагов Wasm единообразна как в VM, так и в zkVM, поэтому она может опираться на предыдущий опыт проверки с помощью интерпретаторов или компиляторов языков программирования. Особенностью проверки zkVM является тип структуры данных, которая представляет собой низкоуровневое состояние системы.
Во-первых, как мы говорили в предыдущей статье, средство доказательства zk по существу представляет собой целочисленную операцию по модулю большого простого числа, тогда как спецификация Wasm и обычный интерпретатор работают с 32-битными или 64-битными целыми числами. Большая часть реализации zkVM предполагает это, поэтому при проверке также необходимо выполнить соответствующую обработку. Однако это «локальная» проблема: каждая строка кода усложняется из-за арифметических операций, которые ей приходится обрабатывать, но общая структура кода и доказательства не меняется.
Еще одно важное отличие заключается в том, как обрабатываются структуры данных динамического размера. В обычном интерпретаторе байт-кода память, стек данных и стек вызовов реализованы как изменяемые структуры данных. Аналогично, спецификация Wasm представляет память как тип данных с методами get/set. Например, интерпретатор EVM Geth имеет тип данных Memory, который реализован как массив байтов, представляющий физическую память, и записывается и считывается с помощью методов Set32 и GetPtr. Чтобы реализовать инструкцию хранения в памяти, Geth вызывает Set32 для изменения физической памяти.
func opMstore(pc *uint64, интерпретатор *EVMInterpreter,scope *ScopeContext) ([]byte, error) { // извлекаемое значение стека mStart, val :=scope.Stack.pop(),scope.Stack.pop() scope.Memory.Set32(mStart.Uint64(), &val) возвращает ноль, ноль}
В приведенном выше доказательстве корректности интерпретатора мы доказали, что его состояние высокого уровня и состояние низкого уровня совпадают после присвоения значений конкретной памяти в интерпретаторе и абстрактной памяти в спецификации. Это относительно легко.
Однако с zkVM ситуация усложняется.
Таблица памяти zkWasm и уровень абстракции памяти
В zkVM в таблице выполнения есть столбцы для данных фиксированного размера (аналогично регистрам в процессорах), но его нельзя использовать для обработки структур данных динамического размера, которые реализуются путем поиска вспомогательных таблиц. Таблица выполнения zkWasm имеет столбец EID со значениями 1, 2, 3... и две вспомогательные таблицы, таблицу памяти и таблицу переходов, которые используются для представления данных памяти и стека вызовов соответственно.
Ниже приведен пример реализации программы вывода средств:
int баланс, сумма;void main () {balance = 100; сумма = 10;баланс -= сумма; // отзывать}
Содержание и структура таблицы выполнения достаточно просты. Он имеет 6 шагов выполнения (от EID1 до 6), каждый шаг имеет строку, в которой указан его код операции (код операции) и, если инструкция представляет собой чтение или запись в память, ее адрес и данные:
Каждая строка в таблице памяти содержит адрес, данные, начальный EID и конечный EID. Начальный EID — это EID шага выполнения, который записывает данные по этому адресу, а конечный EID — это EID следующего шага выполнения, который будет записывать данные по этому адресу. (Он также содержит счетчик, который мы подробно обсудим позже.) Для схемы инструкции чтения памяти Wasm используется ограничение поиска, чтобы гарантировать наличие соответствующей записи в таблице, такой что EID инструкции чтения находится в диапазон от начала до конца Внутри. (Аналогично каждая строка таблицы переходов соответствует кадру стека вызовов, и каждая строка помечена EID шага инструкции вызова, который ее создал.)
Эта система памяти сильно отличается от обычного интерпретатора ВМ: вместо изменяемой памяти, которая постепенно обновляется, таблица памяти содержит историю всех обращений к памяти на протяжении всей трассировки выполнения. Чтобы упростить работу программиста, 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( "сохранить запись res1", ограничение_строитель, eid, перемещение |____| константа_from!(LocationType::Heap as u64), перемещение |meta| load_block_index.expr(meta), // перемещение адреса |____| Constant_from!(0), // 32-битное перемещение |____|constant_from!(1), // (всегда) включено );letstore_value_in_heap1=memory_table_lookup_heap_write1.value_cell;
Функция alloc отвечает за обработку ограничений поиска между таблицами и арифметических ограничений, которые связывают текущий eid с записями таблицы памяти. Благодаря этому программисты могут обращаться с этими таблицами как с обычной памятью, а значение store_value_in_heap1 присваивается адресу load_block_index после выполнения кода.
Аналогично инструкции чтения памяти реализуются с помощью функции read_alloc. В приведенном выше примере последовательности выполнения существует ограничение чтения для каждой инструкции загрузки и ограничение записи для каждой инструкции сохранения, и каждое ограничение удовлетворяется записью в таблице памяти.
Структура формальной проверки должна соответствовать абстракциям, используемым в проверяемом программном обеспечении, чтобы доказательство могло следовать той же логике, что и код. Для zkWasm это означает, что нам необходимо проверить схему таблицы памяти и функции «выделить ячейку чтения/записи» как модуль, который взаимодействует как переменная память. При наличии такого интерфейса проверка каждой схемы инструкций может выполняться аналогично обычному интерпретатору, а дополнительная сложность ЗК инкапсулируется в модуле подсистемы памяти.
При проверке мы реализовали идею о том, что «таблицу памяти фактически можно рассматривать как изменяемую структуру данных». То есть напишите функцию типа Memory_at, которая полностью сканирует таблицу памяти и строит соответствующее отображение адресных данных. (Диапазон значений типа переменной здесь представляет собой три различных типа данных памяти Wasm: куча, стек данных и глобальные переменные.) Затем мы доказываем, что ограничения памяти, генерируемые функцией alloc, эквивалентны использованию функций set и get для установите соответствующие адреса. Изменения данных, внесенные путем сопоставления данных. Мы можем доказать:
Для каждого eid, если выполняются следующие ограничения
Memory_table_lookup_read_celleidtypeoffsetvalue
но
get(memory_ateidtype)offset=Некоторое значение
И если выполняются следующие ограничения
Memory_table_lookup_write_cell значение смещения типа eid
но
тип Memory_at (eid+1) = заданное значение смещения (тип memory_at eid)
После этого проверка каждой инструкции может быть основана на операциях получения и установки на карте адресных данных, аналогично интерпретаторам байт-кода, не использующим ZK.
Механизм подсчета записи в память zkWasm
Однако приведенное выше упрощенное описание не раскрывает все содержимое таблицы памяти и таблицы переходов. В рамках zkVM злоумышленники могут манипулировать этими таблицами. Злоумышленники могут легко манипулировать инструкциями по загрузке памяти и возвращать произвольные значения, вставляя строку данных.
На примере программы вывода средств злоумышленник имеет возможность внедрить ложные данные в баланс счета, подделав операцию записи в память на сумму 110 долларов США перед операцией вывода средств. Этого процесса можно добиться, добавив строку данных в таблицу памяти и изменив значения существующих ячеек в таблице памяти и таблице выполнения. Это приведет к «бесплатному» выводу средств, поскольку после операции баланс счета останется на уровне 100 долларов США.
Чтобы гарантировать, что таблица памяти (и таблица переходов) содержит только действительные записи, созданные фактически выполненными инструкциями записи в память (а также вызова и возврата), zkWasm использует специальный механизм подсчета для отслеживания количества записей. В частности, в таблице памяти есть специальный столбец, в котором отслеживается общее количество записей, записанных в память. В то же время таблица выполнения также содержит счетчик для подсчета количества операций записи в память, ожидаемых для каждой инструкции. Убедитесь, что два счетчика согласованы, установив ограничение равенства. Логика этого метода очень интуитивно понятна: каждый раз, когда в памяти производится операция записи, она будет засчитана один раз, и в таблице памяти должна быть соответствующая запись. Таким образом, злоумышленник не может вставить какие-либо дополнительные записи в таблицу памяти.
Приведенное выше логическое утверждение несколько расплывчато, и в процессе механизированного доказательства его необходимо уточнить. Во-первых, нам нужно пересмотреть утверждение леммы о записи в память, упомянутое выше. Мы определяем функцию mops_at eid type для подсчета записей таблицы памяти с заданным eid и типом (большинство инструкций создают 0 или 1 запись по eid). В полной формулировке теоремы есть дополнительное условие, утверждающее, что в таблице памяти нет ложных записей:
Если выполняются следующие ограничения
(memory_table_lookup_write_celleidtypeoffsetvalue)
И установлены следующие новые ограничения
(mops_ateidtype)=1
но
(memory_at(eid+1)type)=set(memory_ateidtype)offsetvalue
Это требует, чтобы наша проверка была более точной, чем в предыдущем случае. Простого вывода из ограничения равенства, согласно которому общее количество записей таблицы памяти равно общему количеству операций записи в память при выполнении, недостаточно для завершения проверки. Чтобы доказать правильность инструкции, нам нужно знать, что каждая инструкция соответствует правильному количеству записей в таблице памяти. Например, нам необходимо исключить возможность того, что злоумышленник может пропустить запись таблицы памяти для инструкции в последовательности выполнения и создать вредоносную новую запись таблицы памяти для другой несвязанной инструкции.
Чтобы доказать это, мы используем нисходящий подход для ограничения количества записей таблицы памяти, соответствующих данной инструкции, который включает в себя три шага. Сначала мы оцениваем количество записей, которые должны быть созданы для инструкций в последовательности выполнения, в зависимости от типа инструкции. Называем ожидаемое количество записей от i-го шага до конца выполнения инструкциями_mops i, а соответствующее количество записей в таблице памяти от i-й инструкции до конца выполнения cum_mops (eid i). Анализируя ограничения поиска каждой инструкции, мы можем доказать, что она создает не меньше записей, чем ожидалось, что приводит к выводу, что каждый отслеживаемый сегмент [i ... numRows] создает не меньше записей, чем ожидалось:
Лемма cum_mops_bound': forall n i, 0 ≤ i -> i + Z.of_nat n = etable_numRow ->MTable.cum_mops(etable_valueseid_celli)(max_eid+1)≥instructions_mops'in.
Во-вторых, если можно показать, что в таблице не больше записей, чем ожидалось, то в ней ровно столько записей, что очевидно.
Лемма cum_mops_equal': forall n i, 0 ≤ i -> i + 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_valueseid_celli)(max_eid+ 1)=instructions_mops'in.
Теперь приступайте к третьему шагу. Наша теорема корректности утверждает, что для любого n значения cum_mops и Instructions_mops всегда согласованы от строки n до конца таблицы:
Лемма cum_mops_equal : forall n, 0 <= Z.of_nat n < etable_numRow ->MTable.cum_mops(etable_valueseid_cell(Z.of_natn))(max_eid+1)=instructions_mops(Z.of_natn)
Проверка осуществляется путем суммирования н. Первая строка таблицы — это ограничение равенства zkWasm, указывающее, что общее количество записей в таблице памяти правильное, т. е. cum_mops 0 = Instructions_mops 0. Для следующих строк индуктивная гипотеза говорит нам:
cum_mopsn=instructions_mopsn
и мы надеемся доказать
cum_mops (n+1) = инструкции_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, и нам нужно доказать, что операции записи в память засчитываются в таблица выполнения верна; и это. Также необходимо доказать, что каждая инструкция выполняет хотя бы минимальное количество операций записи в память.
Кроме того, есть еще один фактор, который необходимо учитывать. Проект zkWasm довольно большой, поэтому работу по проверке необходимо разбить на модули, чтобы несколько инженеров по проверке могли разделить работу. Поэтому при деконструкции доказательства счетного механизма необходимо обратить особое внимание на его сложность. Например, для инструкции LocalGet существуют следующие две теоремы:
Теорема opcode_mops_correct_local_get : forall i, 0 <= i -> etable_values eid_cell i > 0 -> opcode_mops_correct LocalGet i.
Теорема LocalGetOp_correct : forall i st y xs, 0 <= i -> 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)) = Some y ->state_rel(i+1)(update_stack(incr_iidst)(y::xs)).
Первое утверждение теоремы
opcode_mops_correct LocalGet i
В развернутом виде это означает, что инструкция создает по крайней мере одну запись таблицы памяти в строке i (число 1 указано в спецификации кода операции LocalGet zkWasm).
Вторая теорема представляет собой теорему о полной корректности инструкции, в которой цитируется
mops_at_correct я
В качестве гипотезы это означает, что инструкция создает ровно одну запись таблицы памяти.
Инженер по верификации может доказать эти две теоремы независимо, а затем объединить их с доказательством таблицы выполнения, чтобы доказать правильность всей системы. Стоит отметить, что все доказательства для отдельных инструкций можно выполнить на уровне ограничений чтения/записи, не зная конкретной реализации таблицы памяти. Таким образом, проект разделен на три части, с которыми можно работать независимо.
Подведем итог
Построчная проверка схем zkVM принципиально не отличается от проверки приложений ZK в других областях, поскольку обе они требуют аналогичных рассуждений об арифметических ограничениях. С точки зрения высокого уровня, проверка zkVM требует многих из тех же формальных методов проверки, которые используются в интерпретаторах и компиляторах языков программирования. Основное отличие здесь — состояние виртуальной машины с динамическим размером. Однако влияние этих различий можно свести к минимуму, тщательно структурировав структуру проверки в соответствии с уровнем абстракции, используемым в реализации, позволяя реализовать каждую инструкцию как независимый модуль на основе интерфейса get-set, как в обычном химическом интерпретаторе. проверка.
