У попередній статті ми обговорювали розширену формальну верифікацію систем Zero-Knowledge Proof (ZKP): як перевірити інструкцію ZK. Формально перевіряючи кожну інструкцію zkWasm, ми можемо повністю забезпечити технічну безпеку та коректність усієї схеми zkWasm. У цій статті ми зосередимося на перспективі виявлення вразливостей, аналізі конкретних вразливостей, виявлених у процесах аудиту та верифікації, та уроках, отриманих з них. Для загального обговорення розширеної формальної верифікації блокчейнів ZKP, будь ласка, зверніться до статті про розширену формальну перевірку блокчейнів ZKP.

Перш ніж обговорювати вразливості ZK, давайте спочатку розберемося, як CertiK виконує формальну перевірку ZK. Для складних систем, таких як віртуальна машина ZK (zkVM), першим кроком у формальній верифікації (FV) є чітке визначення того, що потрібно перевірити, та його властивостей. Це вимагає всебічного перегляду дизайну системи ZK, реалізації коду та налаштування тестування. Цей процес перетинається зі звичайними аудитами, але відрізняється тим, що після перевірки повинні бути встановлені цілі та властивості перевірки. У CertiK ми називаємо це перевіркою, орієнтованою на аудит. Аудиторська та перевірочна робота, як правило, інтегровані. Для zkWasm ми проводили і аудит, і формальну верифікацію одночасно.

Що таке вразливість ZK?

