Ця стаття створена спільнотою. Автор Девід Тардіті, віце-президент з інженерних питань в CertiK, фірмі, що займається аудитом смартконтрактів Web3.
Короткий зміст
Формальна верифікація смартконтрактів гарантує відсутність у них помилок, уразливостей й інших непередбачених характеристик. У ньому експерт представляє логіку смартконтракту у вигляді математичних виразів, а потім запускає їх через автоматизований процес, який перевіряє фактичну логіку на відповідність моделям очікуваної поведінки контракту. Поєднання формальної верифікації і ручного аудиту забезпечує всебічну оцінку безпеки смартконтракту.
Вступ
Смартконтракти – це комп'ютерні програми, розгорнуті на блокчейні, які запускаються автоматично під час виконання певних умов. Вони можуть змінюватись від простих до надзвичайно складних, і можуть містити активи на мільйони або навіть мільярди доларів.
Уразливість безпеки в коді смартконтракту може мати руйнівні наслідки, зокрема крадіжку всіх активів, що зберігаються у смартконтракті. У 2021 році в автоматизованого маркет-мейкера (AMM) Uranium Finance було вкрадено 50 мільйонів доларів США через єдину друкарську помилку у смартконтракті.
Також у 2021 році Compound Finance виплатила 80 мільйонів доларів США незароблених винагород через помилку в одному символі. У 2022 році з Wormhole Bridge було вкрадено 320 мільйонів доларів США через помилку в одному із смартконтрактів.
Важливо правильно налаштувати програму смартконтракту із першого разу. Смартконтракти мають відкритий вихідний код, тобто код стає публічним після розгортання контракту. Якщо хакер знаходить помилку, він може негайно нею скористатися. Крім того, виправлення вразливостей безпеки з плином часу не є рішенням, оскільки код смартконтракту зазвичай не може бути змінений після розгортання.
Як працює верифікація смартконтракту?
Формальна верифікація смартконтрактів представляє логіку і бажану поведінку смартконтрактів у вигляді математичних тверджень. Потім аудитори використовують автоматизовані інструменти перевірки правильності цих тверджень.
Процес містить:
Визначення специфікацій і бажаних властивостей контракту формальною мовою.
Переведення коду контракту у формальне представлення, таке як математичні моделі чи логіка.
Запуск автоматизованих засобів доказу тверджень або валідації моделей для перевірки технічних характеристик і властивостей контракту.
Повторення процесу верифікації для виявлення і перевірки будь-яких помилок або відхилень від бажаних властивостей.
Чому важлива верифікація смартконтракту
Використання математичних тверджень допомагає гарантувати, що формально верифіковані смартконтракти не містять помилок, уразливостей й іншої непередбаченої поведінки. Це також допомагає підвищити довіру та впевненість у контракті, оскільки його властивості були строго підтверджені.
Нижче наведено кілька прикладів того, як верифікація смартконтрактів допомогла запобігти значним фінансовим втратам й іншим катастрофічним наслідкам.
Uniswap
Uniswap є відомим AMM. Коли було розроблено смартконтракт Uniswap V1, його було офіційно верифіковано. Перед його випуском ця формальна верифікація виявила і виправила помилки округлення, які могли призвести до виснаження коштів Uniswap V1.
Balancer
Balancer V2 також є офіційно верифікованим AMM. Формальна верифікація виявила і виправила неправильний розрахунок комісії, пов'язаний із функцією миттєвої позики у смартконтракті, що могло зробити біржу вразливою для крадіжки.
SafeMoon
SafeMoon V1 містив непомітну помилку, виявлену формальною верифікацією після його запуску. Власник міг відмовитися від права власності на контракт, а потім знову його придбати, якщо до відмови від права власності було виконано певні операції.
Ця помилка була не помічена у більшості ручних аудитів форків SafeMoon V1, тому що для її виявлення був потрібен аналіз певних комбінацій значень програмних змінних. Така робота складна для людини, але досить проста для машини.
Як формальна верифікація і ручний аудит працюють разом
Формальна верифікація забезпечує систематичний й автоматизований спосіб перевірки логіки та поведінки контракту на відповідність його бажаним властивостям. Це спрощує виявлення і виправлення будь-яких потенційних помилок чи багів. Це особливо корисно для пошуку складних і малопомітних проблем, які може бути важко виявити під час ручної перевірки.
Ручний аудит включає експертну перевірку коду, дизайну і розгортання контракту. Аудитори використовують свій досвід та знання для виявлення ризиків безпеки й оцінки загального стану безпеки контракту. Вони також можуть підтвердити правильність формального процесу верифікації і перевірити наявність проблем, які неможливо виявити за допомогою автоматизованих інструментів.
Поєднання формальної верифікації і ручного аудиту забезпечує всебічну та ретельну оцінку безпеки смартконтракту. Це збільшує шанси знайти та виправити будь-які вразливості. Результатом є багаторівневий підхід до безпеки, в якому використовуються унікальні можливості як людей, так і машин.
Підсумки
Щоб забезпечити безпеку смартконтрактів, важливо використовувати як формальну верифікацію, так і ручний аудит для забезпечення всебічної та ретельної оцінки стану безпеки смартконтракту.
Хоча формальна верифікація може бути ресурсомісткою, вона є виправданим вкладенням коштів для контрактів із високою вартістю чи факторами високого ризику. Зрештою, життєво важливо приділяти пріоритетну увагу безпеці і забезпечувати відсутність помилок, уразливостей та непередбаченої поведінки у смартконтрактах.
Пов'язані статті
Відмова від відповідальності та попередження про ризики: цей контент надається вам на умовах "як є" тільки для загальної інформації та освітніх цілей, без будь-яких заяв чи гарантій. Його не слід розглядати як фінансову пораду, і він не призначений для рекомендації купівлі конкретного продукту чи послуги. Ціни на цифрові активи можуть бути волатильними. Вартість ваших інвестицій може як впасти, так і зрости, і ви можете не повернути інвестовану суму. Ви несете повну відповідальність за свої інвестиційні рішення, і Binance Academy не несе відповідальності за збитки, які ви можете понести. Цей матеріал не слід розглядати як фінансову пораду.