Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем 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, разработанной компанией J.P. Morgan. Однако рассматриваемый алгоритм прошел долгий путь через множество доработок перед полноценным внедрением в 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-протокола:
Согласованность: все корректно работающие узлы принимают одинаковое значение.
Корректность: принятое значение было предложено одним из имеющихся узлов.
Завершаемость: все корректно работающие узлы в конце концов достигают определенного значения.
Первые два свойства относятся к классу 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 активно изучает и применяет методы формальной верификации в блокчейнах, мы понимаем их значимость и эффективность. Мы также активно исследуем и внедряем другие инструменты и методики, которые позволяют повысить качество и безопасность разрабатываемых программ. Они включают в себя как новейшие разработки в области формальной верификации, так и проверенные временем методики — статический анализ, тестирование и фаззинг.