Формальные методы проверки смарт-контрактов. Certora Prover

Друзья, приветствую! Меня зовут Сергей Соболев, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье начну рассказывать про методы и инструменты формальной верификации, их практическое применение в аудите смарт-контрактов, а также про подводные камни.

Сегодня поговорим про общие теоретические аспекты формальной верификации, проблемы

Можно ли найти целочисленные значения a, b, c?

Да, решения есть:

Решатель переводит уравнение в несколько другой вид: проще говоря, начинает от обратного в поисках решения уравнения с отрицанием.

Есть ли решения у следующей формулы?

Решений нет.

Почему SMT-решателю дается противоположное утверждение? Потому что, если SMT-решатель говорит, что данная формула неудовлетворительна (нет решений), это является доказательством того, что изначальное утверждение было верным.

Если представить это в коде на языке Solidity, то получится следующее:

• функция f;

• два оператора require, которые накладывают ограничения на входные данные;

• оператор assert, от которого все зависит и который проверяется SMT-решателем.

Суммируем:

1. Логика смарт-контракта переводится в операторы SMT. 

2. Если SMT-решатель говорит, что утверждение безопасно, то оно действительно безопасно.

3. Если SMT-решатель говорит, что утверждение небезопасно, то будет приведен контрпример и его нужно проверять.

Принцип работы

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

1. Инструмент получает байт-код EVM. 

2. Декомпилирует его во внутреннее представление ТAC (three-address code).

3. Алгоритм статического анализа выводит верные инварианты кода, радикально упрощая задачу проверки.

4. Затем преобразует его в математические формулы (VC generation) и генерирует условия проверки (verification conditions). 

5. Ищет все случаи поведения, которые нарушают спецификацию (SMT solve). 

6. Генерирует математическое доказательство правильности работы функций контракта.

Certora Prover поддерживает байт-код EVM, но его инструментальная цепочка является универсальной и может быть адаптирована для других байт-кодов, например WebAssembly или eBPF.

Помимо Solidity, разработчики добавили поддержку второго по популярности языка для EVM — Vyper.  Работа с ним ничем не отличается, просто вместо solc берется компилятор для Vyper. Кроме того, в Certora Prover постепенно добавляется поддержка других блокчейн-платформ, например Solana с использованием языка Rust, который преобразуется в LLVM, а затем в eBPF.

Поскольку Certora Prover работает с байт-кодом, а не с исходным кодом, этот инструмент можно использовать для поиска ошибок компилятора.

Разработчики взяли курс на максимальную автоматизацию инструмента и упрощение работы с ним. На диаграмме ниже показано примерное распределение инструментов в разрезе безопасности и автоматизации.

Certora Prover выигрывает по сравнению с инструментами тестирования, фаззинга и статического анализа (Foundry, MythX, Manticore и Echidna) за счет использования мощных спецификаций CVL и применения решателей SMT для выявления потенциально редких путей, показывающих случаи, в которых происходят нарушения. Программы для доказательства, такие как K, Coq и Isabelle/HOL, используются в интерактивном режиме, поэтому про автоматизацию здесь и речи быть не может.

Работа с Certora Prover похожа на юнит-тестирование: ее парадигма так же проста и интуитивно понятна. Вы пишете высокоуровневую спецификацию на языке CVL в виде тестов, и дальше она применяется к программной реализации вашей системы, скомпилированной в байт-код. Этот инструмент работает на основе троек Хоара, спецификация пишется в следующем формате: 

{P} C {Q},

где

P — состояние «до»,

С — переход, вызов функций,

Q — состояние «после». 

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

Пара ценных советов по установке

Для того чтобы установить Certora Prover, понадобятся Python 3.5, Java Development Kit (JDK) 11 или выше и solc, размещенный в $PATH.

Установка:

pip3 install certora-cli

echo 'export PATH="$PATH:/home/<username>/.local/bin"' >> ~/.bashrc

Сохранение премиум-ключа:

echo 'export CERTORAKEY=<premium_key>' >> ~/.bashrc

Компания выступает за автоматизацию всего цикла написания спецификации, для этого предназначен JSON-файл .conf. 

