У цій серії блогів про розширену формальну перевірку доказів із нульовим знанням ми обговорили, як перевірити інструкції ZK, і детально проаналізували дві вразливості ZK. Як показано в публічних звітах і базах коду, офіційно перевіривши кожну інструкцію zkWasm, ми знайшли та виправили кожну вразливість, що дозволило нам повністю перевірити технічну безпеку та правильність усієї схеми zkWasm.
Хоча ми показали процес перевірки інструкції zkWasm і представили попередні концепції відповідного проекту, читачі, знайомі з формальною перевіркою, можуть бути більш зацікавлені в розумінні перевірки zkVM з іншими меншими системами ZK або іншими типами унікальності байт-коду на. У цій статті ми детально обговоримо деякі технічні моменти, які виникають під час перевірки підсистеми пам’яті zkWasm. Пам'ять є найбільш унікальною частиною zkVM, і поводження з нею є критичним для всіх інших перевірок zkVM.
Формальна перевірка: віртуальна машина (VM) проти віртуальної машини ZK (zkVM)
Наша кінцева мета — перевірити коректність zkWasm, яка подібна до теореми про коректність звичайних інтерпретаторів байт-коду (ВМ, таких як інтерпретатор 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 prover по суті є цілочисельною операцією за модулем великих простих чисел, тоді як специфікація Wasm і звичайний інтерпретатор обробляють 32-бітні або 64-бітні цілі числа. Більшість реалізації zkVM включає це, тому відповідну обробку також потрібно виконати під час перевірки. Однак це «локальна» проблема: кожен рядок коду стає складнішим через арифметичні операції, які він повинен виконувати, але загальна структура коду та докази не змінюються.
Ще одна основна відмінність полягає в тому, як обробляються структури даних із динамічним розміром. У звичайному інтерпретаторі байт-коду пам’ять, стек даних і стек викликів реалізовано як змінні структури даних. Подібним чином специфікація Wasm представляє пам’ять як тип даних за допомогою методів get/set. Наприклад, інтерпретатор EVM Geth має тип даних `Memory`, який реалізовано як масив байтів, що представляє фізичну пам’ять, записується та зчитується за допомогою методів `Set 32` і `GetPtr`. Щоб реалізувати інструкцію зберігання пам’яті, Geth викликає `Set 32`, щоб змінити фізичну пам'ять.
func opMstore(pc *uint 64, інтерпретатор *EVMInterpreter, область *ScopeContext) ([]байт, помилка) {
// вискочити значення стека
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 залишок, сума;
void main () {
баланс = 100;
сума = 10;
баланс -= сума; // зняти
}
Зміст і структура таблиці виконання досить прості. Він має 6 кроків виконання (EID від 1 до 6), кожен крок має рядок із переліком свого коду операції, а якщо інструкція є читанням або записом у пам’ять, його адресу та дані:
Кожен рядок у таблиці пам’яті містить адресу, дані, початковий і кінцевий 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(
"зберігати запис 1",
constraint_builder,
Ід,
рухатися |____| constant_from!(LocationType::Heap як u 64),
перемістити |мета| load_block_index.expr(meta), // адреса
рухатися |____| constant_from!( 0), // є 32-розрядним
рухатися |____| constant_from!( 1), // (завжди) увімкнено
);
let 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)
⇐ (ряд 1.eid= 1 ∧ ряд 1.store_addr=balance ∧ ряд 1.store_value= 100 ∧ ...)
mtable_lookup_write(рядок 2.eid, рядок 2.store_addr, рядок 2.store_value)
⇐ (ряд 2.eid= 2 ∧ ряд 2.store_addr=сума ∧ ряд 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)
⇐ (ряд 6.eid= 6 ∧ ряд 6.store_addr=balance ∧ ряд 6.store_value= 90 ∧ ...)
Структура формальної перевірки повинна відповідати абстракціям, які використовуються в програмному забезпеченні, яке перевіряється, щоб доказ міг слідувати тій же логіці, що й код. Для zkWasm це означає, що нам потрібно перевірити схему таблиці пам’яті та функції «alloc read/write cell» як модуль, який працює як змінна пам’ять. Враховуючи такий інтерфейс, перевірку кожної схеми інструкцій можна виконати подібно до звичайного інтерпретатора, тоді як додаткова складність ZK інкапсулюється в модулі підсистеми пам’яті.
Під час перевірки ми реалізували ідею, що "таблицю пам'яті можна фактично розглядати як змінну структуру даних". Тобто напишіть функцію `memory_at type`, яка повністю сканує таблицю пам’яті та будує відповідне відображення адресних даних. (Діапазон значень змінної `type` тут — це три різні типи даних пам’яті Wasm: купа, стек даних і глобальні змінні.) Потім ми доводимо, що обмеження пам’яті, створені функцією alloc, еквівалентні використанню набору та отримуємо Зміни даних, внесені відповідним відображенням адресних даних. Ми можемо довести:
Для кожного eid, якщо виконуються наступні обмеження
memory_table_lookup_read_cell значення зміщення типу eid
але
get (memory_at eid type) offset = Деяке значення
І якщо виконуються наступні обмеження
memory_table_lookup_write_cell значення зміщення типу eid
але
memory_at (eid+ 1) type = встановити (memory_at eid type) значення зсуву
Після цього перевірка кожної інструкції може базуватися на операціях отримання та встановлення на карті адресних даних, подібно до інтерпретаторів байт-коду, не пов’язаного з ZK.
Механізм підрахунку записів у пам’ять zkWasm
Однак наведений вище спрощений опис не розкриває весь вміст таблиці пам'яті та таблиці переходів. У рамках zkVM цими таблицями можуть маніпулювати зловмисники, які можуть легко маніпулювати інструкціями завантаження пам’яті та повертати довільні значення, вставляючи рядок даних.
Взявши як приклад програму зняття коштів, зловмисник має можливість ввести неправдиві дані в баланс рахунку, підробивши операцію запису в пам’ять на суму 110 доларів США перед операцією зняття коштів. Цей процес може бути досягнутий шляхом додавання рядка даних до таблиці пам’яті та зміни значень існуючих клітинок у таблиці пам’яті та таблиці виконання. Це призведе до «безкоштовного» зняття коштів, оскільки баланс рахунку залишатиметься на рівні 100 доларів США після операції.
Щоб переконатися, що таблиця пам’яті (та таблиця переходів) містить лише дійсні записи, згенеровані фактично виконаними інструкціями запису в пам’ять (і виклику та повернення), zkWasm використовує спеціальний механізм підрахунку для моніторингу кількості записів. Зокрема, таблиця пам’яті має окремий стовпець, у якому відстежується загальна кількість записів, записаних у пам’ять. У той же час таблиця виконання також містить лічильник для підрахунку кількості операцій запису в пам'ять, очікуваних для кожної інструкції. Переконайтеся, що два підрахунки узгоджені, встановивши обмеження рівності. Логіка цього методу дуже інтуїтивно зрозуміла: кожен раз, коли операція запису виконується в пам'ять, вона буде зарахована один раз, і в таблиці пам'яті повинен бути відповідний запис. Тому зловмисник не може вставити додаткові записи в таблицю пам’яті.
Наведене вище логічне твердження є дещо нечітким, і в процесі механізованого доказу його потрібно уточнити. По-перше, нам потрібно переглянути формулювання леми про запис пам’яті, згаданої вище. Ми визначаємо функцію `mops_at eid type` для підрахунку записів таблиці пам’яті з заданими `eid` і `type` (більшість інструкцій створюватиме 0 або 1 запис у eid). У повному формулюванні теореми є додаткова передумова про відсутність фальшивих записів таблиці пам’яті:
Якщо виконуються наступні обмеження
(значення зміщення типу eid memory_table_lookup_write_cell)
І встановлюються наступні нові обмеження
(тип 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 ≤ i ->
i + 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 ≤ 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_values eid_cell i) (max_eid+ 1) = інструкції_mops' i n.
Тепер перейдіть до третього кроку. Наша теорема про коректність стверджує, що для будь-якого n cum_mops та інструкції_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) = інструкції_mops (n+ 1)
Зверніть увагу тут
cum_mops n = mop_at n + cum_mops (n+ 1)
і
інструкції_швабри n = інструкції_швабри n + інструкції_швабри (n+ 1)
Тому ми можемо отримати
mops_at n + cum_mops (n+ 1) = instruction_mops n + інструкції_mops (n+ 1)
Раніше ми показали, що кожна інструкція створюватиме не менше очікуваної кількості записів, напр.
mops_at n ≥ instruction_mops n.
Тож можна зробити висновок
cum_mops (n+ 1) ≤ instructions_mops (n+ 1)
Тут нам потрібно застосувати другу лему вище.
(Використовуючи подібну лему для перевірки таблиці переходів, можна довести, що кожна інструкція виклику може точно створювати запис таблиці переходів, тому ця техніка доказу є загальнозастосовною. Однак нам все ще потрібна додаткова перевірка, щоб довести, що повернення Коректність інструкція, що повертається, відрізняється від eid інструкції виклику, яка створила кадр виклику, тому нам також потрібна додаткова інваріантна властивість, щоб оголосити, що значення eid збільшується в одному напрямку під час послідовності виконання.)
Опис процесу перевірки в таких деталях є типовим для формальної верифікації і є причиною того, чому перевірка конкретного фрагмента коду часто займає більше часу, ніж його написання. Але чи варто воно того? У цьому випадку це було варте уваги, тому що ми знайшли критичну помилку в механізмі підрахунку таблиці переходів під час перевірки. Цю помилку було детально описано в попередній статті. Підсумовуючи, старіші версії коду враховували інструкції виклику, і інструкції повернення, і зловмисник міг створити фальшивий стрибок, додавши додаткові інструкції повернення до записів таблиці виконання . Незважаючи на те, що неправильний механізм підрахунку може задовольнити інтуїцію, що кожен виклик і інструкція повернення зараховуються, проблеми виникають, коли ми намагаємося уточнити цю інтуїцію в більш точне твердження теореми.
Зробіть процес перевірки модульним
З наведеного вище обговорення ми можемо побачити, що існує циклічна залежність між доказом схеми кожної інструкції та доказом стовпця підрахунку таблиці виконання. Щоб довести правильність схеми інструкцій, нам потрібно поміркувати про записи в пам’ять, тобто нам потрібно знати кількість записів таблиці пам’яті в конкретному EID, і нам потрібно довести, що кількість операцій запису в пам’ять; таблиця виконання є правильною. Також необхідно довести, що кожна інструкція виконує принаймні мінімальну кількість записів у пам'ять.
Крім того, є ще один фактор, який слід враховувати, тому робота з верифікації повинна бути модульною, щоб кілька інженерів з верифікації могли розділити роботу. Тому при деконструкції доказу механізму підрахунку необхідно звернути особливу увагу на його складність. Наприклад, для інструкції 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)) = Деякі y ->
state_rel (i+ 1) (update_stack (incr_iid st) (y :: xs)).
Перше твердження теореми
opcode_mops_correct LocalGet i
У розгорнутому вигляді це означає, що інструкція створює принаймні один запис таблиці пам’яті в рядку i (номер 1 указано в специфікації коду операції LocalGet zkWasm).
Друга теорема є повною теоремою правильності інструкції, яка цитується
mops_at_correct i
Як гіпотезу, це означає, що інструкція створює рівно один запис таблиці пам’яті.
Інженер з верифікації може довести ці дві теореми незалежно, а потім поєднати їх із доказом щодо таблиці виконання, щоб довести правильність усієї системи. Варто зазначити, що всі перевірки для окремих інструкцій можна виконувати на рівні обмежень читання/запису без знання конкретної реалізації таблиці пам’яті. Тому проект розділений на три частини, які можна виконувати незалежно.
Підведіть підсумки
Перевірка схем zkVM рядок за рядком принципово не відрізняється від перевірки додатків ZK в інших областях, оскільки вони обидва вимагають подібних міркувань щодо арифметичних обмежень. З точки зору високого рівня, перевірка zkVM вимагає багатьох тих самих формальних методів перевірки, які використовуються для інтерпретаторів і компіляторів мови програмування. Основною відмінністю тут є стан віртуальної машини з динамічним розміром. Однак вплив цих відмінностей можна звести до мінімуму шляхом ретельного структурування верифікаційної структури відповідно до рівня абстракції, який використовується в реалізації, що дозволяє реалізовувати кожну інструкцію як незалежний модуль на основі інтерфейсу get-set, як для звичайного інтерпретатора перевірка.