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

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

Формальная верификация — это математическое доказательство корректности программы. Не "мы проверили все test cases", а "мы доказали, что для любых входных данных контракт ведёт себя согласно спецификации". Разница критическая: тесты находят присутствие ошибок, верификация доказывает их отсутствие. 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 пытается найти counterexample — набор входных данных, при которых assertion нарушается. Если 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");

        // SMTChecker автоматически проверит:
        // - нет overflow в balances[msg.sender] += amount
        // - нет overflow в 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 — symbolic execution для 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
        // баланс восстанавливается (с учётом fees)
        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 протокола

// Спецификация для упрощённого 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: state не может измениться дважды в одной транзакции
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
}

Ограничения формальной верификации

Формальная верификация не является серебряной пулей:

Completeness gap: верифицируется только то, что указано в спецификации. Если атакующий найдёт вектор, который не покрыт спецификацией — верификация его не поймает. Именно это произошло с рядом "верифицированных" протоколов.

Scalability: большие контракты (> 1000 строк) сложно верифицировать полностью. Инструменты могут не завершиться за разумное время (timeout). Решение — верифицировать критические компоненты по отдельности.

Oracle assumptions: если контракт использует oracle, верификация предполагает что oracle возвращает корректные данные. Некорректный oracle — за рамками верификации.

External calls: взаимодействие с внешними контрактами сложно специфицировать полностью. Certora требует явного указания поведения внешних вызовов через summarization.

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

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

Этап 1 — Спецификация требований: совместно с командой протокола определяем критические свойства, которые должны держаться при любых условиях.

Этап 2 — Написание CVL/Halmos спецификаций: 2-4 недели для типичного DeFi протокола. Покрываем safety invariants, access control, economic invariants.

Этап 3 — Итеративная верификация: запуск Prover, анализ counterexamples, уточнение спецификации или исправление кода. Это итерационный процесс.

Этап 4 — Репорт: список верифицированных свойств, найденных нарушений, ограничений верификации.

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

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