Основна особливість систем Zero-Knowledge Proof (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, які називаються «вразливостями коду», оскільки вони походять від реалізації коду і можуть бути легко виправлені за допомогою незначних локальних модифікацій коду. Погодьтеся, людям також відносно легше ідентифікувати ці вразливості.

Уразливість дизайну: Forged Return Attack

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

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

Наведений вище малюнок ілюструє процес виклику buy_token() add_token() і повернення з add_token() до buy_token(). Видно, що баланс токен-рахунку збільшується на 1. У таблиці виконання кожен крок виконання займає один рядок, включаючи номер поточного кадру виклику, що виконується, поточне ім'я контекстної функції (лише для ілюстрації), номер поточної запущеної інструкції у функції та поточну інструкцію, що зберігається в таблиці (лише для ілюстрації). У таблиці переходів кожен кадр виклику займає один рядок, зберігаючи номер кадру виклику, ім'я контексту функції виклику (лише для ілюстрації) та наступну позицію інструкції кадру виклику (щоб кадр міг повернутися). В обох таблицях є стовпець "jops", який відстежує, чи є поточна інструкція викликом/поверненням (у Execution Table) та загальну кількість інструкцій виклику/повернення для цього кадру (у Jump Table).

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

Однак тут є проблема: в той час як один виклик і одне повернення збільшать кількість «поштовхів» для кадру до 2, два виклики або два повернення також призведуть до рахунку 2. Наявність двох або двох повернень на кадр може здатися абсурдним, але важливо пам'ятати, що це саме те, що хакер спробує зробити, зламавши очікування.

Можливо, зараз ви відчуваєте хвилювання, але чи справді ми знайшли проблему?

Виходить, що два виклики не є проблемою, оскільки обмеження Execution Table та Jump Table не дозволяють закодувати два виклики в один рядок кадру, оскільки кожен виклик генерує новий номер кадру, тобто номер поточного кадру виклику плюс 1.

Однак ситуація не така вдала для двох повернень: оскільки після повернення не створюється новий кадр, хакер дійсно може отримати таблицю виконання та таблицю переходів із законною послідовністю виконання та впровадити підроблені повернення (і відповідні кадри). Наприклад, попередній приклад таблиці виконання та таблиці переходів, коли buy_token() викликав add_token(), міг бути підроблений хакером для наступного сценарію:

Хакер вставив два підроблених повернення між початковим викликом і поверненням у Execution Table і додав новий підроблений рядок фрейму в Jump Table (початковий крок повернення і наступні кроки виконання інструкцій в Таблиці виконання повинні бути збільшені на 4). Оскільки кількість "jops" для кожного рядка в таблиці переходів дорівнює 2, обмеження виконуються, і перевірка доказу zkWasm прийме "доказ" цієї підробленої послідовності виконання. Як видно з малюнка, баланс токен-рахунку збільшується в 3 рази замість 1. Таким чином, хакер міг отримати 3 токени за ціною 1.

Існують різні способи вирішення цієї проблеми. Одним з очевидних підходів є окреме відстеження викликів і повернень і забезпечення того, щоб кожен кадр мав рівно один виклик і одне повернення.

Можливо, ви помітили, що поки що ми не показали жодного рядка коду для цієї вразливості. Основна причина полягає в тому, що немає проблемного рядка коду; Реалізація коду ідеально узгоджується з дизайном таблиць та обмежень. Проблема криється в самому дизайні, як і в виправленні.

Ви можете подумати, що ця вразливість має бути очевидною, але насправді це не так. Це пов'язано з тим, що існує розрив між «два виклики або два повернення також призведуть до того, що кількість «джопів» дорівнює 2» і «два повернення насправді можливі». Останнє вимагає детального та всебічного аналізу різних обмежень у Таблиці виконання та Таблиці стрибків, що ускладнює виконання повних неформальних міркувань.

Порівняння двох вразливостей

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

«Уразливість впровадження даних Load8» була виявлена під час аудиту zkWasm. Це було непросте завдання, оскільки нам довелося переглянути сотні обмежень у понад 6 000 рядках коду Rust та десятках інструкцій zkWasm. Незважаючи на це, вразливість було відносно легко виявити та підтвердити. Оскільки ця вразливість була усунена до початку формальної перевірки, вона не зустрічалася в процесі перевірки. Якби ця уразливість не була виявлена під час аудиту, можна було б очікувати, що вона буде знайдена під час перевірки інструкції Load8.

«Вразливість повернення підробки» була виявлена під час формальної перевірки після аудиту. Одна з причин, чому ми не змогли виявити його під час аудиту, полягає в тому, що zkWasm має механізм, подібний до «jops» під назвою «mops», який відстежує інструкції доступу до пам'яті, що відповідають історичним даним для кожного блоку пам'яті під час виконання zkWasm. Обмеження на кількість швабр дійсно правильні, оскільки він відстежує лише один тип інструкцій пам'яті, запис пам'яті, а історичні дані кожного блоку пам'яті є незмінними та записуються лише один раз (кількість швабр дорівнює 1). Але навіть якби ми помітили цю потенційну вразливість під час аудиту, ми все одно не змогли б легко підтвердити або виключити всі можливі сценарії без суворого формального обґрунтування всіх відповідних обмежень, оскільки насправді не існує рядка коду, який був би неправильним.

Таким чином, ці дві вразливості належать до категорій «вразливостей коду» та «вразливостей дизайну» відповідно. Уразливості коду відносно прості, їх легше виявити (помилковий код), легше обґрунтувати та підтвердити. Вразливості дизайну можуть бути дуже непомітними, їх важче виявити (немає «помилкового» коду), і важче обґрунтувати та підтвердити.

Найкращі практики виявлення вразливостей ZK

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

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

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

Проведення аудитів та формальної верифікації

Дві вразливості, про які ми тут говорили, були виявлені за допомогою аудиту та формальної перевірки. Дехто може припустити, що сама по собі формальна верифікація усуває потребу в аудиті, оскільки всі вразливості будуть виявлені за допомогою формальної перевірки. Однак наша рекомендація полягає в тому, щоб виконувати і те, і інше. Як пояснювалося на початку цієї статті, якісна офіційна робота з перевірки починається з ретельного огляду, перевірки та неформального обґрунтування коду та дизайну, що збігається з аудитом. Крім того, пошук та усунення простіших вразливостей під час аудиту може спростити та спростити формальний процес перевірки.

Якщо ви проводите як аудит, так і формальну перевірку для системи ZK, оптимальним підходом є виконання обох одночасно. Це дозволяє аудиторам та інженерам з формальної верифікації ефективно співпрацювати, потенційно виявляючи більше вразливостей, оскільки для формальної перевірки потрібні високоякісні аудиторські дані.

Якщо ваш проект ZK вже пройшов аудит (kudos) або множинні аудити (big kudos), наша пропозиція полягає в тому, щоб провести офіційну перевірку схеми на основі результатів попереднього аудиту. Наш досвід аудиту та формальної верифікації в таких проектах, як zkVM та інших, як ZK, так і non-ZK, неодноразово показував, що формальна верифікація часто фіксує вразливості, пропущені під час аудиту. З огляду на природу ZKP, хоча системи ZK повинні пропонувати кращу безпеку та масштабованість блокчейну, ніж рішення без ZK, критичність їх безпеки та коректності набагато вища, ніж у традиційних систем, відмінних від ZK. Таким чином, цінність якісної формальної верифікації для систем ZK значно перевищує цінність систем, відмінних від ZK.

Забезпечте безпеку схем і смарт-контрактів

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

Наші зусилля з аудиту та офіційної перевірки zkWasm стосуються лише схеми zkWasm. Однак, з точки зору загальної безпеки додатків ZK, дуже важливо також провести аудит і офіційну перевірку їх смарт-контрактів. Зрештою, було б прикро, якби після вкладення значних зусиль у забезпечення безпеки схеми слабкість у перевірці смарт-контрактів призвела до компрометації додатків.

На особливу увагу заслуговують два типи смарт-контрактів. Перший тип безпосередньо працює з доказами ZK. Хоча вони можуть бути невеликими за масштабом, їх ризик надзвичайно високий. Другий тип включає середні та великі смарт-контракти, що працюють поверх zkVM. Ми знаємо, що ці контракти іноді можуть бути дуже складними, і найцінніші з них повинні пройти аудит і перевірку, тим більше, що деталі їх виконання не видно в мережі. На щастя, після багатьох років розвитку формальна верифікація смарт-контрактів тепер практична та підготовлена для відповідних високовартісних цілей.

Узагальнимо вплив формальної верифікації (ФВ) на системи ЗК та їх компоненти з наступними моментами.

Заява:

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

2. Відмова від відповідальності: Погляди та думки, висловлені в цій статті, відображають лише особисті погляди автора та не є будь-якою інвестиційною порадою.

3. Інші мовні версії статті перекладені командою Gate Learn і не згадуються в Gate.io, перекладена стаття не може бути відтворена, поширена або плагіатина.