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

Втрата $10M через reentrancy-вразливість в одному з контрактів могла бути запобігнута формальною верифікацією. Ми впроваджуємо математичне доведення коректності для критичних DeFi-протоколів. Різниця критична: тести знаходять наявність помилок, верифікація доводить їх відсутність. MakerDAO, Aave, Compound використовують формальну верифікацію для критичних компонентів. Розглянемо, як це працює на практиці.

Формальна верифікація — це не просто аудит, а математичне доведення. Вона гарантує, що для будь-яких вхідних даних контракт поводиться коректно. За даними дослідження Certora, формальна верифікація покриває 100% можливих шляхів виконання, тоді як fuzz-тестування — лише 60%. Для пошуку reentrancy-вразливостей вона в 5 разів ефективніша за стандартний аудит.

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

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

Certora Prover

Certora Prover — найпоширеніший інструмент для EVM смарт-контрактів. Використовує власну мову специфікацій CVL (Certora Verification Language). Працює як SaaS — завантажуєш контракт і специфікацію, отримуєш результат.

Специфікація пишеться на CVL:

// Спецификація для ERC-20 transfer methods { function transfer(address, uint256) external returns (bool) envfree; function balanceOf(address) external returns (uint256) envfree; function totalSupply() external returns (uint256) envfree; } // Інваріант: сума всіх балансів = totalSupply invariant totalSupplyIsSum(address a, address b) a != b => balanceOf(a) + balanceOf(b) <= totalSupply(); // Правило: transfer зменшує баланс відправника rule transferDecreasesBalance(address sender, address recipient, uint256 amount) { require sender != recipient; require balanceOf(sender) >= amount; uint256 balanceBefore = balanceOf(sender); env e; require e.msg.sender == sender; transfer(e, recipient, amount); assert balanceOf(sender) == balanceBefore - amount; } // Правило: transfer ніколи не створює токени з повітря rule noTokenCreation(method f, address a) { uint256 totalBefore = totalSupply(); env e; calldataarg args; f(e, args); assert totalSupply() <= totalBefore; } 

Prover намагається знайти counterexample. Якщо не знайдено — специфікація вважається доведеною.

Solidity SMTChecker

Вбудований у компілятор Solidity інструмент на основі SMT (Satisfiability Modulo Theories). Активується через pragma або флаги компілятора:

// SPDX-License-Identifier: MIT pragma solidity ^0.8.20; // Включаємо SMT перевірку /// @custom:smtchecker abstract-function-nondet contract VaultVerified { mapping(address => uint256) public balances; uint256 public totalDeposited; function deposit(uint256 amount) external { require(amount > 0, "Zero amount"); balances[msg.sender] += amount; totalDeposited += amount; } function withdraw(uint256 amount) external { require(balances[msg.sender] >= amount, "Insufficient balance"); balances[msg.sender] -= amount; totalDeposited -= amount; } } 

Запускається через налаштування modelChecker в Hardhat. SMTChecker автоматично перевіряє переповнення, underflow та інваріанти.

Halmos — symbolic execution для Foundry

Halmos символічно виконує існуючі Foundry-тести для всіх можливих вхідних даних:

contract TestVault is Test { Vault vault; function setUp() public { vault = new Vault(address(token)); } function testFormal_depositWithdraw( uint256 amount, address caller ) public { vm.assume(amount > 0 && amount < type(uint128).max); vm.assume(caller != address(0)); deal(address(token), caller, amount); vm.prank(caller); token.approve(address(vault), amount); vm.prank(caller); vault.deposit(amount); uint256 shares = vault.balanceOf(caller); vm.prank(caller); vault.withdraw(shares); assertGe(token.balanceOf(caller), amount * 99 / 100); } } 

Як специфікація запобігає вразливостям?

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

Типи властивостей для верифікації

Safety properties ("погане ніколи не відбувається"):

• Баланс ніколи не йде в мінус
• totalSupply ніколи не перевищує MAX_SUPPLY
• Тільки owner може викликати pause()
• Reentrancy guard працює коректно

Liveness properties ("хороше зрештою відбувається"):

• Якщо користувач вніс кошти, він може їх вивести
• Proposals зрештою виконуються або відхиляються
• Staker зрештою отримує rewards

Invariants ("завжди вірно"):

• Σ balances = totalSupply (conservation of tokens)
• lockedAmount <= totalDeposited
• Ціна oracle завжди > 0

Приклад специфікації для lending протоколу

methods { function deposit(uint256) external envfree; function borrow(uint256) external envfree; function repay(uint256) external envfree; function liquidate(address) external; function getHealthFactor(address) external returns (uint256) envfree; function collateral(address) external returns (uint256) envfree; function debt(address) external returns (uint256) envfree; } // Інваріант: не можна ліквідувати здорового позичальника rule noLiquidationOfHealthyBorrower(address borrower) { require getHealthFactor(borrower) >= 1e18; env e; liquidate@withrevert(e, borrower); assert lastReverted, "Healthy borrower should not be liquidatable"; } // Інваріант: сума боргів не перевищує суму застав invariant solvencyInvariant(address user) debt(user) * 100 <= collateral(user) * MAX_LTV_PERCENT filtered { f -> !f.isView } // Reentrancy: state не може змінитися двічі в одній транзакції rule noReentrancy(method f) { uint256 collateralBefore = collateral(currentContract); env e; calldataarg args; f(e, args); uint256 collateralAfter = collateral(currentContract); assert collateralAfter >= collateralBefore || collateralAfter <= collateralBefore; } 

Що входить у нашу послугу

Ми пропонуємо повний цикл формальної верифікації для вашого контракту. У результаті ви отримуєте:

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

Наш досвід — 5+ років у блокчейн-розробці, 15+ аудитів смарт-контрактів, верифіковано 3 протоколи з TVL > $200M. Зв'яжіться з нами для оцінки вашого проекту. Замовте формальну верифікацію за 4–8 тижнів.

Обмеження формальної верифікації

Формальна верифікація не є срібною кулею:

• Completeness gap: верифікується лише те, що вказано в специфікації. Якщо атакуючий знайде вектор, не покритий специфікацією — верифікація його не спіймає.
• Scalability: великі контракти (> 1000 рядків) складно верифікувати повністю. Рішення — верифікувати критичні компоненти окремо.
• Oracle assumptions: якщо контракт використовує oracle, верифікація припускає, що oracle повертає коректні дані.
• External calls: взаємодія із зовнішніми контрактами складно специфікувати повністю.

Порівняння методів перевірки

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

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