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

Сегодня поговорим про общие теоретические аспекты формальной верификации, проблемы SAT и SMT и закрепим все это на простом примере с использованием хайпового инструмента для анализа смарт-контрактов Certora Prover со своим языком спецификаций.

Что такое формальная верификация

Для начала нужно дать несколько определений и пояснений.Формальные методы проверки ПО используются для анализа и подтверждения корректности работы программ и для доказательства свойств систем. Они представляют собой строгие математические подходы к моделированию и анализу программного обеспечения и его поведения.

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

В общем виде формальная верификация включает в себя:

• спецификацию, которая является формальным описанием системы, логики программного обеспечения, выражением того, что от нее требуется;

• реализацию — готовую систему;

• доказательство, которое связывает спецификацию и реализацию и отвечает на вопрос, соответствуют ли они друг другу.

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

Инструменты верификации

На рынке представлено очень много видов инструментов для использования формальных методов:

1. Интерактивные средства для доказательства теорем (K, Coq, Isabelle/HOL, Dafny). В них реализован следующий подход к подтверждению корректности кода: программист пишет математическое доказательство модели, а дополнительные инструменты извлекают из него код.

2. Автоматические средства для доказательства теорем (SAT- и SMT-решатели), которые дают на выходе контрпримеры. В индустрии SMT-решатели используются для работы с различными логиками и теориями, такими как целочисленная арифметика, линейная арифметика, массивы, битовые операции. Они предназначены для более сложных задач, чем те, которые могут быть выражены только булевыми формулами.

3. Языки спецификаций (CVL, Act), которые представляют собой формальное описание системы и используются для проверки модели.

4. Программные логики, например логика Хоара, предоставляют формальный способ для определения и верификации поведения компьютерных программ с помощью пред- и постусловий.

SAT и SMT

Задача выполнимости булевых формул (SAT) заключается в определении того, можно ли найти набор значений переменных, который удовлетворяет определенной булевой формуле. Эта задача относится к классу NP-полных; они известны высокой вычислительной сложностью, что делает их решение за разумное время весьма затруднительным, особенно при увеличении объема данных.

Задача выполнимости формул в теориях (SMT) — это обобщение задачи SAT, которое включает дополнительные теории, в том числе теории целых и вещественных чисел, теории списков, массивов, битовых векторов.

В чем заключается задача SAT? Пусть у вас есть булева формула, которая состоит из переменных, операторов логической конъюнкции (AND), дизъюнкции (OR) и отрицания (NOT). Задача состоит в том, чтобы определить, существует ли такой набор значений (истина или ложь) для переменных, при котором вся формула будет истинной.

Булевы формулы годятся только для представления конечных пространств состояний. В смарт-контрактах пространство состояний обычно включает структуры (например, массивы), которые не ограничены, поэтому необходимо более комплексное понятие удовлетворительности.

SMT-решатели — это инструменты, которые предназначены для решения задач выполнимости булевых формул и содержат операции и предикаты из различных теорий.

Существует множество программ с открытым исходным кодом для решения задач с SMT-ограничениями, в том числе Z3, CVC4, CVC5, Yices, Vampire, Boolector, Eldarica.

Как работает SMT-решатель

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

Рассмотрим примеры задач.

Дана формула:

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

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

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

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

Решений нет.

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

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

• функция f;

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

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

Суммируем:

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

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

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

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

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

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

Certora Prover

Архитектура

Компания Certora предлагает набор инструментов для аудита смарт-контрактов, включая обнаружение уязвимостей и предоставление гарантий того, что основные свойства системы всегда сохраняются.

В возможности инструмента входят:

• Solidity-подобный язык спецификаций CVL и проверка соответствия;

• инструмент мутационного тестирования Gambit;

• проверка эквивалентности двух функций (она еще не доработана, поэтому можно проверить эквивалентность только двух pure-функций).

Инструмент проводит все сложные вычисления на удаленном сервере, поэтому Certora Prover доступен для всех в бесплатной пробной версии. Без премиум-ключа вычислительная мощность и объем памяти решателя ограничены. Компания предоставляет премиум-ключ бесплатно на два месяца. 

Вот как это работает:

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), которые позволяют повысить качество и безопасность разрабатываемых программ. Они включают в себя как новейшие разработки в области формальной верификации, так и проверенные временем методики — статический анализ, тестирование и фаззинг. 

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