English
Формальная верификация и устойчивость к цензуре протоколов византийского консенсуса на примере IBFT
Зиборов К. В., Бондарев Н. С., Янович Ю. А.
Получена: 21.01.2026 Принята: 19.03.2026
Опубликована: 2026 год, том 30, выпуск 1, С. 58–86
Аннотация
В работе выполнен формальный анализ семейства протоколов Istanbul BFT (IBFT), объединяющий уязвимую первую версию, исправленные промежуточные варианты и модификацию, обеспечивающую устойчивость к цензуре, в рамках единого подхода к верификации. На основе спецификаций TLA+ с помощью средства проверки моделей TLC (i) строятся контрпримеры, демонстрирующие нарушение согласованности в первой версии IBFT, (ii) подтверждаются свойства безопасности и живучести для исправленного варианта QBFT, и (iii) вводится строгая формализация устойчивости к цензуре для византийских протоколов с лидером как ограниченной гарантии качества цепочки, для которой стандартная ротация лидера может давать нарушение. В работе также предлагается и формально верифицируется правило выбора лидера f-skip, обеспечивающее устойчивость к цензуре без ослабления исходных гарантий безопасности и живучести.
Ключевые слова: IBFT, QBFT, BFT-консенсус, формальная верификация, TLA+, TLC, устойчивость к цензуре.
BibTeX
@article{IS-Ziborov-Bondarev-Yanovich2026,
author = {Зиборов, Кирилл Викторович and Бондарев, Никита Сергеевич and Янович, Юрий Александрович},
title = {{Формальная верификация и устойчивость к цензуре протоколов византийского консенсуса на примере IBFT}},
journal = {Интеллектуальные системы. Теория и приложения},
year = {2026},
volume = {30},
number = {1},
pages = {58--86},
}
AMSBIB
\RBibitem{IS-Ziborov-Bondarev-Yanovich2026}
\by К.\,В.~Зиборов, Н.\,С.~Бондарев, Ю.\,А.~Янович
\paper Формальная верификация и устойчивость к цензуре протоколов византийского консенсуса на примере IBFT
\jour Интеллектуальные системы. Теория и приложения
\yr 2026
\vol 30
\issue 1
\pages 58--86