Формальная верификация смарт-контрактов во фреймворке ConCert / forpes.ru

Главная
Формальная верификация смарт-контрактов во фреймворке ConCert

Формальная верификация смарт-контрактов во фреймворке ConCert

03.04.2024 15:32

krlzi 0 492 Источник

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

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

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

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

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

Среды интерактивного доказательства

Дедуктивная верификация ПО обычно производится в средах автоматического или интерактивного доказательства теорем (также называемых proof assistants). В средах автоматического доказательства (Why3, PVS, Z3 и других) доказательства (или контрпримеры) генерируются автоматически с помощью SAT- и SMT-решателей, а пользователь не принимает непосредственного участия в дедукции. Основной проблемой такого метода является ограниченность класса утверждений, которые могут быть доказаны автоматически. Кроме того, в случае неудачи автоматического доказательства зачастую трудно понять, что пошло не так и является ли свойство доказуемым в принципе.

Что касается интерактивных доказательств в proof assistants (наиболее популярными из которых являются Coq, Lean, Isabelle и семейство HOL), то такие доказательства вырабатываются в процессе взаимодействия человека с компьютером (зачастую через IDE). Между собой среды интерактивного доказательства различаются используемым в них языком (обычно функциональным), степенью автоматизации, использованием или отсутствием зависимых типов.

Coq

Рассматриваемый в этой статье фреймворк реализован в Coq. Это среда интерактивного доказательства теорем, использующая Gallina — зависимо-типизированный функциональный язык программирования, позволяющий выражать как программы, так и их свойства. В Coq также реализована автоматизация доказательств через тактики и метапрограммирование с использованием MetaCoq. В индустрии Coq был успешно использован в различных проектах, в том числе:

для проверки безопасности JavaCard;
создания формально верифицированного компилятора CompCert для C;
доказательства теоремы о четырех красках и теоремы Фейта — Томпсона;
верификации смарт-контрактов в проекте Pruvendo и в проектах Formal Land (для нее используют также и ConCert).

Фреймворк ConCert

Архитектура

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

Сначала функции смарт-контракта записываются на языке Gallina. Это обычные функции, которые используют некоторые предопределенные примитивы блокчейна, предоставляемые инфраструктурой ConCert. Затем пишется спецификация и с помощью интеграции QuickChick полуавтоматически тестируются функции контракта по ней. Более того, фреймворк позволяет доказывать свойства смарт-контрактов с помощью инфраструктуры ConCert. Доказательства используют модель среды исполнения для рассуждений о взаимодействующих между собой контрактах. Это позволяет доказывать свойства, выходящие за рамки простой корректности отдельной функции контракта.

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

Несколько советов по установке

ConCert разработан в Coq 8.17 и зависит от MetaCoq и std++. Для работы с тестами необходима библиотека QuickChick. Все зависимости можно установить через opam, менеджера пакетов OCaml:

sudo apt install opam opam switch create . 4.10.2 --repositories default,coq-released=https://coq.inria.fr/opam/released eval $(opam env)

Установка ConCert и его зависимостей:

git clone https://github.com/AU-COBRA/ConCert.git cd ConCert opam install ./coq-concert.opam

Сборка примеров из репозитория:

git clone https://github.com/AU-COBRA/ConCert.git cd ConCert opam install ./coq-concert.opam --with-test

Модель смарт-контракта и среды исполнения

Модель среды исполнения смарт-контрактов облегчает рассуждения о результатах выполнения последовательности вызовов (трассы) смарт-контрактов. Сам смарт-контракт в модели представляется как пара функций: init и receive.

init : Chain -> ContractCallContext -> Setup -> option State

Функция init используется при развертывании контракта для того, чтобы задать его начальное состояние. Первый параметр типа Chain передает данные о блокчейне: количество блоков и отображение из адресов в их балансы. Параметр ContractCallContext передает данные о текущем вызове: адреса вызывающего и вызываемого и сумму, отправленную в контракт. Setup представляет собой параметры инициализации.

receive : Chain -> ContractCallContext -> State -> option Msg -> option (State ∗ list ActionBody)

Функция receive используется для реализации пользовательских вызовов и выполняется при каждом обращении к контракту. State — это текущее состояние контракта. Msg — это определяемый пользователем тип сообщений, которые принимает контракт (его точки входа). Результатом успешного выполнения является новое состояние и список действий, представленный с помощью типа ActionBody. Действия могут быть переводами средств, вызовами других контрактов и развертываниями контрактов.

Тип Chain не содержит достаточно информации, чтобы смоделировать выполнение действий в блокчейне. Нам нужно иметь возможность просматривать информацию о текущих развернутых контрактах, а точнее, об их функциях и состояниях. Для этого вводится тип Environment, описывающий состояние всего окружения:

Record Environment :=
    { env_chain :> Chain;
      env_contracts : Address -> option WeakContract;
      env_contract_states : Address -> option SerializedValue; }.

