Untersuchung der AWS-Ausfall-Race-Condition mit Spin-Checker

Reproduzierung der AWS-Ausfall-Race-Condition mit Spin-Checker

Der jüngste Ausfall bei Amazon Web Services (AWS) zog eine detaillierte Analyse nach sich, die unter anderem auf eine Race Condition hinwies, die das DynamoDB-System betraf. Diese Race Condition stellt eine Herausforderung dar, da sie selten und schwer reproduzierbar ist. Eine Methode zur Untersuchung solcher Probleme ist die Modellprüfung, die es ermöglicht, systematische Prozesse zu analysieren und Fehler zu simulieren. In diesem Artikel betrachten wir, wie mithilfe des Spin-Modellprüfers eine solche Race Condition untersucht werden kann.

Die Kontexte des Ausfalls

Laut dem AWS-Post-Mortem-Bericht betraf die Race Condition das automatisierte DNS-Verwaltungssystem von DynamoDB. Dieses System besteht aus einem DNS Planer und mehreren DNS Enactors, die unabhängig voneinander in verschiedenen Verfügbarkeitszonen arbeiten. Der kritische Punkt ist das Gleichgewicht zwischen dem Anwenden neuer DNS-Pläne und dem Bereinigen älterer, was durch ungleichzeitige Prozesse schnell kompliziert werden kann.

Modellierung mit SPIN

Um dieses Phänomen zu untersuchen, wurde ein experimentelles Setup mit dem Spin-Modellprüfer erstellt, der die Promela-Sprache nutzt. Ziel war es, das Problem zu simulieren und verschiedene Szenarien zu testen, um zu verstehen, wie die Race Condition entsteht.

Im Wesentlichen funktioniert der DNS Enactor so, dass er die neuesten DNS-Pläne aufnimmt und diese nach einer Überprüfung auf Neuheit gegenüber dem zuletzt angewendeten Plan implementiert. Diese Überprüfung ist für die Vermeidung von Inkonsistenzen entscheidend. Gibt es jedoch eine Asynchronität innerhalb der Enactor-Prozesse, kann es dazu kommen, dass ein älterer Plan fälschlicherweise erneut aktiv wird, während ein anderer gerade die Bereinigung durchführt. Die Folge ist potenziell der Verlust wichtiger DNS-Einträge.

Ergebnis der Modellprüfung

Der Spin-Modellprüfer erstellt Prozesse, die von einem Anfangszustand ausgehen und jede mögliche Statusänderung analysieren. Dies erlaubt das Erkennen sämtlicher Interleavings der DNS-Enactor-Prozesse und deren Auswirkungen auf den Systemzustand. Die Untersuchung ergab, dass die Race Condition dadurch auftreten konnte, dass zwei Enactors in nicht synchronisierten Zeitpunkten Pläne anwendeten und bereinigten, was zu einem Datenverlust führte.

Invarianzprüfung

Ein zentraler Bestandteil dieser Modellprüfung war die Festlegung eines Invarianten: Der DNS-Eintrag sollte niemals gelöscht werden, wenn ein neuerer Plan bereits angewendet wurde. Diese Regel wurde formal mit linearer temporaler Logik (LTL) ausgedrückt, um die kontinuierliche Konsistenz des Systems zu gewährleisten.

Diese Modellprüfung zeigt, dass auch bei komplexen Systemen wie AWS grundsätzlich analysierbare Schwachstellen vorhanden sein können. Sie zeigt auch den Wert von formalen Methoden in der Softwarearchitektur, um solch subtile Fehler frühzeitig zu entdecken.

Insgesamt zeigt das Experiment mit dem Spin-Modellprüfer, dass formale Verifikationen, obwohl sie keine hundertprozentige Sicherheitsgarantie bieten können, entscheidend dazu beitragen, die Zuverlässigkeit von verteilten Systemen zu erhöhen.