Reproducing the AWS Outage Race Condition with a Model Checker

AWS опубликовал отчет о недавнем сбое, связанном с race condition в системе управления DNS. Автор статьи воспроизвел упрощенную версию проблемы с помощью верификатора моделей Spin и языка Promela. В системе участвуют DNS Planner (создает планы) и три независимых DNS Enactor (применяют планы в разных зонах доступности). Race condition возникает, когда один Enactor применяет новый план и начинает очистку старых, в то время как другой, отставший, все еще обрабатывает более старый план. Когда первый Enactor завершает очистку, он удаляет этот "старый" план, который на самом деле еще активен, что приводит к исчезновению DNS-записей.

Используя Spin, автор смоделировал Planner и два параллельных Enactor. Каждый Enactor проверяет свежесть плана перед применением и отслеживает высший примененный план. Во время очистки он удаляет только значительно более старые версии, но если удаляемый план совпадает с текущим активным, это сбрасывает флаг dns_valid в false. Spin систематически проверял все возможные состояния системы и обнаружил последовательность действий, приводящую к race condition, подтвердив уязвимость.

Комментарии (37)

Пользователи обсуждают, что формальные методы (TLA+, Alloy и т.д.) могли бы предотвратить инцидент, если бы инвариант «не удалять активный план» был бы формализован и проверялся непрерывно.
Обсуждается, что реальные системы часто отклоняются от «чистой» модели из-за компромиссов с производительностью и стоимостью хранения логов и т.д.
Участники спора сходятся в том, что даже если бы формальные методы были бы применены, они бы не предотвратили бы ошибку, если бы не было процесса, который бы гарантировал, что модель и код синхронизированы.
Некоторые комментаторы подчеркивают, что даже самые продвинутые инструменты не могут предотвратить ошибки, если нет культуры их использования и процессов, которые бы обеспечивали бы, что модель всегда актуальна.
В конце концов, большинство соглашается, что самым важным является не наличие формальных методов, а культура их использования и процессов, которые бы гарантировали бы, что модель всегда отражает код.