Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне

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

Протокол консенсуса

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

Существует множество разновидностей протоколов консенсуса, разработанных для удовлетворения различных требований к безопасности, производительности и масштабируемости сети. Наиболее известные из них — Proof of Work (PoW), используемый в Bitcoin, где участники предоставляют вычислительные мощности для решения сложных криптографических задач для подтверждения транзакций, и Proof of Stake (PoS), используемый сейчас в Ethereum (ранее там также использовался PoW), где право создания нового блока выдается участнику с наибольшим количеством нативных токенов. 

Протоколы консенсуса можно разделить на две группы по типу ошибок в сети, к которым они устойчивы. Невизантийские ошибки возникают, когда узлы выходят из строя из-за аппаратных сбоев или сетевых проблем, но не ведут себя злонамеренно. Византийские ошибки, с другой стороны, предполагают наличие вредоносных узлов, которые могут функционировать произвольно или умышленно вредить сети, передавая противоречивую или ложную информацию. Лесли Лэмпорт и Роберт Шостак доказали, что для достижения консенсуса с N византийских узлов распределенная система должна состоять как минимум из 3N + 1 узлов и реализовывать специальный алгоритм консенсуса, устойчивый к византийским ошибкам (Byzantine Fault Tolerant, BFT).

Роль протоколов консенсуса в блокчейнах критически важна для поддержания безопасности и децентрализации сети. Выбор неэффективного протокола консенсуса может привести к сетевым разделениям, при которых разные узлы будут хранить разные цепочки транзакций, или к полной остановке сети. Существует множество примеров атак на протоколы консенсуса. Самая известная из них — атака 51% на консенсусы PoW, позволяющая злоумышленнику с достаточной вычислительной мощностью контролировать сеть и совершать двойные траты. 

Как обезопасить блокчейн от ошибок в консенсусе

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

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

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

TLA+

В этой статье я остановлюсь на методе проверки моделей и буду использовать язык TLA+ вместе с инструментом проверки модели TLC. TLA+ — это язык для написания моделей распределенных систем и параллельных алгоритмов. Он основан на теории множеств, логике первого порядка и темпоральной логике действий (TLA, temporal logic of actions). Программы, написанные на TLA+, не выполняются компьютером как программы на обычном языке программирования: они запускаются через средство проверки моделей. Средство проверки моделей (model checker) — это программа, которая исследует все возможные варианты выполнения системы. Пользователь задает поведение и свойство, а model checker проверяет, выполнены ли они для данной модели или нет. В случае если свойство нарушается, средство предоставит контрпример.

Модель в TLA+ — это набор состояний и переходов между этими состояниями, которые задаются в терминах предикатов и действий. Модель описывает поведение системы как последовательность состояний, удовлетворяющих логическим условиям и изменяющихся в результате действий. Для того чтобы написать модель на TLA+, необходимо задать начальное состояние и систему переходов. Проверить модель на выполнение свойств можно специфицировав эти свойства в виде предикатов и запустив model checker.

С помощью TLA+ было построено и проверено множество моделей различных протоколов консенсуса: Paxos, Raft, Tendermint, HotStuff и другие.

Алгоритм IBFT

Алгоритм Practical Byzantine Fault Tolerant (pBFT) был первым алгоритмом, обеспечивающим достижение консенсуса в частично синхронных сетях с византийскими ошибками, где безопасность не зависит от временных предположений. Эта работа вдохновила множество алгоритмов, улучшающих и дополняющих pBFT, спроектированных в рамках одной и той же частично синхронной модели, где сообщения доставляются в течение ограниченного времени.

Алгоритм IBFT (Istanbul Byzantine Fault Tolerant) также вдохновлен pBFT и был предложен в рамках EIP650 (Ethereum Improvement Proposals). Создание алгоритма было мотивировано тем, что pBFT в оригинальном виде не подходит для использования в блокчейн-сетях. Это связано попросту с тем, что он создавался в далеком 1999 году, за 10 лет до появления первого блокчейна Bitcoin. В pBFT, как видно из его схемы, подразумевается существование некоторого «клиента», который отправляет запросы и ждет результатов. Однако в контексте блокчейна мы можем рассматривать всех валидаторов как «клиентов». Кроме того, чтобы цепочка прогрессировала, в каждом раунде должен постоянно выбираться участник, который будет создавать блок-предложение для консенсуса. Также результат работы оригинального pBFT — это набор операций чтения и записи в файловой системе, а от алгоритма консенсуса в блокчейне мы ожидаем выбор нового блока для добавления в цепочку.

