Аудит смарт-контрактов: как находят то, что не видит компилятор

В марте 2023 года Euler Finance потерял $197M через flash loan атаку на функцию donateToReserves. Контракт прошёл несколько аудитов. Уязвимость существовала больше года. Аудиторы смотрели на функцию — и не увидели, что она нарушает инвариант health factor в комбинации с liquidate. Это не исключение. Это норма для сложных DeFi-протоколов, где уязвимость — не баг в одной функции, а нарушение инварианта в цепочке вызовов.

Что статический анализ не найдёт

Slither — стандартный первый инструмент. Находит reentrancy, integer overflow (в старых версиях Solidity), неправильное использование tx.origin, shadowing переменных, неинициализированные хранилища. На реальном проекте Slither выдаёт десятки предупреждений, из которых критических — 0-2. Остальное — информационный шум.

Slither не найдёт логическую уязвимость. Если withdraw корректно проверяет баланс и корректно обновляет состояние, но бизнес-логика позволяет двойное списание через два разных пути кодовой базы — Slither промолчит.

Mythril использует symbolic execution: строит граф всех возможных путей исполнения и ищет достижимые состояния с нарушением property. Работает хорошо на изолированных контрактах. На протоколе из 20 контрактов с cross-contract вызовами — path explosion, анализ зависает или выдаёт false positive's.

Оба инструмента обязательны как первый pass. Но они не заменяют ручной анализ.

Fuzzing: где Echidna и Foundry находят реальные баги

Echidna — property-based fuzzer от Trail of Bits. Идея: формулируешь инварианты контракта как Solidity-функции (echidna_invariant), Echidna генерирует случайные последовательности вызовов и пытается сломать инвариант.

Пример инварианта для lending протокола:

function echidna_total_assets_ge_liabilities() public view returns (bool) {
    return totalAssets() >= totalLiabilities();
}

Echidna найдёт последовательность deposit → borrow → liquidate → repay, которая нарушает этот инвариант. Руками такой кейс не построишь — комбинаций слишком много.

Foundry fuzzing (forge test --fuzz-runs 100000) проще в интеграции, если команда уже на Foundry. Поддерживает stateful fuzzing через invariant тесты начиная с версии 0.2.0. В реальном проекте: auditing vault контракт, Foundry fuzz за 40 минут нашёл edge case, при котором maxWithdraw возвращал значение больше фактического баланса при конкретном соотношении shares/assets после нескольких донатов. Hardhat unit-тесты этот кейс пропускали — там не было такой комбинации параметров.

Medusa (от Trail of Bits, новее Echidna) поддерживает corpus-guided fuzzing и работает быстрее на больших контрактах. Если объём кодовой базы > 5000 строк Solidity — смотрим на Medusa.

Формальная верификация: когда нужна и когда нет

Formal verification доказывает, что контракт удовлетворяет спецификации для всех возможных входных данных — не для N случайных, а математически для всех. Инструменты: Certora Prover, K Framework, Halmos.

Certora работает с CVL (Certora Verification Language): пишешь rules и invariants, Prover транслирует их в SMT-формулы и проверяет через Z3/CVC5. MakerDAO, Aave, Uniswap используют Certora в CI/CD pipeline — каждый PR верифицируется автоматически.

Ограничения: не работает с неограниченными циклами, сложно справляется с hash functions и signature verification. Для контрактов с простой математикой (AMM, lending) — отлично. Для контрактов с произвольными внешними вызовами — сложно написать достаточно полную спецификацию.

Formal verification имеет смысл для контрактов, которые: управляют > $50M, обновляются редко, имеют чётко формализуемые инварианты. Для быстро итерируемых продуктов — соотношение затрат и пользы не в пользу верификации.

Векторы атак, которые пропускают джуниор-аудиторы

Storage collision в proxy паттерне. Transparent proxy и UUPS используют конкретные слоты для хранения адреса имплементации (EIP-1967). Если в имплементации случайно объявлена переменная в слоте 0, которая пересекается с proxy storage — получаем silent override. Slither это не поймает, если proxy и имплементация в разных файлах.

Read-only reentrancy. Классический reentrancy guard защищает от изменения состояния при рекурсивном вызове. Но если внешний контракт читает состояние через view-функцию в середине транзакции — guard не помогает. Curve pools в 2023 году стали вектором атаки именно через это: внешний протокол читал get_virtual_price во время reentrancy-уязвимого состояния Curve.

Oracle manipulation через TWAP. Spot price — стандартная цель для flash loan атаки. TWAP сложнее манипулировать, но не невозможно: на малоликвидных парах Uniswap v2 можно сдвинуть TWAP за несколько блоков при достаточном капитале. Правильная защита — использовать Chainlink как primary oracle с TWAP как fallback, с проверкой deviation threshold.

Gas griefing на unbounded loop. Функция итерируется по массиву пользователей. Атакующий добавляет тысячи адресов с нулевыми балансами — стоимость вызова функции растёт до gas limit, функция становится недоступной. Защита: pull-pattern вместо push, ограничение длины массивов, batch-обработка с сохранением позиции.

Front-running на MEV. Транзакция видна в mempool до включения в блок. MEV-бот видит addLiquidity на значительную сумму, вставляет свой swap перед ней (sandwich attack). Для AMM это часть модели. Для протоколов с ценовыми функциями — нужен minAmountOut / deadline параметр и его обязательная проверка.

Структура полного аудита

Работа начинается со scope definition: список контрактов, commit hash, версия компилятора, список out-of-scope. Без фиксированного commit результаты аудита теряют смысл.

Фаза 1 — автоматический анализ (1-2 дня). Slither, Mythril, Aderyn. Triage: что реально критично, что false positive. Составляем карту зависимостей контрактов.

Фаза 2 — ручной анализ (основная часть, 5-15 дней). Каждый контракт построчно. Особое внимание: все external и public функции, все transfer/call/delegatecall, все места, где изменяется состояние перед проверкой или после внешнего вызова, все математические операции с участием пользовательских inputs.

Фаза 3 — fuzzing и тестирование (2-5 дней). Echidna или Foundry invariant tests для критических инвариантов. Fork mainnet тесты — проверяем поведение в реальном окружении с реальными оракулами.

Фаза 4 — отчёт и митигация. Отчёт с severity (Critical/High/Medium/Low/Informational), описанием вектора атаки, PoC-кодом для Critical/High. Разработчики исправляют, аудиторы делают re-audit исправлений.

Аудит в CI/CD

Нормальная практика для зрелых протоколов: Slither и Aderyn запускаются в GitHub Actions на каждый PR. Certora Prover — на merge в main. Это не заменяет полный аудит перед деплоем, но ловит регрессии.

# .github/workflows/audit.yml
- name: Run Slither
  uses: crytic/[email protected]
  with:
    target: 'src/'
    slither-args: '--filter-paths "test|mock|script"'

Сроки

Аудит простого токена или NFT-контракта — 3-5 рабочих дней. DeFi протокол с lending/AMM — 2-4 недели. Полный стек с несколькими протоколами, cross-chain, proxy upgrades — 4-8 недель. Re-audit исправлений — 3-7 дней отдельно.

Экономить на аудите имеет смысл ровно один раз: до первого взлома.