Советую использовать такую структуру папок. В корне каталога можно вызвать команду CLI:

certoraRun certora/conf/<filename>.conf

Язык спецификации

Язык CVL очень похож на Solidity. Он строго типизирован и наследует типы Solidity, кроме mapping, function и многомерных массивов. В этом языке есть свои типы данных. Самый интересный из них — это env, тип окружения, который содержит поля tx, msg, block. С помощью этого типа можно работать с окружением, которое создает Certora Prover.

Ниже приведен пример из спецификации для ERC-20. Это правило проверяет, что никакие функции, кроме mint и burn, не могут менять totalSupply токена. В спецификации есть инвариант «сумма балансов равна общему предложению», он проверяется первым. Далее определяются типы данных, которые я упоминал выше, они определяют окружение, методы контракта и их аргументы.

Вызов totalSupply сохраняет состояние «до», вызывается метод f(), то есть произвольный метод, который представляет собой абстракцию: вместо него по очереди подставляются все методы контракта. Второй вызов totalSupply сохраняет состояние «после». Проверяются утверждения в assert: если они нарушены, то будет приведен контрпример, состоящий из трассировки вызовов с определенными переменными.

Помимо всего прочего, в языке есть встроенные правила, которые можно подключать к спецификации; они используют паттерны в коде. Их список пока небольшой: проверка на read-only reentrancy, поиск delegatecall, поиск повторного использования msg.value и правило sanity для поиска методов, которые невозможно проверить и, следовательно, придется упрощать.

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

Написание спецификации

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

Кроме того, следует отметить, что ошибки в спецификации могут привести к ложным доказательствам корректности. Написание спецификации — это всегда трудоемкий и сложный процесс, иногда, можно сказать, бесконечный. Давайте посмотрим, как это происходит.

Код ниже взят из Ethernaut OZ, уязвимость контракта основана на коллизии storage: вызов delegatecall сохраняет контекст выполнения основного контракта и изменяет в контракте библиотеки слот номер 0, что ведет за собой изменение нулевого слота вызывающего контракта. 

Эту уязвимость очень просто найти с помощью Certora Prover. Первое, что нужно понять, — что делает код. Если библиотека изменяет переменную storedTime, то в основном контракте должно измениться значение storedTime, поэтому мы можем написать такое правило:

Однако это правило не выполняется, и инструмент приводит трассировку вызовов для получения состояния, которое нас не удовлетворяет, — это и есть контрпример.

На скриншоте ниже приведен отчет, слева указаны правила, которые описаны в спецификации: 

• changeStoredTime проверяет, изменилась ли записанная временная метка; это правило нарушено;

• equalityTimeZone1Library предназначено для проверки того, что переменная timeZone1Library в нулевом слоте не изменяется; это правило нарушено;

• параметрическое правило, которое проверило каждый метод контракта и указало, какие из них нарушают правило;

• envfreeFuncsStaticCheck — встроенная проверка того, что методы контракта не зависят ни от одной из переменных окружения;

• hasDelegateCalls — встроенное правило, которое ищет использование delegatecall в контракте.

Справа выводятся все локальные переменные правила, а посередине — трассировка вызовов, где инструмент сохраняет состояние «до», вызывая метод storedTime. Параметр require накладывает ограничения на timeStamp, поэтому его значение не может быть равно или меньше, так как в реальной жизни время течет вперед. От функции setFirstTime ожидается, что она изменит состояние контракта, однако приведенный контрпример доказывает обратное. После изучения отчета вы можете завести функции с переменными справа и проверить наличие этих ошибок.

Заключение

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

Наша компания активно изучает и применяет формальные методы в блокчейнах, и мы понимаем их значимость и эффективность. Certora Prover, один из ведущих инструментов в этой области, демонстрирует впечатляющие результаты в анализе и верификации смарт-контрактов. Однако наш опыт выходит за рамки использования Certora Prover. Мы также активно исследуем и внедряем другие инструменты и методики (Solidity SMTChecker, K Framework, Coq), которые позволяют повысить качество и безопасность разрабатываемых программ. Они включают в себя как новейшие разработки в области формальной верификации, так и проверенные временем методики — статический анализ, тестирование и фаззинг. 

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