IBFT разработан для использования в блокчейн-сетях с разрешениями (permissioned blockchains), где участники известны и идентифицированы. Он был первоначально представлен как часть платформы Quorum, разработанной компанией JPMorgan Chase. Однако рассматриваемый алгоритм прошел долгий путь через множество доработок перед полноценным внедрением в Quorum.

Первая версия IBFT не всегда работала корректно: два честных узла могли выбрать различные значения. В обновленном варианте эти проблемы были решены, но появились проблемы с живучестью протокола: некоторые выполнения могли привести к взаимному ожиданию и остановке (deadlock). В ответ на эти проблемы было предложено два решения. Первое решение — избавиться от механизма блокировки узлов и добавить алгоритм смены раундов, похожий на тот, что используется в pBFT. Второе решение было представлено как раз в рамках работы над Quorum, и именно об этой версии алгоритма пойдет речь далее.

Моделирование протокола консенсуса IBFT на TLA+

Как я уже отметил, модели протоколов консенсуса удобно строить по псевдокоду алгоритма. Именно такой подход я избрал для IBFT, взяв псевдокод из последней публикации Quorum об этом алгоритме. 

Каждый экземпляр алгоритма проходит по раундам. В каждом раунде один из узлов ведет себя как лидер, чтобы предложить остальным узлам некоторое значение для принятия. Специфицируем функцию выбора лидера на TLA+ следующим образом: Leader == [v \in 0..MaxView |-> v % N], где MaxView — номер последнего раунда, а N — общее число узлов.

Как уже было сказано выше, модель в TLA+ — это набор состояний и переходов между этими состояниями. Состояние программы — это набор значений ее переменных. Для объявления переменных в TLA+ используется ключевое слово VARIABLES.

VARIABLES        messages,       \* множество сообщений, отправленных узлами     RCmessages      \* множество всех сообщений о смене раунда       processState,   \* состояние узлов IBFT     decision        \* дополнительная – хранит принятое значение

В IBFT есть четыре типа сообщений, которые могут отправлять узлы: PRE-PREPARE, PREPARE, COMMIT и ROUND-CHANGE. Первые три имеют вид <message-type, λ, r, value>, где λ — номер экземпляра алгоритма, r — текущий раунд, а value — предлагаемое значение; множество всех таких сообщений будем хранить в переменной messages. Сообщения типа ROUND-CHANGE предназначены для случая смены раунда и имеют вид <ROUND-CHANGE, λ, r, pr, pv>, где, помимо номеров экземпляра и раунда, передаются переменные: pr (prepared round) — номер раунда, в котором узел получил кворум сообщений PREPARE, и pv (prepared value) — величина, полученная в этих сообщениях.

В рассматриваемой статье в алгоритме IBFT есть пять переменных состояния: номер экземпляра, отображения из номера процесса в номере текущего раунда, pr, pv, а также исходное предложенное значение. Стоит упомянуть, что я строил модель отдельного экземпляра алгоритма, поэтому номера экземпляров везде будут опущены.

Опишем формально начальное состояние модели протокола. Все узлы находятся в первом раунде, а лидер отправляет сообщение типа PRE-PREPARE с некоторым предлагаемым значением v.

Init ==    /\ \E v \in Values:     /\ messages = {[type |-> "PRE-PREPARE", view_num |-> 1,                               cmd |-> v, from |-> Leader[1]]}     /\ processState = [p \in Corr |->                         [view_num |-> 1,                          inputValue |-> v,                          pr |-> NilView,                          pv |-> NilValue]]     /\ decision = [p \in Corr |-> NilValue]     /\ RCmessages = {}

Рассмотрим работу алгоритма в «хорошем» случае, когда лидер не византийский и в сети не происходит сбоев. Сначала каждый честный узел p ждет сообщения PRE-PREPARE от лидера и проверяют его на актуальность предлагаемого значения с помощью предиката JustifyPrePrepare. Если такое сообщение получено, честный узел должен отправить по сети сообщение типа PREPARE.

UponPrePrepared(p) ==    /\ \E msg \in messages :      /\ msg.from = Leader[processState[p].view_num]     /\ msg.type = "PRE-PREPARE"     /\ msg.view_num = processState[p].view_num     /\ JustifyPrePrepare (msg)     /\ LET prepare_msg == [type |-> "PREPARE",                             view_num |-> processState[p].view_num,                            cmd |-> msg.cmd, from |-> p]        IN /\ prepare_msg \notin messages           /\ sendMsg({prepare_msg})   /\ UNCHANGED <<processState, decision, RCmessages>>