Состояние окружения изменяется в результате транзакций, которые определяются в ConCert типом Action:

Record Action := { act_from : Address; act_body : ActionBody; }.

Когда receive возвращает новый список действий, среда исполнения должна будет оценить их результат. Эта оценка определяется с помощью отношения ActionEvaluation в Coq с типом Environment -> Action-> Environment -> list Action -> Type. Оно содержит в себе требования для выполнения транзакции в окружении и ее последствия.

И receive, и init являются обычными функциями Coq, что делает их удобными для верификации. Однако просто рассуждения о функциях отдельного контракта зачастую недостаточно, поскольку многие развернутые контракты подразумевают взаимодействие с другими контрактами. Один вызов функции receive потенциально порождает несколько вызовов, а это может создавать сложные графы вызовов между развернутыми контрактами. Поэтому необходимо рассматривать последовательность вызовов выполнения. Трасса выполнения ChainTrace — это рефлексивное, транзитивное замыкание отношения ChainStep, которое, по сути, отражает добавление блока в блокчейн, а в ConCert имеет типChainState -> ChainState -> Type, где:

Record ChainState := { chain_state_env :> Environment;
                       chain_state_queue : list Action; }

Тестирование на основе свойств

Property-based testing — это техника тестирования, в которой данные генерируются псевдослучайным образом и проверяются на соответствие некоторому свойству. В ConCert интегрирована библиотека PBT QuickChick, благодаря этому поддерживается тестирование функциональной корректности контрактов, а также тестирование свойств трасс выполнения. Обзор фреймворка тестирования приведен на рисунке.

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

Рассмотрим пример смарт-контракта токена с типом возможных сообщений:

Inductive Msg :=
    transfer of (address * address * nat)
  | approve of (address * address * nat).

То есть у него есть две точки входа: одна для передачи токенов между двумя заданными адресами и одна для одобрения адреса на расходование заданного количества токенов от имени другого адреса. Генерация псевдослучайных значений Msg тогда сводится к генерации transfer или approve и их параметров с помощью генераторов для address и nat.

Предположим, мы хотим проверить, что transfer корректно обновляет внутренние балансы. В ConCert это свойство функциональной корректности задается с помощью пред- и постусловий. Тестирование такого свойства с помощью QuickChick может выглядеть следующим образом:

QuickChick ({{msg_is_transfer}} Token.receive {{transfer_correct}}).

Выше представлен код теста, в котором мы проверяем, что если входящее сообщение — transfer, то после выполнения функции receive смарт-контракта токена, его состояние должно соответствовать предикату transfer_correct, который мы пишем вручную. По умолчанию QuickChick сгенерирует 10 000 тестов и проверит, что свойство удовлетворяется во всех из них, или сообщит о контрпримере. Полученные контрпримеры автоматически минимизируются фреймворком PBT для более простого понимания. Разработчики утверждают, что эти тесты обычно занимают меньше минуты.

Пример применения для iToken

Разработчики ConCert продемонстрировали уже достаточно большое количество случаев успешного применения фреймворка для тестирования и верификации смарт-контрактов. К примеру, с помощью ConCert были найдены новые уязвимости в смарт-контракте Basic Authentification Token, формализована DAO Attack, смоделирован контракт обменника Dexter на блокчейне Tezos, в ранней версии которого тоже была уязвимость.

Остановимся подробнее на примере уязвимости в Solidity-контракте токена iToken, который использовался на платформе bZx. Уязвимость заключалась в неправильном расположении строк кода и в сентябре 2020 года позволила атакующему украсть 8 млн долларов.

Рассмотрим код с уязвимостью:

Логика смарт-контракта была бы корректной, если переместить строку 6 после строки 8. Рассмотрим случай, когда _from = _to. В этом случае переведенная сумма будет вычтена из баланса отправителя в строке 8. Однако в строке 9 исходный баланс отправителя используется для добавления переданной суммы к балансу отправителя, в результате чего отправитель переводит себе все токены.

Эта уязвимость была также найдена с помощью ConCert. На рисунке мы видим реализацию этой функции во фреймворке.

Рис 4. Реализация функции iToken _internalTransferFrom, содержащей баг — Рис 4. Реализация функции `iToken _internalTransferFrom`, содержащей баг

Эту ошибку можно найти с помощью фреймворка PBT, написав тест, проверяющий, что баланс остается неизменным после перевода самому себе. Однако такая спецификация предполагает, что мы знаем о возможности ошибки в этом случае. Вместо этого можно сформулировать более общее свойство, согласно которому сумма всех балансов должна оставаться неизменной после вызова, за исключением вызовов функций mint и burn. В ConCert такое свойство выглядит следующим образом:

Рис 5. Предикат об инвариантности суммы балансов пользователей iToken

QuickChick ({{msg_is_not_mint_or_burn}} iTokenContract {{sum_balances_unchanged}})

