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

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

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

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

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

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

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

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

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

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

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

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

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

Низькорівневі моделі вважаються ідеальними, оскільки вони представляють фактичне виконання смарт-контракту в середовищі виконання Ethereum (тобто 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 — це «правила для міркувань про пропозиції, кваліфіковані з погляду часу (наприклад, «Я завжди голодний» або «Я колись зголоднію»).” При застосуванні до формальної верифікації темпоральні логіки використовуються для формулювання тверджень про коректну поведінку систем, змодельованих як скінченні автомати. Зокрема, темпоральна логіка описує майбутні стани, у яких може перебувати смарт-контракт, і як він переходить між станами.

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

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

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

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

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

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

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

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

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

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

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

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

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

Багато фреймворків формальної верифікації використовують специфікації в стилі Гоара для доведення семантичної коректності функцій. Також можна додавати властивості в стилі Гоара (як твердження) безпосередньо в код контракту за допомогою операторів 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.

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

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

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

1function safe_add(uint x, uint y) returns(uint z){
2
3  z = x + y;
4  require(z>=x);
5  require(z>=y);
6
7  return z;
8}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Документаціяopens in a new tab

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

GitHubopens in a new tab

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

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

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

GitHubopens in a new tab

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

GitHubopens in a new tab

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

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

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

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

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

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

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

GitHubopens in a new tab

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