Формальная верификация смарт-контрактов с помощью Certora Prover

Ошибка в смарт-контракте стоит дорого: контракты управляют токенами, депозитами и кредитными позициями, и баг означает прямые потери денег. Поэтому безопасность контрактов проверяют несколькими способами сразу, чаще всего ручным аудитом и автоматическими тестами.

Есть и третий способ, формальная верификация. Тест проверяет поведение на конкретных входных данных, а формальная верификация доказывает свойство для всех возможных состояний контракта или находит контрпример, на котором оно ломается.

Один из инструментов формальной верификации для Solidity называется Certora Prover. На его примере видно, что такая проверка получает на вход, как она устроена и как выглядит на контракте ERC-20.

Что такое Certora Prover

Prover автоматизирует доказательство: выводить математические доказательства вручную не нужно. На вход Prover получает исходный код контракта и спецификацию, то есть описание свойств, которым код должен соответствовать. Спецификацию пишут на языке CVL (Certora Verification Language).

На выходе получается отчёт. По каждому свойству он показывает, доказано ли оно для всех сценариев или найден контрпример, то есть последовательность вызовов, при которой свойство нарушается.

Как устроена проверка

Prover компилирует Solidity-код в байткод EVM, а байткод декомпилирует в трёхадресный код (Three-Address Code, TAC). TAC длиннее исходника, зато каждый шаг вычислений в нём простой, и анализировать его удобнее.

Затем статический анализ оптимизирует TAC: например, выбрасывает участки программы, которые не влияют на проверяемое свойство. Оптимизированный код вместе со спецификацией на CVL Prover переводит в логические формулы и передаёт солверу ограничений (constraint solver), например Z3 или CVC5. Солвер либо доказывает свойство, либо находит контрпример.

Индукция и тройки Хоара

В основе Prover две классические идеи формальной верификации: индукция и тройка Хоара.

Индукция позволяет не симулировать длинные цепочки вызовов. Prover проверяет свойство для состояния сразу после конструктора и для произвольного состояния контракта. Если свойство выполнялось до вызова любой функции, оно должно выполняться и после. Чтобы произвольное состояние не оказалось нереалистичным, в спецификацию добавляют ограничения на начальное состояние.

Тройка Хоара записывается как {P} C {Q}, где P обозначает предусловие, C команду, а Q постусловие. Предусловие описывает состояние системы до команды, а постусловие ожидаемое состояние после неё. Если предусловие выполнено, корректная реализация команды обязана обеспечить постусловие.

В CVL эти идеи выражаются через правила (rule) и инварианты (invariant). Правило описывает конкретный сценарий: задаёт последовательность действий и проверяет, что после них выполняется нужное свойство. Инвариант описывает свойство, которое должно сохраняться всегда, на любом этапе жизни системы.

Разница между ними в области применения. Любой инвариант можно записать как правило, но не любое правило можно записать инвариантом. Кроме того, инварианты Prover проверяет начиная с состояния после конструктора, а правила из произвольного состояния, без отдельной проверки конструктора.

Вот правило, которое проверяет поведение функций: после вызова любой функции контракта значение contractOwner не меняется.

rule contractOwnerNeverChange(env e) {
    address owner = contractOwner();
    method f;
    calldataarg args;
    f(e, args);
    assert owner == contractOwner();
}

А вот инвариант, описывающий свойство состояния: totalSupply всегда равен сумме балансов всех пользователей.

invariant totalSupplyIsSumOfBalances()
    totalSupply() == sumOfBalances;

Правило contractOwnerNeverChange нельзя переписать инвариантом: инвариант в Certora Prover не может запомнить значение переменной до вызова функции и сравнить его со значением после.

Тайм-ауты и как с ними справляться

Не каждая проверка заканчивается доказательством или контрпримером. На вычислительно сложных свойствах солвер может упереться во внутренние ограничения, и проверка завершится тайм-аутом.

Против тайм-аутов чаще всего применяют аппроксимацию. Участки кода, которые не влияют на проверяемое свойство, заменяют более простыми моделями. Сверхаппроксимация заменяет функцию более простой, которая возвращает значения из более широкого диапазона. Недоаппроксимация, наоборот, сужает диапазон значений, поэтому её применяют осторожнее: она уменьшает полноту проверки.

Ещё помогают переписать спецификацию и настроить Prover: выбрать другой солвер и поменять параметры анализа.

Где Prover полезен в жизненном цикле проекта

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

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

При этом аудит и тесты Prover не заменяет.

Пример: ERC-20

Возьмём базовый ERC-20, один из самых распространённых контрактов в блокчейне. Для него проверяют, что балансы меняются корректно, что totalSupply равен сумме балансов всех пользователей, а трансферы и разрешения работают правильно. После запуска Prover выдаёт отчёт со списком всех свойств и результатом проверки каждого. Если свойство нарушено, в отчёте есть стек вызовов и значения переменных, по которым можно разобрать сценарий ошибки.

На скриншоте показан инвариант «totalSupply равен сумме балансов всех пользователей» и вспомогательные ghost-переменные и хуки, через которые Prover считает сумму балансов.

А здесь Prover нашёл контрпример: правило для permit нарушается, и отчёт показывает последовательность вызовов и значения переменных, на которых это происходит.

Итог