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

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

(відкривається в новій вкладці)

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

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

ЩО ТАКЕ ФОРМАЛЬНА ПЕРЕВІРКА?

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

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

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

У комп'ютерних науках формальна модель

(відкривається в новій вкладці)

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

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

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

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

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

(відкривається в новій вкладці)

, щоб міркувати про властивості, що є важливими для виконання контракту.

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

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

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

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

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

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

ТИПИ ФОРМАЛЬНИХ СПЕЦИФІКАЦІЙ ДЛЯ СМАРТ-КОНТРАКТІВ

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

Формальні специфікації виводяться за допомогою елементів логіка програми

(відкривається в новій вкладці)

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

(відкривається в новій вкладці)

тимчасова логіка

(відкривається в новій вкладці)

та Логіка Хоара

(відкривається в новій вкладці)

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

Високорівневі технічні характеристики

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

(відкривається в новій вкладці)

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

Часові логіки

(відкривається в новій вкладці)

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

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

(відкривається в новій вкладці)

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

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

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

(відкривається в новій вкладці)

.

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

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

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

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

властивості у стилі Хоара

Логіка Хоара

(відкривається в новій вкладці)

надає набір формальних правил для мислення про правильність програм, включаючи смарт-контракти. Властивість у стилі Хоара представлена Хоаровським потрійним {P}c{Q}, де c - це програма, а P та Q - предикати стану c (тобто програми), формально описані як передумови та наслідки, відповідно.

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

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

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

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

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

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

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

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

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

(відкривається в новій вкладці)

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

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

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

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

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

ТЕХНІКИ ФОРМАЛЬНОЇ ПЕРЕВІРКИ СМАРТ-КОНТРАКТІВ

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

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

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

(відкривається в новій вкладці)

. Це спрощує завдання алгоритму перевірки моделі, а саме довести, що математична модель задовольняє задану логічну формулу.

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

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

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

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

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

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

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

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

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

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

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

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

(відкривається в новій вкладці)

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

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

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

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

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

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

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

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

(відкривається в новій вкладці)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

НЕДОЛІКИ ФОРМАЛЬНОЇ ПЕРЕВІРКИ

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

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

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

Хибні негативи

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

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

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

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

Крім того, програмні верифікатори не завжди можуть визначити, чи може властивість (описана як логічна формула) бути задоволена чи ні ("проблема вирішуваності

(відкривається в новій вкладці)

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

ФОРМАЛЬНІ ЗАСОБИ ВЕРИФІКАЦІЇ ДЛЯ СМАРТ-КОНТРАКТІВ ETHEREUM

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

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

• GitHub
• (відкривається в новій вкладці)
• Документація
• (відкривається в новій вкладці)

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

• Документація
• (відкривається в новій вкладці)

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

• GitHub
• (відкривається в новій вкладці)

Program verifiers for checking correctness

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

• Веб-сайт
• (відкривається в новій вкладці)
• Документація
• (відкривається в новій вкладці)

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

• GitHub
• (відкривається в новій вкладці)

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

• GitHub
• (відкривається в новій вкладці)

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

• GitHub
• (відкривається в новій вкладці)
• Документація
• (відкривається в новій вкладці)

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

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

• GitHub
• (відкривається в новій вкладці)
• Документація
• (відкриється в новій вкладці)

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

• GitHub
• (відкривається в новій вкладці)
• Документація
• (відкривається в новій вкладці)

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

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

• GitHub
• (відкривається в новій вкладці)
• Документація
• (відкривається в новій вкладці)

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

• GitHub
• (відкривається в новій вкладці)

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

• GitHub
• (відкривається в новій вкладці)
• Документація
• (відкривається в новій вкладці)

Disclaimer：

1. Ця стаття була перевидана з [ ]. Усі авторські права належать оригінальному авторові [**]. Якщо є заперечення щодо цього перевидання, будь ласка, зв'яжіться з Ворота Вчитькоманда, і вони оперативно вирішать це.
2. Відповідальність за відмову: Погляди та думки, висловлені в цій статті, є виключно тими автора і не становлять жодної інвестиційної поради.
3. Переклади статей на інші мови виконуються командою Gate Learn. Якщо не зазначено, копіювання, поширення або плагіатування перекладених статей заборонено.