Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Речь пойдет о верификации смарт-контракта BaseToken в Hyperledger Fabric с помощью метода проверки моделей.
HLF
Hyperledger Fabric (HLF) — одна из самых популярных корпоративных блокчейн-платформ, в которой бизнес-логика реализуется в виде смарт-контрактов, также называемых чейнкодами. Чейнкоды (chaincodes) реализуют на языках общего назначения, таких как Go, JavaScript или Java. Ошибки на уровне чейнкодов, то есть на уровне бизнес-логики, могут привести к огромным финансовым и репутационным потерям. В отличие от Ethereum и Bitcoin, Hyperledger Fabric — permissioned-платформа: к сети допускается ограниченный список контрагентов. Но ошибки в чейнкоде по-прежнему бьют по деньгам и репутации, поэтому факт «это не публичный блокчейн» глобально не спасает от критичных багов.
В своей прошлой статье о формальной верификации смарт-контрактов в Ethereum, я подробно рассказывал о том, что такое методы формальной верификации и почему они важны в контексте блокчейн-безопасности. Вкратце: формальные методы позволяют строго математически доказать корректность программного кода относительно заданных свойств. В контексте блокчейна это значит, что можно заранее обнаружить уязвимости или строго доказать их отсутствие. Актуальность формальной верификации смарт-контрактов в том, что аудит и тестирование смарт-контрактов позволяют обнаружить ошибки, но не гарантируют их отсутствие.
Foundation: фреймворк для chaincode под HLF
Фреймворк Foundation представляет собой Go-библиотеку, которая упрощает разработку чейнкодов под Hyperledger Fabric и используется в российских платформах ЦФА. Foundation обеспечивает готовые примитивы — такие как BaseToken и BaseContract — и единые подходы к маршрутизации вызовов, а также вспомогательные функции, чтобы не писать инфраструктурный код с нуля. Базовый кирпич — BaseContract: он хранит окружение вызова (stub, трейсинг), держит роутер методов и предоставляет стандартные служебные запросы вроде перечня доступных функций, работая как общий слой для любых смарт-контрактов на базе Foundation.
BaseToken строится поверх BaseContract: структура BaseToken встраивает его и добавляет хранение конфигурации токена (эмитент, параметры комиссий, лимиты) в глобальное состояние, а также методы работы с эмиссией и параметрами токена. Вызовы роутятся автоматически по имени метода: все публичные функции с префиксами Tx и Query становятся транзакционными и читающими точками входа, а первый аргумент sender включает проверку прав; reflect-роутер сам разбирает аргументы и вызывает нужный метод без ручного парсинга.
Таким образом, чейнкод BaseToken обеспечивает стандартную функциональность токена на платформе Hyperledger Fabric — хранение балансов участников, операции выпуска токенов, передачи от одного аккаунта другому, установка и сбор комиссий, сжигание токенов и др. Перед нами стояла задача с помощью формальной верификации убедиться, что эта реализация безопасна и не содержит багов.
Формальная верификация чейнкодов
Итак, нашей целью было формально верифицировать чейнкод BaseToken, то есть доказать, что его поведение соответствует набору важнейших требований безопасности и корректности, а также сформулировать эти требования в виде формальной спецификации.
Первое, что необходимо было сделать, — выбрать подход и инструмент для верификации. Мы остановились на методе проверке моделей, который ранее уже использовали для формальной верификации протоколов консенсуса. Такой выбор был сделан, во-первых, по архитектурным причинам. Архитектура HLF сильно отличается от архитектуры публичных блокчейнов, что затрудняет использование существующих фреймворков для моделирования и дедуктивной верификации, разработанных в большинстве своем для Ethereum (например, Concert). Чейнкоды, по сути, являются обычными программами на Golang, однако зрелых инструментов, покрывающих все возможные конструкции языка, для формальной верификации программ на этом языке пока не разработано. Goose и coq-of-go поддерживают лишь подмножества Go, недостаточные для анализа выбранных чейнкодов. Кроме того, метод проверки модели является менее трудозатратным, чем дедуктивная верификация.
Для моделирования и верификации были выбраны TLA+ и Apalache Model Checker соответственно. Модель в TLA+ — это набор состояний и переходов между этими состояниями, которые задаются в терминах предикатов и действий. Модель описывает поведение системы как последовательность состояний, удовлетворяющих логическим условиям и изменяющихся в результате действий. Программы, написанные на TLA+, не выполняются компьютером как программы на обычном языке программирования: они запускаются через средство проверки моделей. Средство проверки моделей, model checker — это программа, которая исследует все возможные варианты выполнения системы. Пользователь задает поведение и свойство, а model checker проверяет, выполнены ли они для данной модели или нет. В случае если свойство нарушается, средство предоставит контрпример.
Для того чтобы написать модель на TLA+, необходимо задать начальное состояние и систему переходов. Проверить модель на выполнение свойств можно специфицировав эти свойства в виде предикатов и запустив model checker.
Построение формальной модели chaincode
Теперь перейдем к построению формальн��й модели поведения BaseToken, абстрагируясь от конкретного кода на Go, при этом вручную транслируя ключевую логику.
Стандартно чейнкод HLF должен реализовывать интерфейс, состоящий из методов Init и Invoke:
type Chaincode interface { // Init is called during Instantiate transaction Init(stub ChaincodeStubInterface) pb.Response // Invoke is called to update or query the ledger Invoke(stub ChaincodeStubInterface) pb.Response }
BaseToken напрямую Init/Invoke не объявляет: он встраивает core.BaseContract и реализует core.BaseContractInterface. Эта реализация передается в core.NewCC, а вызовы Init/Invoke проходят через структуру Chaincode, на которой реализованы Init и Invoke. Она создается через core.NewCC, настраивает роутер на методы контракта и содержит поле contract с типом BaseContractInterface.
Рассмотрим основные аспекты моделирования.
Модель состояния: мы определили переменные состояния, отражающие ключевые элементы ledger Fabric. В случае токена это прежде всего балансы аккаунтов и связанные параметры (общий выпуск токенов, обменные курсы, лимиты и комиссии).
VARIABLES \* @type: Str -> Int; tokenBalances, \* @type: <<Str, Str>> -> Int; allowedBalances, \* [address: Address, currency: Currency] -> Nat \* @type: Int; totalEmission, \* @type: <<Str, Str>> -> Int; rates, \* [dealType: String, currency: Currency] -> Rate \* @type: <<Str, Str>> -> $limit; limits, \* [dealType: String, currency: Currency] -> [min: Nat, max: Nat] \* @type: $feeRecord; fee, \* [currency: String, rate: Nat, floor: Nat, cap: Nat] \* @type: Str; feeAddress
Начальное состояние моделирует вызов Init, то есть инициализирует переменные. Предполагаем, что в начальном состоянии все балансы токена нулевые, а балансы в фиатных валютах равны 1000.
Init == /\ tokenBalances = [a \in Addresses |-> 0] /\ allowedBalances = [ac \in Addresses \X Currencies |-> IF ac[1] # Issuer /\ ac[1] # FeeAddress THEN 1000 ELSE 0] /\ totalEmission = 0 /\ rates = [dc \in DealTypes \X Currencies |-> 0] /\ limits = [dc \in DealTypes \X Currencies |-> [min |-> 0, max |-> 0]] /\ fee = [currency |-> "TOKEN", rate |-> 0, floor |-> 0, cap |-> 0] /\ feeAddress = FeeAddress
Учет прав и ролей: в модели введены роли пользователей согласно исходной логике BaseToken. Issuer владеет эмиссией и тарифами и имеет уникальные права для вызова функций TxSetRate, TxSetLimits, TxDeleteRate, TxBuyToken/TxBuyBack. Fee_setter — может вызывать TxSetFee, то есть устанавливать комиссию за операции. Fee_address_setter — может вызывать TxSetFeeAddress, устанавливая адрес получения комиссий. В ядре Foundation реализована матрица доступа и обозначены роли acl.Issuer, acl.FeeSetter, позволяющие спрашивать ACL про права (GetAccountRight, IsIssuerAccountRight), но BaseToken сейчас их не использует: управление доступом реализовано через статические адреса в конфигурации и проверки sender.Equal.
Абстракции Hyperledger Fabric: сама среда Hyperledger Fabric (механизм транзакций, порядок выполнения, подтверждения) была опущена в рамках верификации. Мы предполагаем последовательное выполнение транзакций (то есть полагаемся на корректную работу Orderer Service, отвечающего за их упорядочение) и фокусируемся непосредственно на бизнес-логике чейнкода.
Модель транзакций: основные методы рассматриваемого чейнкода TxTransfer, TxBuyToken, TxBuyBack, EmissionAdd, EmissionSub, TxSetRate, TxSetLimits, TxDeleteRate, TxSetFee, TxSetFeeAddress были выражены как переходы между состояниями. Каждый переход имеет предусловия и эффект на состояние. Мы тщательно заложили эти правила согласно оригинальной реализации BaseToken, предварительно проведя ручной аудит ее логики. Для наглядности рассмотрим пример модели функции TxBuyToken, чтобы понять, как реальный код отображается в проверяемую модель. TxBuyToken предназначена для покупки токена за фиатную валюту (allowed currency): в ней проверяется, что покупатель не является эмитентом, а также проверяются лимиты; в случае успешных проверок происходит обмен по текущему курсу из состояния.
func (bt *BaseToken) TxBuyToken(sender *types.Sender, amount *big.Int, currency string) error { if sender.Equal(bt.Issuer()) { return errors.New("impossible operation") } if amount.Cmp(big.NewInt(0)) == 0 { return errors.New(ErrAmountEqualZero) } price, err := bt.CheckLimitsAndPrice("buyToken", amount, currency) if err != nil { return err } if err = bt.AllowedBalanceTransfer(currency, sender.Address(), bt.Issuer(), price, "buyToken"); err != nil { return err } return bt.TokenBalanceTransfer(bt.Issuer(), sender.Address(), amount, "buyToken") }
BuyToken(buyer, amount, currency) == /\ buyer # Issuer /\ amount > 0 /\ rates[<<"buyToken", currency>>] > 0 /\ InLimits(amount, "buyToken", currency) /\ amount <= tokenBalances[Issuer] /\ LET price == CalcPrice(amount, "buyToken", currency) IN /\ price <= allowedBalances[<<buyer, currency>>] /\ tokenBalances' = [tokenBalances EXCEPT ![Issuer] = @ - amount, ![buyer] = @ + amount] /\ allowedBalances' = [allowedBalances EXCEPT ![<<buyer, currency>>] = @ - price, ![<<Issuer, currency>>] = @ + price] /\ UNCHANGED <<totalEmission, rates, limits, fee, feeAddress>>
Спецификация свойств для проверки
Определим ключевые свойства, которым должен удовлетворять токен. Мы приведем лишь несколько примеров спецификации проверяемых свойств, полную формальную спецификацию BaseToken на TLA+ можно найти в нашем репозитории.
Сохранение баланса: общий суммарный баланс во всей системе остается консистентным. Сумма всех токен-балансов равна общей эмиссии, то есть токены не создаются и не уничтожаются никак, кроме операций EmissionAdd и EmissionSub.
Рассмотрим пример спецификации этого свойства на TLA+.
AddBalance(sum, addr) == sum + tokenBalances[addr] TotalTokenBalance == ApaFoldSet(AddBalance, 0, Addresses) TotalBalanceEqualsEmission == TotalTokenBalance = totalEmission
Оператор ApaFoldSet(Op, b, C) работает как свертка (fold) по множеству: он берет начальное значение аккумулятора b и последовательно применяет бинарный оператор (в нашем случае — сложение) ко всем элементам множества C в некотором порядке. Если множество непусто, то результат определяется рекурсией вида ApaFoldSet(Op, b, C) = ApaFoldSet(Op, Op(b, x), C \ {x}) для некоторого элемента x ∈ C.
Отсутствие негативных балансов: ни у одного аккаунта не может быть отрицательного баланса токенов в результате каких бы то ни было последовательностей операций. Эмиссия, обменные курсы, комиссии и лимиты также не должны быть отрицательны ни в каком состоянии системы.
BalancesNonNegative == /\ \A a \in Addresses: tokenBalances[a] >= 0 /\ \A a \in Addresses, c \in Currencies: allowedBalances[<<a, c>>] >= 0
Только эмитент может изменять эмиссию. Если эмиссия изменилась то разница ушла (пришла) на баланс Issuer; никто другой не может «создать» себе токены.
EmissionAuthorization == totalEmission' # totalEmission => tokenBalances'[Issuer] - tokenBalances[Issuer] = totalEmission' - totalEmission
��орректность переводов и операций покупки: токены могут пересылаться между счетами только при выполнении необходимых условий (например, у отправителя достаточно средств и после транзакции балансы обновляются корректно).
BuyConsistency == \A a \in Addresses, c \in Currencies: (a # Issuer /\ allowedBalances'[<<a, c>>] < allowedBalances[<<a, c>>] /\ tokenBalances'[a] > tokenBalances[a]) => /\ InLimits(tokenBalances'[a] - tokenBalances[a], "buyToken", c) /\ rates[<<"buyToken", c>>] > 0 /\ allowedBalances[<<a, c>>] - allowedBalances'[<<a, c>>] = (tokenBalances'[a] - tokenBalances[a]) * rates[<<"buyToken", c>>]
Обратите внимание на переменные со штрихом. Инварианты, содержащие такие переменные, называются инвариантами действий (action invariants) и проверяются model checker не в каждом состоянии, а на любой паре соседних состояний. То есть в паре (s, s’), s’ это значение переменной s в следующем состоянии. В нашем случае это удобно для проверки корректности операций вроде Transfer: нам важно связать старое и новое состояния, а не просто смотреть на снапшоты. Возможность проверки таких свойств является преимуществом инструмента Apalache перед более классическим TLC Model Checker.
Перед началом model checking нам необходимо задать значения всех констант. Чтобы избежать комбинаторного взрыва числа состояний, будем проверять модель не более чем с пятью адресами и двумя фиатными валютами. Ограничение области проверки помогает сделать проверку модели выполнимым за разумное время, не жертвуя при этом проверкой важных случаев.
После этапа спецификации свойств и ограничения констант можем перейти к их проверке на модели.
Запуск проверки и результаты верификации
Как уже было сказано выше, в качестве инструмента проверки построенной TLA+-модели BaseToken был выбран Apalache. Apalache — это bounded model checker, то есть инструмент, проверяющий конечное число переходов модели, стартуя из начального состояния. При проверке мы должны явно указывать, какое число переходов мы хотим проверить. Среди преимуществ Apalache стоит отметить проверку инвариантов действий (actions invariants) и трасс (trace invariants), а также встроенный type checker для TLA+, который упрощает написание корректных моделей. Другим подходящим инструментом является TLC, который проверяет все возможные состояния модели. Очевидно, что наша модель будет иметь неограниченное число состояний (например, при нулевой комиссии пользователи могут бесконечно отправлять токены друг другу). Мы могли бы использовать TLC в режиме симуляции или добавить счетчик числа переходов в модели, наложив на него ограничение сверху, однако предпочли использовать Apalache из-за более подходящей в данном случае функциональности.
После подготовки модели и свойств мы запустили проверку с помощью Apalache. Инструмент автоматически перебрал всевозможные последовательности операций (в рамках заданных ограничений) и проверил, что ни одно из сформулированных свойств не нарушается. Мы проверяли модель с числом шагов до k=7, а также в режиме симуляции на 10 000 трасс и k=20 переходах. Отдельно отметим, что fold по множествам в свойстве TotalBalanceEqualsEmission заметно влияет на производительность: каждое такое выражение разворачивается в нетривиальные ограничения над всеми элементами множества, поэтому размер множества участников напрямую отражается на времени проверки. Остальные инварианты проверяются гораздо быстрее.
В результате ни одна из проверок не выявила нарушений: модель BaseToken удовлетворяет всем заданным инвариантам. Это означает, что в рамках построенной модели, охватывающей проверенные сценарии и допущения, поведение смарт-контракта согласуется с заданными свойствами: токены не пропадают и не появляются из воздуха, права доступа соблюдаются, недопустимые действия предотвращаются.
Отсутствие контрпримеров — важный результат: в рамках построенной модели BaseToken удовлетворяет заявленным свойствам, что существенно снижает риск ошибок в бизнес-логике токена. При этом важно понимать границы таких гарантий. Мы проверяли внутреннюю логику чейнкода при ряде архитектурных допущений: что сама платформа Hyperledger Fabric корректно исполняет транзакции, что окружение и ACL возвращают ожидаемые разрешения и что модель абстрагирует детали, не влияющие на проверяемые инварианты. Кроме того, проверка выполнялась на ограниченных параметрах и длинах сценариев. Тем не менее даже в этих рамках инструмент перебрал тысячи достижимых переходов, включая пограничные случаи, и не нашел нарушений: это хороший сигнал для разработчиков, но не гарантия безошибочности для всего стека и любых условий эксплуатации.
Заключение
Методы формальной верификации, в частности проверка модели, доказали свою ценность на практике: они позволяют обнаруживать и предотвращать ошибки до развертывания кода в продакшен. В нашем случае проверка чейнкода BaseToken не выявила логических уязвимостей, что повышает уверенность в корректности реализации. Но не менее важно то, что сам процесс верификации усиливает культуру разработки — заставляет явно формулировать требования, понимать границы системы и думать о граничных случаях.
Наш проект принес несколько ценных инсайтов и результатов для сообщества Hyperledger Fabric:
Демонстрация возможностей формальных методов для Hyperledger Fabric. Мы показали, что техники модельной проверки успешно применимы не только к смарт-контрактам EVM-сетей, но и к чейнкодам на Hyperledger Fabric. Это расширяет арсенал средств обеспечения качества для корпоративных блокчейн-разработок.
Повышение доверия к BaseToken. Формальная верификация существенно повышает уверенность в безопасности и корректности BaseToken.
Для нас этот кейс стал хорошей проверкой: формальные методы здесь не остались на уровне теории, а превратились в рабочий инструмент для реального чейнкода в реальной экосистеме. Мы намерены продолжить исследования в этой области и применять формальные методы к другим чейнкодам и инфраструктурным компонентам Hyperledger Fabric.
Спасибо за внимание! Если у вас остались вопросы или идеи, будем рады обсудить их в комментариях.