Запустив такой тест, будет получен контрпример, когда свойство не выполняется:

Рис 6. Результаты тестов. Свойство нарушается при вызове transferFrom c одинаковыми параметрами _from и _to — Рис 6. Результаты тестов. Свойство нарушается при вызове `transferFrom` c одинаковыми параметрами `_from и _to`

Моделирование смарт-контракта AMM/DEX и верификация свойств его функций

Мы попробовали применить ConCert для моделирования и верификации смарт-контракта автоматического маркет-мейкера с одного российского хакатона, прошедшего летом 2023 года (см. фронт проекта).

Смарт-контракт написан на Solidity. Пользователи могут создавать пулы ликвидности, вносить в них средства в токенах, зарабатывать комиссионные на внесенных активах и снимать заработанное. Смарт-контракт взимает комиссию за использование протокола.

У контракта пять входных точек: создание пула, внесение средств в пул, вывод средств из пула, вывод заработанных комиссионных, а также обмен:

 Inductive Msg :=
  | createPair : Address -> Address -> N -> bool -> Msg
  | deposit : N -> N -> N -> Msg
  | withdrawFees : N -> Msg 
  | withdraw : N -> Msg
  | swap : N -> Address -> Msg

Рассмотрим исходный код функции создания пула createPair. Создать пул может любой участник сети при условии, что эта пара еще не представлена в DEX.

function createPair(address token0, address token1, uint _fee, bool _isStable) external returns (uint) {
        require(token0 != token1, "two identical addresses");
        require(token0 != address(0), "Zero Address tokenA");
        require(token1 != address(0), "Zero Address tokenB");
        require(getPool[token0][token1][_fee][_isStable] == 0, "Pair already exists");

        PIDs++;
        uint PID = PIDs;

        Pools[PID].token0 = token0;
        Pools[PID].token1 = token1;
        Pools[PID].feeRate = _fee;
        Pools[PID].isStable = _isStable;

        getPool[token0][token1][_fee][_isStable] = PIDs;
        getPool[token1][token0][_fee][_isStable] = PIDs;

        return PID;
    }

Также рассмотрим формализацию этой функции в ConCert:

Рис 7. Реализация функции createPair смарт-контракта sberAMM — Рис 7. Реализация функции `createPair` смарт-контракта sberAMM

Так как мы уже обсудили тестирование смарт-контрактов в ConCert с помощью PBT, подробнее остановимся на доказательстве теорем о корректности рассматриваемого смарт-контракта.

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

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

Рис 8. Предикат корректности и теорема о функции createPair — Рис 8. Предикат корректности и теорема о функции `createPair`

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

function swap(uint PID, address tokenIn, uint amount) external pidExists(PID) PIDstatus(PID) returns (uint) {
        require(tokenIn == Pools[PID].token0 || tokenIn == Pools[PID].token1, "Wrong token address");
        require(IERC20(tokenIn).transferFrom(msg.sender, address(this), amount));

        address tokenOut = _getOtherTokenAddr(PID, tokenIn);
        uint fee = (ud(Pools[PID].feeRate) * ud(amount)).unwrap();
        uint amountMinusFee = amount - fee;
        uint amountOut = _calculateAmounts(PID, tokenIn, amountMinusFee);

        _handleFees(PID, tokenIn, fee);
        IERC20(tokenOut).safeTransfer(msg.sender, uint(amountOut));

        return uint(amountOut);
    }

Ошибка заключается в том, что в функции createPair отсутствует проверка на ограниченность переменной feeRate. Эта переменная хранит значение (по логике контракта — в процентах) комиссии за обмен. Получается, что в седьмой строке функции swap значение переменной amountMinusFee типа uint, равное amount – fee, может стать отрицательным. В рассматриваемом смарт-контракте используется Solidity версии 0.8.19, а значит, в случае такого переполнения произошел бы revert, и транзакция swap не была бы выполнена. То есть функция swap не содержит уязвимости, но отсутствие проверки на значение переменной _fee в функции createPair может привести к тому, что недобросовестный пользователь способен устанавливать неограниченную комиссию за обмен пары, в то время как другие пользователи не смогут создать новый пул этой пары.

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

Заключение

Итак, мы разобрали фреймворк ConCert. Несмотря на то что ConCert не может напрямую проверить корректность исходного кода смарт-контракта, написанного на Solidity, мы убедились, что он хорошо подходит для тестирования и формального доказательства корректности логики контракта. ConCert не является единственным инструментом в этой области, даже на Coq реализовано еще несколько проектов для формальной верификации смарт-контрактов. Если выйти за рамки Coq, то можно найти такие проекты, как Certora (о котором рассказывал мой коллега Сергей), Isabelle/Solidity, Solidity SMTChecker, KEVM и другие.

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

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

По всем вопросам и предложениям можете написать на наш адрес электронной почты: web3@ptsecurity.com.