Безпека, тестування та формальна верифікація

Ми — Runtime Verification, компанія з досліджень та розробок, що створює суворі інструменти для забезпечення безпеки та правильності критичних систем. Наша команда розробила KEVM, найповнішу та перевірену в бойових умовах формальну семантику віртуальної машини Ethereum (EVM), написану у фреймворку K. KEVM — це не просто специфікація, це виконувана специфікація, яку можна використовувати для символьного міркування про смартконтракти, запуску тестів на відповідність, аналізу використання газу, налагодження програм та формальної перевірки властивостей правильності. Вона проходить повний набір тестів Ethereum і використовується для перевірки високоцінних контрактів, включаючи токени ERC-20 як на Solidity, так і на Vyper. Нещодавно ми оновили семантику для підтримки оновлення Pectra. KEVM активно використовується Kontrol — нашим інструментом формальної верифікації для Solidity, який активно застосовується провідними командами в екосистемі EVM, включаючи Optimism, Ethereum Foundation, Lido, Uniswap, а також дослідниками безпеки та аудиторами в ширшій спільноті Ethereum. Ми активно підтримуємо цей репозиторій, робимо внесок в еволюцію протоколу Ethereum та інтегруємося з інструментами для розробників, такими як Foundry. За допомогою KEVM ми розширюємо межі можливого в доказово правильній та безпечній інфраструктурі смартконтрактів.

Act — це мова специфікації смарт-контрактів та набір інструментів для формальної верифікації. Специфікації Act — це формальний, високорівневий опис усіх можливих варіантів поведінки програми EVM. Act дозволяє використовувати багато існуючих інструментів верифікації загального призначення для доведення властивостей специфікації. До таких інструментів належать SMT-солвери (cvc5, z3, bitwuzla), системи автоматичного доведення теорем (Coq) та інструменти економічного аналізу (CheckMate, Open Games). Специфікації Act можуть бути автоматично доведені як еквівалентні конкретним реалізаціям в EVM. Для дуже простих контрактів специфікації Act можуть бути автоматично згенеровані з байт-коду EVM. Це наскрізний конвеєр, який підтримує принципове міркування про високорівневі властивості байт-коду EVM. Він підтримує міркування як про коректність (наприклад, облікові інваріанти), так і про економічні властивості (наприклад, сумісність стимулів). Специфікації Act слугують високорівневим представленням смарт-контракту, що дозволяє легко інтегрувати існуючі інструменти аналізу та верифікації загального призначення в контекст EVM.

Titanoboa — це інтерпретатор і фреймворк для тестування Vyper, який забезпечує сучасний інтегрований досвід розробки смартконтрактів на Vyper. Він дозволяє розробникам тестувати та налагоджувати контракти Vyper безпосередньо в Python, пропонуючи такі функції, як зручне трасування (tracebacks), створення форків, можливості налагодження, інтеграцію з pytest та готовий до використання фазинг. Окрім своїх автономних можливостей, Titanoboa слугує основою для інших популярних фреймворків тестування, таких як Ape та Moccasin, і є ключовою частиною інфраструктури для екосистеми Vyper.