Формальная верификация смарт-контрактов для 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: взаимодействие с внешними контрактами сложно специфицировать полностью.

Сравнение методов проверки

Сравнение инструментов формальной верификации

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