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

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

Формальна верифікація — це математичне доведення коректності програми. Не «ми перевірили всі тестові випадки», а «ми довели, що для будь-яких вхідних даних контракт поводиться відповідно до специфікації». Різниця критична: тести знаходять наявність помилок, верифікація доводить їхню відсутність. MakerDAO, Aave, Compound використовують формальну верифікацію для критичних компонентів. Розглянемо, як це працює на практиці.

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

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

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");

        // SMTChecker автоматично перевіряє:
        // - немає переповнення в balances[msg.sender] += amount
        // - немає переповнення в totalDeposited += amount
        // - інваріант: totalDeposited = Σ balances[i]

        balances[msg.sender] += amount;
        totalDeposited += amount;
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");

        balances[msg.sender] -= amount;
        totalDeposited -= amount;
        // assert не потрібен — SMTChecker перевіряє що underflow неможливий
    }
}

Запуск через Hardhat:

npx hardhat compile --config hardhat.smtchecker.config.ts

// hardhat.smtchecker.config.ts
export default {
    solidity: {
        version: "0.8.20",
        settings: {
            modelChecker: {
                engine: "chc",        // Constrained Horn Clauses — найпотужніший
                targets: [
                    "assert",
                    "overflow",
                    "underflow",
                    "divByZero",
                    "constantCondition",
                    "balance"
                ],
                timeout: 20000,       // мілісекунди на кожну перевірку
                showUnproved: true
            }
        }
    }
};

Halmos

Halmos — символічне виконання для EVM, написан на Python. Працює з існуючими тестами Foundry — символічно виконує їх для всіх можливих вхідних даних:

// Тест Foundry стає формальною верифікацією у Halmos
// Запуск: halmos --contract TestVault --function testFormal

contract TestVault is Test {
    Vault vault;

    function setUp() public {
        vault = new Vault(address(token));
    }

    // Halmos запустить це для ВСІХ можливих значень amount та caller
    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);

        // Для всіх можливих amount та caller: після deposit+withdraw
        // баланс восстановлюється (з урахуванням комісій)
        assertGe(token.balanceOf(caller), amount * 99 / 100);
    }
}

Специфікація: найскладніша частина

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

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

Властивості безпеки («погане ніколи не відбувається»):

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

Властивості життєвості («хороше врешті-решт відбувається»):

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

Інваріанти («завжди істинно»):

• Σ balances = totalSupply (збереження токенів)
• lockedAmount <= totalDeposited
• Ціна оракула завжди > 0

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

// Специфікація для спрощеного Aave-подібного протоколу

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; // health factor >= 1.0

    env e;
    liquidate@withrevert(e, borrower);

    assert lastReverted, "Healthy borrower should not be liquidatable";
}

// Інваріант: сума боргів не перевищує суму заставок (з коефіцієнтом LTV)
invariant solvencyInvariant(address user)
    debt(user) * 100 <= collateral(user) * MAX_LTV_PERCENT
    filtered { f -> !f.isView }

// Reentrancy: стан не може змінитися дважды у одній транзакції
rule noReentrancy(method f) {
    uint256 collateralBefore = collateral(currentContract);

    env e;
    calldataarg args;
    f(e, args);

    uint256 collateralAfter = collateral(currentContract);

    // Баланс змінився точно як очікується
    assert collateralAfter >= collateralBefore || /* withdrawal */
           collateralAfter <= collateralBefore; // deposit
}

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

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

Прогалина повноти: верифікується тільки те, що вказано у специфікації. Якщо атакувальник знайде вектор, не охоплений специфікацією — верифікація його не виявить. Це трапилося з деякими «верифікованими» протоколами.

Масштабованість: великі контракти (> 1000 рядків) важко верифікувати повністю. Інструменти можуть не завершити за розумний час (timeout). Рішення — верифікувати критичні компоненти окремо.

Припущення оракула: якщо контракт використовує оракул, верифікація припускає, що оракул повертає коректні дані. Неправильний оракул — поза межами верифікації.

Зовнішні дзвінки: взаємодія з зовнішніми контрактами важко специфікувати повністю. Certora вимагає явного вказання поведінки зовнішніх дзвінків через summarization.

Процес верифікаційного аудиту

Повний процес формальної верифікації:

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

Етап 2 — Написання CVL/Halmos специфікацій: 2-4 тижні для типового DeFi протоколу. Охоплюємо safety інваріанти, контроль доступу, економічні інваріанти.

Етап 3 — Ітеративна верифікація: запуск Prover, аналіз контрприкладів, уточнення специфікації або виправлення коду. Це ітеративний процес.

Етап 4 — Звіт: список верифікованих властивостей, знайдених порушень, обмежень верифікації.

Типова вартість верифікаційного аудиту — $50k-$200k залежно від складності протоколу. Суттєво дорожче, ніж звичайний аудит, але виправдано для контрактів з $100M+ TVL: вартість знаходження однієї критичної вразливості вартістю $10k у специфікації може запобігти втраті $10M.

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