Перейти до основного вмісту
Change page

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

Редагувати сторінку (opens in a new tab)

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

Формальна верифікація є одним із рекомендованих методів для підвищення безпеки смарт-контрактів. Формальна верифікація, яка використовує формальні методи (opens in a new tab) для специфікації, проєктування та перевірки програм, роками застосовується для забезпечення правильності критично важливих апаратних і програмних систем.

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

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

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

Очікувана поведінка системи (у цьому випадку смарт-контракту) описується за допомогою формального моделювання, тоді як мови специфікацій дозволяють створювати формальні властивості. Методи формальної верифікації потім можуть перевірити, чи відповідає реалізація контракту його специфікації, і отримати математичний доказ правильності першої. Коли контракт задовольняє свою специфікацію, він описується як «функціонально правильний», «правильний за задумом» або «правильний за побудовою».

Що таке формальна модель?

В інформатиці формальна модель (opens in a new tab) — це математичний опис обчислювального процесу. Програми абстрагуються в математичні функції (рівняння), причому модель описує, як обчислюються результати функцій на основі вхідних даних.

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

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

Високорівневі моделі зосереджуються на взаємозв'язку між смарт-контрактами та зовнішніми агентами, такими як зовнішні акаунти (EOA), акаунти контрактів та середовище блокчейну. Такі моделі корисні для визначення властивостей, які вказують, як контракт повинен поводитися у відповідь на певні взаємодії з користувачем.

Навпаки, інші формальні моделі зосереджуються на низькорівневій поведінці смарт-контракту. Хоча високорівневі моделі можуть допомогти в міркуваннях про функціональність контракту, вони можуть не враховувати деталі внутрішньої роботи реалізації. Низькорівневі моделі застосовують підхід «білої скриньки» до аналізу програм і покладаються на низькорівневі представлення застосунків смарт-контрактів, такі як траси програм і графи потоку керування (opens in a new tab), для міркувань про властивості, що стосуються виконання контракту.

Низькорівневі моделі вважаються ідеальними, оскільки вони представляють фактичне виконання смарт-контракту в середовищі виконання Етеріуму (тобто EVM). Методи низькорівневого моделювання особливо корисні для встановлення критичних властивостей безпеки в смарт-контрактах і виявлення потенційних вразливостей.

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

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

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

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

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

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

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

Формальні специфікації виводяться з використанням елементів логіки програм (opens in a new tab), які дозволяють формально міркувати про властивості програми. Логіка програм має формальні правила, які виражають (математичною мовою) очікувану поведінку програми. Для створення формальних специфікацій використовуються різні логіки програм, зокрема логіка досяжності (opens in a new tab), темпоральна логіка (opens in a new tab) та логіка Гоара (opens in a new tab).

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

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

Як випливає з назви, високорівнева специфікація (також звана «модельно-орієнтованою специфікацією») описує високорівневу поведінку програми. Високорівневі специфікації моделюють смарт-контракт як скінченний автомат (opens in a new tab) (FSM), який може переходити між станами шляхом виконання операцій, при цьому темпоральна логіка використовується для визначення формальних властивостей моделі FSM.

Темпоральні логіки (opens in a new tab) — це «правила для міркувань про судження, кваліфіковані з точки зору часу (наприклад, "я завжди голодний" або "я зрештою зголоднію")». При застосуванні до формальної верифікації темпоральні логіки використовуються для формулювання тверджень про правильну поведінку систем, змодельованих як автомати станів. Зокрема, темпоральна логіка описує майбутні стани, в яких може перебувати смарт-контракт, і те, як він переходить між станами.

Високорівневі специфікації зазвичай фіксують дві критичні темпоральні властивості для смарт-контрактів: безпеку (safety) та живучість (liveness). Властивості безпеки відображають ідею про те, що «нічого поганого ніколи не трапляється», і зазвичай виражають інваріантність. Властивість безпеки може визначати загальні вимоги до програмного забезпечення, такі як відсутність взаємного блокування (opens in a new tab), або виражати специфічні для предметної області властивості контрактів (наприклад, інваріанти контролю доступу до функцій, допустимі значення змінних стану або умови для переказів токенів).

