Що таке формальна верифікація смарт-контрактів?

Формалізована перевірка смарт-контрактів допомагає уникнути помилок, вразливостей та інших негативних ситуацій. У цьому процесі людські експерти перетворюють логіку смарт-контракту у математичні твердження, а потім за допомогою автоматизованих інструментів порівнюють їх із моделлю очікуваної поведінки контракту для перевірки відповідності. Поєднання формалізованої перевірки та ручного аудиту дозволяє всебічно оцінити безпеку смарт-контрактів.

Вступ

Смарт-контракти — це програми, розгорнуті у блокчейні, які автоматично виконуються при виконанні певних умов. Вони можуть бути дуже простими або надзвичайно складними, і можуть містити активи на мільйони або навіть мільярди доларів.

Якщо у коді смарт-контракту є вразливості, це може призвести до руйнівних наслідків, наприклад, до крадіжки всіх активів. У 2021 році через орфографічну помилку у смарт-контракті автоматичного маркет-мейкера (AMM) Uranium Finance було викрадено 50 мільйонів доларів.

Так само у 2021 році через одну помилку у коді компанія Compound Finance неправильно виплатила 80 мільйонів доларів у виграші. У 2022 році через помилку у смарт-контракті було викрадено 320 мільйонів доларів з Wormhole Bridge.

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

Як працює перевірка смарт-контрактів?

Формалізована перевірка смарт-контрактів реалізується шляхом перетворення логіки та очікуваної поведінки у математичні твердження. Потім аудитори використовують автоматизовані інструменти для перевірки їх правильності.

Цей процес включає:

• Визначення за допомогою формальної мови специфікацій та очікуваних характеристик контракту.
• Перетворення коду контракту у формалізовані твердження, наприклад, математичні моделі або логіку.
• Використання автоматизованих теоремних доведень або моделювання для перевірки відповідності специфікацій та характеристик.
• Повторна перевірка для виявлення та виправлення будь-яких помилок або відхилень від очікуваної поведінки.

Чому важлива перевірка смарт-контрактів

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

Нижче наведені приклади, які ілюструють, як перевірка смарт-контрактів допомагає запобігти значним фінансовим втратам та іншим катастрофічним наслідкам.

Uniswap

Uniswap — відома платформа автоматичного маркет-мейкера (AMM). Під час розробки смарт-контрактів Uniswap V1 було проведено формалізовану перевірку. Перед запуском ця перевірка виявила та виправила кілька похибок округлення, що запобігло повному висмоктуванню коштів з Uniswap V1.

Balancer

Balancer V2 також є перевіреним AMM. Формалізована перевірка виявила та виправила помилку у розрахунку комісій за функцію миттєвого позики, яка могла легко призвести до крадіжки коштів.

SafeMoon

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

Більшість ручних аудитів SafeMoon V1 пропустили цю помилку, оскільки для її виявлення потрібно було проаналізувати конкретні комбінації значень змінних. Людському оку цю проблему легко пропустити, тоді як машина може вчасно її зафіксувати.

Як формалізована перевірка та ручний аудит працюють разом

Формалізована перевірка пропонує систематичний, автоматизований спосіб перевірки логіки та поведінки контракту відповідно до його очікуваних характеристик. Це полегшує виявлення та виправлення потенційних помилок або вразливостей. Такий підхід особливо корисний для складних і тонких проблем, які важко виявити вручну.

Ручний аудит включає експертний огляд коду, дизайну та розгортання контракту. Аудитори використовують свій досвід і професійні знання для виявлення безпекових ризиків і оцінки загального стану безпеки контракту. Вони також можуть перевірити правильність виконання процесу формалізованої перевірки і виявити будь-які проблеми, які автоматизовані інструменти можуть пропустити.

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

Заключення

Щоб забезпечити безпеку смарт-контрактів, необхідно поєднувати формалізовану перевірку і ручний аудит, щоб отримати всебічну та ґрунтовну оцінку їх безпекового стану.

Хоча формалізована перевірка вимагає значних ресурсів, для контрактів із високою вартістю або високим ризиком це виправдані інвестиції. Адже безпека — понад усе, і потрібно пріоритетно ставитися до її забезпечення, щоб уникнути помилок, вразливостей і несподіваних негативних наслідків. **$BNT **$BROCCOLI