При получении кворума (2F + 1) сообщений типа PREPARE в текущем раунде r c одинаковым значением v, честный узел обновляет значения pr и pv на r и v и отправляет сообщение типа COMMIT с принимаемым значением.

UponPrepared(p) ==   /\ \E v \in Values:     /\ Cardinality(PrepareMessages(p, v)) >= QUORUM     /\ LET commit_msg == [type |-> "COMMIT",                            view_num |-> processState[p].view_num,                           cmd |-> v, from |-> p]        IN /\ commit_msg \notin messages           /\ processState' = [processState EXCEPT ![p].pr = processState[p].view_num,                                                   ![p].pv = v]           /\ sendMsg({commit_msg})    /\ UNCHANGED <<decision, RCmessages>>

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

UponCommit(p) ==   /\ decision[p] = NilValue   /\ \E v \in Values:     /\ Cardinality(CommitMessages(p, v)) >= QUORUM     /\ decision' = [decision EXCEPT ![p] = v]   /\ UNCHANGED <<processState, messages, RCmessages>>

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

Реализуем этот механизм в нашей модели с помощью двух действий. Действие Timeout может быть выполнено любым узлом и моделирует некорректную работу сети. В этом случае узел переходит в следующий раунд и отправляет сообщение типа ROUND-CHANGE, которое содержит в себе значения pv и pr, а также новый номер раунда. Действие UponQRC отвечает за возврат алгоритма к нормальной работе: лидирующий узел отправляет сообщение типа PRE-PREPARE в случае получения кворума сообщений типа ROUND-CHANGE.

Timeout(p) ==    /\ processState[p].view_num < MaxView   /\ LET rcMsg == [type |-> "ROUND-CHANGE",                     view_num |-> processState[p].view_num + 1,                    pv |-> processState[p].pv, pr |-> processState[p].pr,                     from |-> p]      IN /\ rcMsg \notin RCmessages         /\ sendRC({rcMsg})   /\ processState' = [processState EXCEPT ![p].view_num = processState[p].view_num + 1]   /\ UNCHANGED <<decision, messages>>  RCsMessages(p) == {msg \in RCmessages : /\ msg.type = "ROUND-CHANGE"                                          /\ Leader[msg.view_num] = p}  UponQRC(p) ==   /\ Cardinality(RCsMessages(p)) >= QUORUM   /\ JustifyRoundChange(RCsMessages(p))    /\ LET q == RCsMessages(p)          v == IF HighestPrepared[q][2] /= NilValue                THEN HighestPrepared[q][2]                ELSE processState[p].inputValue          ppMsg == [view_num |-> processState[p].view_num,                     type |-> "PRE-PREPARE",                    cmd |-> v, from |-> p]      IN /\ ppMsg \notin messages         /\ sendMsg({ppMsg})   /\ UNCHANGED <<decision, processState, RCmessages>>

Стоит отметить некоторые важные шаги при моделирования механизма смены раундов. Они связаны с природой выбранного подхода: средство проверки TLC проверяет все возможные состояния модели. В связи с этим нам необходимо ограничивать все константы, в том числе и количество раундов. Также добавлена проверка processState[p].view_num < MaxView, ограничивающая число тайм-аутов и отсутствующая в оригинальном описании алгоритма. Кроме того, необходимо было опустить моделирование времени для избежания проблемы комбинаторного взрыва состояний при проверке модели. В модели я компенсирую это тем, что узел может уйти в тайм-аут в любом состоянии (кроме последнего раунда). 

Предикаты JustifyRoundChange и JustifyPrePrepare реализованы на основе описания протокола и отвечают за проверку безопасности предлагаемого значения при смене раунда и за предотвращение принятия честными узлами значения, предложенного византийским лидером, соответственно.

Так, спецификация системы переходов модели алгоритма выглядит следующим образом.

Steps(p) == IF p \in Corr              THEN \/ UponPrePrepared(p) \/ UponPrepared(p) \/ UponCommit(p)                   \/ Timeout(p) \/ UponQRC(p)             ELSE ByzantineBehavior(p)  Next ==   \/ \E p \in AllProcs: Steps(p)   \/ UNCHANGED <<processState, messages, RCmessages, decision>>

Действие ByzantineBehaviour моделирует поведение византийских узлов: они могут отправлять сообщения любого содержания при любом состоянии алгоритма.

Теперь можно переходить к проверке построенной модели. В целом протокол корректно решает задачу византийского консенсуса при условии наличия 2f + 1 честных участников и f византийских, если он обладает тремя ключевыми свойствами. Именно эти свойства необходимо проверить при формальной верификации BFT-протокола:

1. Согласованность: все корректно работающие узлы принимают одинаковое значение.

2. Корректность: принятое значение было предложено одним из имеющихся узлов.

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

Первые два свойства относятся к классу safety, то есть гарантируют, что система никогда не перейдет в недопустимое состояние. Специфицируем их на TLA+.

Agreement ==   \A p, q \in Corr:     (decision[p] /= NilValue /\ decision[q] /= NilValue) =>      decision[p] = decision[q]  Validity == \A p \in Corr: decision[p] \in ValuesOrNil

Здесь ValuesOrNil — константное множество, которое мы задаем перед проверкой. Оно состоит из возможных принятых значений и NilValue — пустого значения.

Свойство завершаемости, в свою очередь, относится к классу свойств liveness (живучести), гарантирующих, что система рано или поздно достигнет нужного состояния. Такие свойства вычислительно сложнее в проверке, а для их спецификации обычно используются темпоральные операторы. В данном случаем нам необходим темпоральный оператор <> (eventually). 

Done == \A p \in Corr: decision[p] \in Values Termination == <>Done

При проверке свойств такого типа необходимо учитывать, что в TLA+ по умолчанию любое поведение допускает stuttering, то есть выполнение действия, в котором ничего не происходит и переменные не изменяются. Более того, TLA+ допускает бесконечное количество таких переходов. Это позволяет симулировать работу реальных сетей, которые могут остановиться в произвольный момент времени. В связи с этим для проверки свойств живучести нам необходимо добавить условие честности (fairness condition), то есть предположение о том, что система не останавливается:

• Weak fairness означает, что если процесс всегда может прогрессировать, то в конечном итоге он будет прогрессировать. 

• Strong fairness означает, что если процесс всегда может периодически прогрессировать (то есть действия могут выполняться или не выполняться), то в конце концов он добьется прогресса. 

Добавим условие fairness в нашу спецификацию. Weak fairness влечет за собой strong fairness, поэтому добавим это условие. Weak fairness записывается как темпоральная формула WF_vars(Action), где vars — кортеж всех переменных модели.

Spec == Init          /\ [][Next]_vars         /\ \A p \in AllProcs: WF_vars(Steps(p))

Темпоральный оператор [] (always) означает, что Next будет выполняться всегда. Это стандартный вид записи спецификации: мы задали начальное состояние с помощью Init, систему переходов с помощью Next и условие weak fairness для избежания симуляции остановки системы.

Проверяем модель протокола

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

CONSTANT       Corr = {1, 2, 3}      \* множество честных узлов   Byzantine = {0}       \* множество византийских узлов   MaxView = 2           \* число раундов   Values = {"a", "b"}   \* возможные значения

Используем консольную версию TLC 2.19. Как уже было сказано выше, TLC анализирует все возможные состояния модели на выполнение заданных свойств; в отличие от других средств (например, Apalache), мы не можем задать глубину проверки. Если свойство не выполняется, инструмент вернет контрпример — состояние или последовательность состояний (для темпорального свойства), не удовлетворяющую заданному свойству.

В результате проверки модели с максимальным числом раундов, равным 2, получаем успешный результат. Инструменту понадобилось около минуты для полной проверки. 

При увеличении значения MaxView до 3 результат оказался не таким быстрым (проверка проводилась с 10 воркерами):

Model checking completed. No error has been found.
The depth of the complete state graph search is 31.
Finished in 18d 19h

Это означает, что дальнейшее увеличение параметров проверки приведет к разрастанию числа состояний и, как следствие, к длительному времени проверки. В первую очередь это связано с вычислительной сложностью проверки темпорального свойства завершаемости. Проверка только свойств корректности и согласованности при 3, 4 и 5 раундах происходит гораздо быстрее.

Заключение

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

В этой статье я хотел показать актуальность метода проверки моделей для верификации протоколов консенсуса. Ограничения этого метода не являются определяющими для таких алгоритмов: почти всегда мы можем построить модели, совпадающие с псевдокодом алгоритмов и их неформальным описанием. Главной проблемой становится ограниченность и вычислительная сложность такого метода. Однако, как мы можем наблюдать, даже инструмент TLC позволяет добиться результата за разумное время, а более современные инструменты (Apalache, Quint и др.) могут проверять модель еще быстрее. IBFT продолжает длинный список протоколов, верифицированных методом model checking: от ставших классическими Paxos и Raft до относительно новых Ceph и ChonkyBFT.

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