Візьмемо для прикладу цю вимогу безпеки, яка охоплює умови використання transfer() або transferFrom() у контрактах токенів ERC-20: «Баланс відправника ніколи не буває меншим за запитану кількість токенів для відправлення». Цей опис інваріанта контракту природною мовою можна перекласти у формальну (математичну) специфікацію, яку потім можна ретельно перевірити на валідність.

Властивості живучості стверджують, що «зрештою відбувається щось хороше», і стосуються здатності контракту просуватися через різні стани. Прикладом властивості живучості є «ліквідність», яка стосується здатності контракту переказувати свої баланси користувачам за запитом. Якщо ця властивість порушується, користувачі не зможуть вивести активи, що зберігаються в контракті, як це сталося під час інциденту з гаманцем Parity (opens in a new tab).

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

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

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

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

Властивості в стилі Гоара

Логіка Гоара (opens in a new tab) надає набір формальних правил для міркувань про правильність програм, зокрема смарт-контрактів. Властивість у стилі Гоара представлена трійкою Гоара {P}c{Q}, де c — це програма, а P і Q — предикати стану c (тобто програми), формально описані як передумови та післяумови відповідно.

Передумова — це предикат, що описує умови, необхідні для правильного виконання функції; користувачі, які викликають контракт, повинні задовольняти цю вимогу. Післяумова — це предикат, що описує умову, яку функція встановлює у разі правильного виконання; користувачі можуть очікувати, що ця умова буде істинною після виклику функції. Інваріант у логіці Гоара — це предикат, який зберігається під час виконання функції (тобто він не змінюється).

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

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

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

Багато фреймворків формальної верифікації використовують специфікації в стилі Гоара для доведення семантичної правильності функцій. Також можна додавати властивості в стилі Гоара (як твердження) безпосередньо до коду контракту, використовуючи оператори require та assert у Solidity.

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

Властивості на рівні трас

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

Цей підхід покладається на модель смарт-контрактів як систем переходів станів із деякими заздалегідь визначеними станами (описаними змінними стану) разом із набором заздалегідь визначених переходів (описаних функціями контракту). Крім того, граф потоку керування (opens in a new tab) (CFG), який є графічним представленням потоку виконання програми, часто використовується для опису операційної семантики контракту. Тут кожна траса представлена як шлях на графі потоку керування.

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

Використаймо приклад контракту DAO, який має деякі загальнодоступні функції, щоб описати властивості на рівні трас. Тут ми припускаємо, що контракт DAO дозволяє користувачам виконувати такі операції:

  • Вносити кошти

  • Голосувати за пропозицію після внесення коштів

  • Затребувати відшкодування, якщо вони не голосують за пропозицію

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

Методи формальної верифікації смарт-контрактів

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

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

Перевірка моделей вимагає створення абстрактного математичного представлення системи (тобто контракту) та вираження властивостей цієї системи за допомогою формул, що ґрунтуються на логіці висловлювань (opens in a new tab). Це спрощує завдання алгоритму перевірки моделей, а саме доведення того, що математична модель задовольняє задану логічну формулу.

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

Наприклад, властивість безпеки, пов'язана з контролем доступу (наприклад, Тільки власник контракту може викликати selfdestruct), може бути записана у формальній логіці. Після цього алгоритм перевірки моделей може перевірити, чи задовольняє контракт цю формальну специфікацію.

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

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

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

Мета доведення теорем полягає в перевірці логічної еквівалентності між цими твердженнями. «Логічна еквівалентність» (також звана «логічною біімплікацією») — це тип зв'язку між двома твердженнями, за якого перше твердження є істинним тоді і тільки тоді, коли друге твердження є істинним.

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

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

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

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

Символьне виконання — це метод аналізу смарт-контракту шляхом виконання функцій з використанням символьних значень (наприклад, x > 5) замість конкретних значень (наприклад, x == 5). Як метод формальної верифікації, символьне виконання використовується для формальних міркувань про властивості на рівні трас у коді контракту.

Символьне виконання представляє трасу виконання як математичну формулу над символьними вхідними значеннями, інакше звану предикатом шляху. SMT-вирішувач (opens in a new tab) використовується для перевірки того, чи є предикат шляху «здійсненним» (тобто чи існує значення, яке може задовольнити формулу). Якщо вразливий шлях є здійсненним, SMT-вирішувач згенерує конкретне значення, яке спрямує виконання на цей шлях.

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

