Вступ

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

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

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

Коротка історія смартконтрактів

Джерело: CryptoSlate

Нік Сзабо, американський комп'ютерний вчений і криптограф, про якого часто говорять, що він є Сатоші Накамото, був піонером смартконтрактів, вперше представивши концепцію в 1994 році. Сзабо описав смартконтракти як цифрові протоколи транзакцій, призначені для автоматичного забезпечення виконання умов угоди. Його метою було покращення методів електронних транзакцій, таких як системи продажу, та розширення їх можливостей в цифровому світі.

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

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

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

Джерело: Середній

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

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

Типи формальних специфікацій для смартконтрактів

Джерело: Ever Scale

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

Високорівневі специфікації

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

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

Низькорівневі специфікації

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

Техніки формальної верифікації смартконтрактів

Джерело: Ever Scale

Перевірка моделі

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

Доведення теореми

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

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

Символьне виконання

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

Наприклад, якщо контрактна функція повертається, коли значення знаходиться між 5 і 10, символьне виконання може ефективно ідентифікувати такі значення, що запускають, обчислюючи умову як X > 5 ∧ X < 10. Цей метод часто є більш ефективним, ніж традиційне тестування, виробляючи менше помилкових спрацьовувань і безпосередньо генеруючи конкретні значення, які потім повторюють будь-який SMT-розв'язувач, використовується для визначення знайдених помилок, що робить його цінним інструментом для забезпечення надійності смарт-контрактів.

Що таке смартконтракти?

Джерело: Ніжно

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

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

Вразливості зі смартконтрактами

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

• У 2021 році автоматизований ринковий мейкер Uranium Finance постраждав від крадіжки на $50 мільйонівчерез просту помилку в його смартконтракті.
• Також у 2021 році,Компанія Compound Finance ненавмисно розподілила $80 мільйоніву незаслужених винагородах, знову через помилку в одному символі.
• Більш серйозне порушення сталося у 2022 роціколи з воротами викрадено $320 мільйонів з ворот Wormholeчерез помилку в одному з його смартконтрактів.

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

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

Джерело: Certik

Процес включає в себе:

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

Основні характеристики смартконтрактів

Джерело: Certik

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

Чому важлива формальна верифікація смартконтрактів

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

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

Uniswap

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

Balancer

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

SafeMoon

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

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

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

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

Переваги та недоліки смартконтрактів

Джерело: Blockonomi

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

Плюси смарт-контрактів

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

Недоліки смартконтрактів

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

Засоби формальної верифікації для смартконтрактів Ethereum

Джерело: Calibraint

Мови специфікації для створення формальних специфікацій

• Act: Act дозволяє користувачам визначати оновлення сховища, попередні та післяумови та інваріанти контракту. Його набір інструментів включає засоби підтвердження, які можуть перевіряти різні властивості за допомогою Coq, SMT-рішувачів або hevm.

GitHub

Документація

• Scribble: Scribble перетворює анотації коду, написані мовою своєї специфікації, в конкретні твердження, які перевіряють специфікації.

Документація

• Dafny: Dafny - це мова програмування, призначена для верифікації, використовуючи високорівневі анотації, щоб допомогти обговорити та підтвердити правильність коду.

GitHub

Перевірники програм для перевірки правильності

• Certora Prover: Certora Prover - це автоматизований інструмент формальної верифікації, який перевіряє правильність кодів смартконтрактів. Специфікації створюються за допомогою мови верифікації Certora (CVL), а виявлення порушень властивостей здійснюється за допомогою комбінації статичного аналізу та технік розв'язання обмежень.

Веб-сторінка

Документація

• Solidity SMTChecker: SMTChecker Solidity - це інтегрований перевірник моделей, який використовує Satisfiability Modulo Theories (SMT) та розв'язання Horn. Він перевіряє, чи відповідає вихідний код контракту специфікаціям під час компіляції та перевіряє порушення властивостей безпеки.

GitHub

• Solc-verify: Solc-verify - це розширена версія компілятора Solidity, яка дозволяє автоматизовану формальну верифікацію коду Solidity за допомогою анотацій та модулярної верифікації програм.

GitHub

• KEVM: KEVM формально представляє Віртуальну Машину Ethereum(EVM)створено за допомогою K-платформи. Він є виконавчим і може перевіряти конкретні вимоги, пов'язані з властивостями, за допомогою логіки досяжності.

GitHub

Документації

Логічні рамки для доведення теорем

• Isabelle: Isabelle/HOL — це помічник доказу, який допомагає користувачам висловлювати математичні формули формальною мовою та надає інструменти для їх доведення. Його основне використання - формалізація математичних доведень, особливо для перевірки правильності апаратного і програмного забезпечення комп'ютерів, а також властивостей мов програмування і протоколів.

GitHub

Документація

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

GitHub

Документація

Інструменти на основі символьного виконання для виявлення вразливих шаблонів у смарт-контрактах

• Manticore - Інструмент, який аналізує байт-код EVM за допомогою символьного виконання.

GitHub

Документація

• Hevm - hevm - це двигун символьного виконання, який перевіряє еквівалентність байткоду EVM.

GitHub

• Mythril - Інструмент символічного виконання, який використовується для пошуку вразливостей у смартконтрактах Ethereum.

GitHub

Документація

Висновок

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