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

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

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

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

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

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

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

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

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

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

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

TLA+

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

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

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

Алгоритм IBFT

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

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

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

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

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

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

Каждый экземпляр алгоритма проходит по раундам. В каждом раунде один из узлов ведет себя как лидер, чтобы предложить остальным узлам некоторое значение для принятия. Специфицируем функцию выбора лидера на 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 ^[15]), мы не можем задать глубину проверки. Если свойство не выполняется, инструмент вернет контрпример — состояние или последовательность состояний (для темпорального свойства), не удовлетворяющую заданному свойству.

В результате проверки модели с максимальным числом раундов, равным 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 ^[15], Quint ^[16] и др.) могут проверять модель еще быстрее. IBFT продолжает длинный список протоколов, верифицированных методом model checking: от ставших классическими Paxos ^[5] и Raft ^[6] до относительно новых Ceph ^[17] и ChonkyBFT ^[18].

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