Навпаки, інструмент символьного виконання виконав би функцію із символьним значенням: X > 5 ∧ X < 10 (тобто x більше за 5 ТА x менше за 10). Пов'язаний предикат шляху x = X > 5 ∧ X < 10 потім був би переданий SMT-вирішувачу для розв'язання. Якщо певне значення задовольняє формулу x = X > 5 ∧ X < 10, SMT-вирішувач обчислить його — наприклад, вирішувач може видати 7 як значення для x.

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

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

Символьне виконання також може надати певний ступінь математичного доказу правильності. Розгляньмо такий приклад функції контракту із захистом від переповнення:

function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}

Траса виконання, яка призводить до цілочисельного переповнення, повинна була б задовольняти формулу: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) Таку формулу навряд чи вдасться розв'язати, тому вона слугує математичним доказом того, що функція safe_add ніколи не зазнає переповнення.

Чому варто використовувати формальну верифікацію для смарт-контрактів?

Потреба в надійності

Формальна верифікація використовується для оцінки правильності критично важливих для безпеки систем, збій яких може мати руйнівні наслідки, такі як смерть, травми або фінансовий крах. Смарт-контракти — це цінні застосунки, що контролюють величезні обсяги цінностей, і прості помилки в проєктуванні можуть призвести до безповоротних втрат для користувачів (opens in a new tab). Однак формальна верифікація контракту перед розгортанням може підвищити гарантії того, що він працюватиме належним чином після запуску в блокчейні.

Надійність є дуже бажаною якістю будь-якого смарт-контракту, особливо тому, що код, розгорнутий у віртуальній машині Етеріуму (EVM), зазвичай є незмінним. Оскільки оновлення після запуску не є легкодоступними, потреба гарантувати надійність контрактів робить формальну верифікацію необхідною. Формальна верифікація здатна виявляти складні проблеми, такі як цілочисельне недоповнення та переповнення, повторний вхід (re-entrancy) і погана оптимізація газу, які можуть залишитися непоміченими аудиторами та тестувальниками.

Доведення функціональної правильності

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

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

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

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

Ідеальні цілі для верифікації

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

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

Швидший цикл розробки

Методи формальної верифікації, такі як перевірка моделей і символьне виконання, зазвичай є ефективнішими за звичайний аналіз коду смарт-контракту (який виконується під час тестування або аудиту). Це пов'язано з тим, що формальна верифікація покладається на символьні значення для перевірки тверджень («що, якщо користувач спробує вивести n етерів?»), на відміну від тестування, яке використовує конкретні значення («що, якщо користувач спробує вивести 5 етерів?»).

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

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

Недоліки формальної верифікації

Вартість ручної праці

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

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

Хибнонегативні результати

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

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

Проблеми з продуктивністю

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

Крім того, верифікатори програм не завжди можуть визначити, чи може бути задоволена властивість (описана як логічна формула) чи ні («проблема розв'язності (opens in a new tab)»), оскільки програма може ніколи не завершитися. Таким чином, може бути неможливо довести деякі властивості для контракту, навіть якщо він добре специфікований.

Інструменти формальної верифікації для смарт-контрактів Етеріуму

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

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

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

Dafny - Dafny — це готова до верифікації мова програмування, яка покладається на високорівневі анотації для міркувань про правильність коду та її доведення.

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

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

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

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

KEVM - KEVM — це формальна семантика віртуальної машини Етеріуму (EVM), написана у фреймворку K. KEVM є виконуваним і може доводити певні твердження, пов'язані з властивостями, використовуючи логіку досяжності.

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

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

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

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

Мантікора - Інструмент для аналізу байт-коду EVM на основі символьного виконання.

hevm - hevm — це рушій символьного виконання та засіб перевірки еквівалентності для байт-коду EVM.

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

Подальше читання

Останнє оновлення сторінки: 28 квітня 2026 р.

shalom-ezekiels (opens in a new tab)
corwintinesc (opens in a new tab)
MOSHKA-GOTM (opens in a new tab)
+12