InnoChain: распределенный реестр для индустриального применения с формальной верификацией на всех уровнях реализации

Моделирование и анализ информационных систем. 2020. Т. 27. № 4. С. 454–471.

Кухаренко В. А., Зиборов К. В., Садыков Р. Ф., Наумчев А. В., Резин Р. М., Меркин Л. А.

Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации и формальной верификации. Формальная спецификация и верификация протокола консенсуса необходима, но недостаточна. Необходимо удостовериться, что программная реализация узлов СРР соответствует данному протоколу. Верифицированная программная реализация протокола должна запускаться на достаточно надежной операционной системе. Так называемые “умные контракт”, которые являются важной частью прикладных реализаций конкретных бизнес-процессов на основе СРР, также должны быть верифицируемы.В данной работе мы описываем реализующийся в настоящее время индустриальный проект, результатом которого станет СРР, верифицированная по меньшей мере на четырех описанных выше технологических уровнях. Мы также описываем наш опыт формальной спецификации и верификации протокола HotStuff – отказоустойчивого протокола для гарантированного достижения консенсуса в присутствии византийских процессов и лидера.

Ключевые слова: верификация, блокчейн, проверка моделей, ATLAS, устойчивость к византийским условиям, распределенный консенсус, TLA+