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

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

Что такое уязвимость ZK?

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

Для прувера zkVM процесс доказательства ZK включает в себя запуск программы, генерацию записей выполнения для каждого шага и преобразование этих записей выполнения в набор числовых таблиц (процесс, известный как «арифметизация»). Эти числа должны удовлетворять набору ограничений («схема»), которые включают отношения между конкретными ячейками таблицы, фиксированные константы, ограничения поиска в базе данных между таблицами и полиномиальные уравнения (или «вентили»), которым должна удовлетворять каждая пара смежных строк таблицы. Ончейн-верификация может подтвердить существование таблицы, которая соответствует всем ограничениям, не раскрывая конкретных чисел в таблице.

Таблица арифметизации в zkWasm

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

Схема ZK, которая обеспечивает соблюдение правил выполнения инструкций zkVM, чрезвычайно сложна. Для zkWasm реализация схемы ZK включает в себя более 6 000 строк кода Rust и сотни ограничений. Эта сложность часто означает, что может быть обнаружено несколько уязвимостей.

Архитектура схемы zkWasm

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

Уязвимость кода: атака с внедрением данных Load8

Первая уязвимость связана с инструкцией Load8 в zkWasm. В zkWasm чтение памяти кучи выполняется с помощью набора инструкций LoadN, где N — размер загружаемых данных. Например, Load64 должен считывать 64-битные данные с адреса памяти zkWasm. Load8 должен считывать 8-битные данные (т.е. один байт) из памяти и заполнять их нулями, чтобы создать 64-битное значение. Внутренне zkWasm представляет память в виде массива 64-битных байтов, поэтому ему нужно «выбрать» часть массива памяти. Это делается с помощью четырех промежуточных переменных (u16_cells), которые вместе образуют полное 64-битное значение нагрузки.

Ограничения для этих инструкций LoadN определены следующим образом:

Это ограничение делится на три варианта: Load32, Load16 и Load8. Load64 не имеет ограничений, так как единицы памяти равны 64 битам. Для случая Load32 код гарантирует, что старшие 4 байта (32 бита) в блоке памяти должны быть равны нулю.

Для случая Load16 код гарантирует, что старшие 6 байт (48 бит) в блоке памяти должны быть равны нулю.

Для случая Load8 необходимо, чтобы старшие 7 байт (56 бит) в блоке памяти были равны нулю. К сожалению, в коде этого нет.

Как вы можете видеть, только старшие биты от 9 до 16 ограничены нулем. Остальные старшие 48 бит могут быть любыми значениями и по-прежнему передаваться как «чтение из памяти».

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

Исправить эту уязвимость на самом деле довольно просто.

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

Уязвимость конструкции: атака «Подделка ответа»

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

Пользователи могут вызвать функцию buy_token() для покупки токенов (возможно, путем оплаты или передачи других ценных предметов). Одним из его основных шагов является увеличение баланса счета токена на 1 путем вызова функции add_token(). Поскольку ZK prover сам по себе не поддерживает структуру данных кадра вызова, для записи и отслеживания полной истории этих кадров вызова необходимы таблица выполнения (E-Table) и таблица переходов (J-Table).

На приведенном выше рисунке показан процесс вызова add_token() buy_token() и возврата из add_token() в buy_token(). Видно, что баланс счета токена увеличивается на 1. В таблице выполнения каждый шаг выполнения занимает одну строку, включая номер текущего выполняемого кадра вызова, имя текущей контекстной функции (только для иллюстрации), номер текущей выполняемой инструкции в функции и текущую инструкцию, хранящуюся в таблице (только для иллюстрации). В таблице переходов каждый кадр вызова занимает одну строку, в которой хранится номер кадра вызывающего объекта, имя контекста вызывающей функции (только в целях иллюстрации) и позиция следующей инструкции кадра вызывающего объекта (чтобы кадр мог вернуться). В обеих таблицах есть столбец "jops", который отслеживает, является ли текущая инструкция вызовом/возвратом (в таблице выполнения) и общее количество инструкций вызова/возврата для этого кадра (в таблице переходов).

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

Однако здесь есть проблема: в то время как один вызов и один возврат увеличат количество "jops" для кадра до 2, два вызова или два возврата также приведут к счетчику 2. Наличие двух вызовов или двух возвратов на кадр может показаться абсурдным, но важно помнить, что это именно то, что хакер попытается сделать, нарушив ожидания.

Возможно, вы сейчас взволнованы, но действительно ли мы обнаружили проблему?

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

Тем не менее, ситуация не столь удачна для двух возвратов: поскольку при возврате не создается новый фрейм, хакер действительно может получить таблицу выполнения и таблицу переходов легитимной последовательности выполнения и внедрить поддельные возвраты (и соответствующие кадры). Например, предыдущий пример Execution Table и Jump Table, в котором buy_token() вызывает add_token(), может быть изменен хакером в следующем сценарии:

