Формальная верификация zk-SNARKs: методы доказательства памяти

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

Система памяти zkWasm состоит из таблицы выполнения и таблицы памяти. Таблица выполнения фиксирует процесс выполнения инструкций, а таблица памяти сохраняет всю историю доступа к памяти. Для упрощения разработки zkWasm предоставляет абстрактный уровень, позволяя управлять памятью с помощью двух функций: alloc_memory_table_lookup_write_cell и alloc_memory_table_lookup_read_cell.

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

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

Процесс верификации осуществляется сверху вниз и включает три шага:

1. Ожидаемое количество создаваемых записей для команды
2. Количество записей в таблице доказательств не должно превышать ожидаемое
3. Докажите с помощью индукции, что cum_mops и instructions_mops всегда一致 в таблице

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

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

В целом, хотя zkVM-верификация имеет различия при обработке динамических состояний, благодаря соответствию абстрактным уровням реализации все же можно применять модульный подход, аналогичный верификации традиционных интерпретаторов. Такой подход минимизирует влияние различий, позволяя каждой инструкции независимо проверяться на основе интерфейса get-set.