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