Хакер внедрил два поддельных возврата между исходным вызовом и возвратом в таблицу выполнения и добавил новую строку поддельного кадра в таблицу переходов (исходный возврат и последующие шаги выполнения инструкций в таблице выполнения должны быть увеличены на 4). Так как количество "jops" для каждой строки в таблице переходов равно 2, ограничения выполняются, и средство проверки доказательств zkWasm принимает "доказательство" этой поддельной последовательности выполнения. Как видно из рисунка, баланс токен-счета увеличивается в 3 раза вместо 1. Таким образом, хакер мог получить 3 токена по цене 1.

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

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

Вы можете подумать, что эта уязвимость должна быть очевидной, но на самом деле это не так. Это связано с тем, что существует разрыв между утверждениями «два вызова или два возврата также приведут к тому, что количество «джопов» равно 2» и «два возврата на самом деле возможны». Последнее требует детального и всестороннего анализа различных ограничений в Execution Table и Jump Table, что затрудняет выполнение полных неформальных рассуждений.

Сравнение двух уязвимостей

«Уязвимость внедрения данных Load8» и «Уязвимость возврата подделки» могут позволить хакерам манипулировать доказательствами ZK, создавать фальшивые транзакции, обманывать проверяющих доказательства и участвовать в краже или угоне. Однако их природа и способ обнаружения совершенно различны.

Уязвимость "Load8 Data Injection" была обнаружена во время аудита zkWasm. Это была непростая задача, так как нам пришлось просмотреть сотни ограничений в более чем 6 000 строк кода Rust и десятки инструкций zkWasm. Несмотря на это, уязвимость было относительно легко обнаружить и подтвердить. Поскольку эта уязвимость была устранена до начала формальной верификации, она не была обнаружена в процессе проверки. Если бы эта уязвимость не была обнаружена в ходе аудита, мы могли бы ожидать, что она будет обнаружена при проверке инструкции Load8.

«Уязвимость возврата подделки» была обнаружена во время формальной проверки после аудита. Одна из причин, по которой мы не смогли обнаружить его во время аудита, заключается в том, что zkWasm имеет механизм, похожий на "jops", называемый "mops", который отслеживает инструкции доступа к памяти, соответствующие историческим данным для каждой единицы памяти во время выполнения zkWasm. Ограничения на количество швабр действительно правильные, потому что они отслеживают только один тип инструкций памяти, записи в память, а исторические данные каждого блока памяти являются неизменяемыми и записываются только один раз (количество швабр равно 1). Но даже если бы мы заметили эту потенциальную уязвимость во время аудита, мы все равно не смогли бы легко подтвердить или исключить все возможные сценарии без строгих формальных рассуждений по всем соответствующим ограничениям, поскольку на самом деле нет ни одной строки кода, которая была бы некорректной.

Таким образом, эти две уязвимости относятся к категориям «уязвимости кода» и «уязвимости дизайна» соответственно. Уязвимости в коде относительно просты, их легче обнаружить (ошибочный код), а также легче обосновать и подтвердить. Уязвимости в дизайне могут быть очень тонкими, их сложнее обнаружить (нет «ошибочного» кода) и труднее объяснить и подтвердить.

Рекомендации по обнаружению уязвимостей ZK

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

Проверка кода и дизайна

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

Проведение аудитов и формальных проверок

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

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

Если ваш проект ZK уже прошел аудит (похвала) или несколько аудитов (большая похвала), мы предлагаем провести формальную проверку схемы на основе результатов предыдущего аудита. Наш опыт проведения аудита и формальной верификации в таких проектах, как zkVM и других, как ZK, так и не-ZK, неоднократно показывал, что формальная верификация часто фиксирует уязвимости, пропущенные во время аудита. Учитывая природу ZKP, в то время как ZK-системы должны обеспечивать лучшую безопасность и масштабируемость блокчейна, чем не-ZK-решения, критичность их безопасности и корректности намного выше, чем у традиционных не-ZK-систем. Таким образом, ценность высококачественной формальной верификации для систем ZK намного выше, чем для систем без ZK.

Обеспечьте безопасность схем и смарт-контрактов

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

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

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

Подытожим влияние формальной верификации (ФВ) на системы ZK и их компоненты следующими моментами.

Утверждение:

1. Эта статья воспроизведена с [panewslab], авторские права принадлежат оригинальному автору [CertiK], если у вас есть какие-либо возражения против перепечатки, пожалуйста, свяжитесь с командой Gate Learn, и команда рассмотрит ее как можно скорее в соответствии с соответствующими процедурами.

2. Дисклеймер: Взгляды и мнения, выраженные в этой статье, представляют собой только личные взгляды автора и не являются какими-либо инвестиционными рекомендациями.

3. Версии статьи на других языках переведены командой Gate Learn и не упоминаются в Gate.io, переведенная статья не может быть воспроизведена, распространена или использована в качестве плагиата.