Потеря $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 или миграции.
- Какие гарантии вы даёте? Мы гарантируем математическое доказательство всех указанных в спецификации свойств. Если после верификации найдена ошибка, мы бесплатно исправляем спецификацию и повторно доказываем корректность.
Свяжитесь с нами для обсуждения вашего проекта. Получите математическое доказательство безопасности вашего смарт-контракта.