Найден способ автоматизировать проверку базового протокола облачных вычислений

Важным шагом на пути обеспечения надёжности работы ответственных распределённых инфраструктур стал предложенный командой из Мичиганского университета метод автоматизации так называемой формальной верификации.

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

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

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

Мичиганская команда в своём решении использовала присущее распределённым протоколам свойство регулярности: все серверы, работающие над определенной функцией, обрабатывают примерно одинаковые большие пакеты запросов, и характер их задач со временем меняется очень мало.

Регулярность позволила трансформировать невероятно большую задачу в маленькую и управляемую. Сначала протокол проверяли для фиксированного небольшого количества узлов, а затем полученное решение обобщали на «теоретически неограниченное количество» узлов.

Система проверки моделей IC3PO, разработанная для этого доказательства, контролирует безопасность поведения в каждом состоянии, в которое может войти программа. Если протокол верен, IC3PO менее чем за час выдает индуктивный инвариант – доказательство того, что он верен во всех случаях. Этот индуктивный инвариант, снабженный исчерпывающей документацией, идентичен тому, который ранее получали со значительными затратами человеческих усилий, методом интерактивного доказательства теорем.

В случае обнаружения ошибки в протоколе IC3PO создаст контрпример и трассировку выполнения, демонстрирующую, как проявляется эта ошибка.

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