Втрата $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: взаємодія із зовнішніми контрактами складно специфікувати повністю.
Порівняння методів перевірки
| Тип перевірки | Що знаходить | Вартість | Час |
|---|---|---|---|
| Unit тести | Конкретні сценарії | Низька | 1–2 тижні |
| Fuzz тестування | Випадкові вхідні дані | Низька | 1 тиждень |
| Мануальний аудит | Логічні помилки | Середня | 2–4 тижні |
| Формальна верифікація | Математичне доведення | Висока | 4–8 тижнів |
Порівняння інструментів формальної верифікації
| Інструмент | Тип | Мова специфікації | Складність впровадження | Покриття |
|---|---|---|---|---|
| Certora Prover | Model checking | CVL | Середня | Повне для EVM |
| SMTChecker | SMT-solving | Solidity annotations | Низька | Автоматичне |
| Halmos | Symbolic execution | Foundry тести | Середня | Залежить від тестів |
Формальна верифікація не замінює мануальний аудит — вони доповнюють один одного. Мануальний аудит знаходить логічні помилки в бізнес-логіці, верифікація доводить коректність математичних властивостей.
Часті запитання (натисніть, щоб розгорнути)
- Чим формальна верифікація відрізняється від звичайного аудиту? Звичайний аудит шукає помилки в коді, а формальна верифікація доводить їх відсутність. Для критичних контрактів це єдиний спосіб гарантувати безпеку за будь-яких вхідних даних.
- Скільки часу займає повна верифікація? Зазвичай від 4 до 8 тижнів залежно від складності протоколу. Етапи включають специфікацію, написання правил, ітеративну верифікацію та звіт.
- Які інструменти ви використовуєте? Certora Prover для EVM-контрактів, Halmos для symbolic execution, а також вбудований SMTChecker в Solidity. Вибір залежить від розміру контракту та необхідної глибини.
- Чи можна верифікувати вже розгорнутий контракт? Так, якщо є вихідний код. Однак виправлення помилок після деплою потребуватиме оновлення через proxy або міграції.
- Які гарантії ви даєте? Ми гарантуємо математичне доведення всіх зазначених у специфікації властивостей. Якщо після верифікації знайдено помилку, ми безкоштовно виправляємо специфікацію та повторно доводимо коректність.
Зв'яжіться з нами для обговорення вашого проекту. Отримайте математичне доведення безпеки вашого смарт-контракту.