Блокчейн
Формальная верификация контрактов
В 2023 году DeFi-протоколы потеряли более 1.8 миллиарда из-за уязвимостей в смарт-контрактах. Тесты покрывали все известные сценарии, аудиторы проверяли код строка за строкой, а взломы всё равно происходили. Проблема в том, что тестирование проверяет конечное число случаев, а атакующий ищет единственный пропущенный. Формальная верификация меняет правила игры: вместо проверки тысячи входов она математически доказывает, что свойство выполняется для ВСЕХ возможных входов. Это не тестирование с большим покрытием. Это математическое доказательство корректности.
- **Aave V3** - крупнейший lending-протокол (10B+ TVL) использует Certora для формальной верификации всех ключевых контрактов. Более 200 CVL-правил проверяют: корректность ликвидаций, целостность accounting, невозможность вывести чужие средства. Спецификации опубликованы в open-source
- **Compound V3 (Comet)** - перед запуском прошёл формальную верификацию через Certora с 80+ правилами и инвариантами. Каждое обновление протокола ре-верифицируется. Результат: ноль критических инцидентов после запуска
- **Uniswap V2** - Runtime Verification (создатели K Framework) формально доказали через KEVM корректность AMM-формулы x*y=k: swap-операция всегда сохраняет инвариант, liquidity providers не теряют средства при корректном использовании
Предварительные знания
Symbolic Execution: выполнение программы с переменными вместо значений
Обычное тестирование проверяет контракт на конкретных входах: "если пользователь внёс 1 ETH, может ли он вывести 2?" Но входных данных - бесконечное множество. **Symbolic execution** переворачивает подход: вместо конкретных значений в переменные подставляются **символы** (α, β, γ), и программа выполняется одновременно по всем возможным путям. На каждом ветвлении (`if`, `require`) путь разделяется, и для каждой ветки копится набор **ограничений** (constraints) на символы. Если хотя бы один путь приводит к нарушению инварианта - инструмент нашёл баг.
Основные инструменты symbolic execution для смарт-контрактов: **Mythril** (ConsenSys) - анализирует EVM-байткод, находит reentrancy, integer overflow, selfdestruct. **Manticore** (Trail of Bits) - символическое выполнение с Python API для написания собственных детекторов. **HEVM** (dapptools/Foundry) - symbolic execution прямо из Foundry-тестов с использованием `vm.assume()` и cheatcodes.
Главная проблема symbolic execution - **path explosion** (взрыв путей). Каждый `if` удваивает количество путей, цикл `for(i=0; i<n; i++)` создаёт n путей. Контракт с 30 вложенными ветвлениями имеет 2^30 ≈ 1 миллиард путей. Решение - **bounded model checking**: ограничиваем глубину анализа (например, до 3 транзакций или 128 итераций цикла). Это компромисс: мы не проверяем все возможные пути, но находим баги в разумное время.
Контракт содержит функцию с двумя require() и одним if-else внутри каждой ветки. Сколько уникальных путей выполнения исследует symbolic execution?
SMT-солверы: математический движок верификации
Symbolic execution собирает ограничения вида `β >= α ∧ α > 0 ∧ β < 2^256`. Но кто решает, существуют ли значения α и β, удовлетворяющие этим ограничениям? Эту работу выполняют **SMT-солверы** (Satisfiability Modulo Theories) - программы, которые отвечают на вопрос: "Существует ли набор значений, при котором формула истинна?" SAT-солверы работают с булевыми формулами (true/false), а SMT расширяет их **теориями** - арифметикой целых чисел, битовыми векторами, массивами. Для EVM особенно важна теория **битовых векторов** (bitvector), потому что uint256 - это именно 256-битный вектор с модулярной арифметикой.
Solidity начиная с версии 0.8.4 имеет **встроенный SMTChecker** - формальный верификатор прямо в компиляторе. Он использует Z3 или Eldarica и проверяет: underflow/overflow, деление на ноль, assert-ы, выход за границы массива, недостижимый код. Активируется через `pragma experimental SMTChecker;` или настройку в `solc --model-checker-engine all`. Это самый доступный инструмент формальной верификации - не требует отдельной установки.
SMT-солверы имеют фундаментальное ограничение: для некоторых теорий задача **неразрешима** (undecidable). Нелинейная арифметика (`a * b > c * d` где все - переменные), рекурсивные структуры данных и бесконечные циклы могут привести к ответу `unknown` вместо `sat`/`unsat`. На практике это означает, что солвер может работать минутами, часами или не завершиться вовсе. Инструменты формальной верификации устанавливают **таймауты** и ограничения на глубину анализа - полнота приносится в жертву практичности.
SMT-солвер анализирует функцию transfer(), у которой есть require(balance >= amount) перед вычитанием balance - amount. Солвер пытается найти значения, при которых результат вычитания больше исходного balance (underflow). Какой результат вернёт солвер?
Certora Prover: промышленная верификация DeFi-протоколов
Mythril и SMTChecker ищут **известные классы багов** (overflow, reentrancy). Но как доказать, что `totalSupply` токена **всегда** равен сумме всех балансов? Или что ни один пользователь не может вывести больше, чем внёс? Для этого нужно формулировать **собственные свойства** - и здесь начинается **Certora Prover**. Certora использует язык спецификаций **CVL** (Certora Verification Language) для описания правил, инвариантов и свойств, которые SMT-солвер проверяет на EVM-байткоде контракта. Aave, Compound, MakerDAO, Lido и десятки других протоколов используют Certora для формальной верификации перед деплоем.
Certora работает как облачный сервис: `certoraRun Token.sol --verify Token:Token.spec`. Пруверу требуется от 5 минут до нескольких часов в зависимости от сложности контракта и спецификации. Результаты доступны в веб-интерфейсе с визуализацией контрпримеров. Certora предоставляет бесплатный тариф для open-source проектов и активно сотрудничает с аудиторскими компаниями.
Формальная верификация через Certora **не гарантирует** отсутствие всех багов. Она доказывает, что контракт соответствует **спецификации** - но спецификация сама может быть неполной или некорректной. Если вы забыли описать свойство - Certora его не проверит. Кроме того, Certora не анализирует: экономические атаки (flash loans, MEV), ошибки в конфигурации (неправильные адреса, привилегии), проблемы на уровне инфраструктуры (приватные ключи, oracle manipulation). Формальная верификация - гибкий инструмент, но лишь один слой в defense in depth.
В CVL-спецификации Certora определено параметрическое правило: для ЛЮБОЙ функции контракта f, вызванной пользователем X, баланс пользователя Y (где X ≠ Y) не должен уменьшаться. Certora сообщает VIOLATION с контрпримером: функция transferFrom(Y, Z, amount) вызвана X с allowance. Что это означает?
K Framework: формальная семантика EVM
Certora доказывает свойства контракта, интерпретируя его байткод. Но насколько точна эта интерпретация? Что если сам **инструмент верификации** неправильно понимает, как работает EVM? **K Framework** решает проблему радикально: вместо интерпретации байткода он создаёт **формальную математическую семантику** EVM - полное описание каждого опкода, каждого правила gas-расчёта, каждого edge case. Это проект **KEVM** (K Ethereum Virtual Machine), разработанный компанией **Runtime Verification**. Имея формальную семантику, можно доказывать свойства контрактов с математической строгостью, где каждый шаг EVM определён однозначно.
Самый известный проект верификации через K Framework - **Uniswap V2**. Runtime Verification формально доказала корректность ключевых свойств AMM: формула `x * y = k` сохраняется после каждого swap, liquidity providers не теряют средства при корректном использовании, а swap-операция всегда выполняется по заявленной цене. Другие проекты: **Gnosis Safe** (multisig wallet), **Ethereum 2.0 deposit contract**, **ERC-20** reference implementation.
На практике выбор инструмента зависит от требований проекта. Для большинства DeFi-протоколов **Certora** - оптимальный выбор: понятный язык, облачная инфраструктура, результаты за минуты. **K Framework** применяется для критической инфраструктуры, где нужна абсолютная математическая строгость: core-протоколы (Uniswap, Gnosis), мосты, системные контракты Ethereum. Оба инструмента не заменяют аудит и тестирование - они дополняют их, формируя ещё один уровень defense in depth.
Формальная верификация гарантирует, что контракт не содержит багов - если Certora или K Framework говорят 'verified', контракт абсолютно безопасен и аудит не нужен
Формальная верификация доказывает соответствие контракта спецификации - набору свойств, написанных человеком. Если спецификация неполна (забыли описать edge case), некорректна (ошибка в формулировке свойства), или не покрывает целый класс угроз (экономические атаки, oracle manipulation, governance attacks), верификация этого не обнаружит. Контракт верифицирован настолько, насколько хороша его спецификация.
Взлом Euler Finance ($197M, март 2023) произошёл несмотря на формальную верификацию отдельных компонентов - атака эксплуатировала взаимодействие между модулями, которое не было покрыто спецификацией. Beanstalk ($182M, апрель 2022) был атакован через flash loan governance attack - тип угрозы, который формальная верификация не проверяла. Верификация не заменяет аудит, fuzzing и мониторинг - она дополняет их как один из уровней defense in depth.
DeFi-протокол управляет 2B TVL. Команда хочет формально верифицировать контракт. Certora Prover подтверждает все 47 правил CVL-спецификации. K Framework верифицирует ключевые инварианты через KEVM. Можно ли считать контракт полностью безопасным?
Итоги
- **Symbolic execution** выполняет программу с символами вместо конкретных значений, исследуя все пути одновременно. На каждом ветвлении путь разделяется, копятся ограничения (constraints). Path explosion - главный враг, решаемый через bounded model checking
- **SMT-солверы** (Z3, Bitwuzla) - математические движки, решающие системы ограничений от symbolic execution. Для EVM критична теория битовых векторов (uint256 = 256-bit bitvector). Solidity SMTChecker использует Z3 прямо в компиляторе
- **Certora Prover** позволяет описывать собственные свойства на языке CVL: инварианты (`totalSupply == Σ balances`), правила (transfer не меняет totalSupply), параметрические правила (ни одна функция не уменьшает чужой баланс). Ghost variables и hooks связывают спецификацию с storage контракта
- **K Framework / KEVM** - формальная семантика EVM: математическое определение каждого из 140+ опкодов. В отличие от Certora (property-based), K Framework верифицирует через точную модель EVM, что устраняет ошибки абстракции. Используется для критической инфраструктуры (Uniswap, Gnosis Safe)
- Ни один инструмент не заменяет все остальные. DeFi-протоколы потеряли 1.8B за год, несмотря на тестирование и аудиты - формальная верификация добавляет математическую строгость, но проверяет только то, что описано в спецификации. **Defense in depth**: SMTChecker → Mythril → Certora → аудит → fuzzing → мониторинг
Связанные темы
Формальная верификация - один из уровней безопасности смарт-контрактов, тесно связанный с другими методами защиты:
- Reentrancy и классические атаки — Symbolic execution инструментов вроде Mythril автоматически обнаруживает reentrancy-паттерны. Certora позволяет доказать отсутствие reentrancy через инвариант на state transitions
- Безопасность: overflow и underflow — SMT-солверы идеально подходят для поиска integer overflow - Z3 решает задачу 'может ли uint256 переполниться' за миллисекунды. SMTChecker Solidity находит overflow на этапе компиляции
- Fuzzing смарт-контрактов — Fuzzing (Echidna, Foundry) и формальная верификация - комплементарные подходы: fuzzing находит баги быстро, верификация доказывает отсутствие целых классов багов. Лучшие протоколы используют оба
- Аудит безопасности — Формальная верификация не заменяет ручной аудит: экономические атаки, governance-уязвимости и архитектурные проблемы требуют человеческого анализа. Верификация + аудит = defense in depth
Вопросы для размышления
- Certora-спецификация для ERC-20 токена содержит 50 правил и все показывают VERIFIED. Означает ли это, что токен невозможно взломать? Какие типы атак останутся за пределами даже идеальной CVL-спецификации?
- K Framework даёт академическую строгость, но требует месяцы работы и узких специалистов. Certora проще в использовании, но зависит от абстракции EVM. Для стартапа с 5M TVL и ограниченным бюджетом - какой уровень формальной верификации оправдан? Можно ли обойтись только SMTChecker и Mythril?
- Формальная верификация Compound V3 стоила сотни тысяч долларов и заняла месяцы. В то же время, один разработчик с Foundry может за неделю написать обширную fuzzing-кампанию. С точки зрения ROI на безопасность - когда формальная верификация оправдывает свою стоимость, а когда fuzzing достаточно?