Praktiken zur Systemkorrektheit bei Amazon Web Services

• AWS betrachtet Systemkorrektheit als zentrale Grundlage, um Sicherheit, Dauerhaftigkeit, Integrität und Verfügbarkeit zu gewährleisten, und hat den Einsatzbereich von TLA+ ausgehend auf Model Checking, Fuzzing, eigenschaftsbasiertes Testen, Laufzeitverifikation und formale Beweise ausgeweitet
• TLA+ beseitigte früh Fehler, die mit klassischen Tests schwer zu finden sind, und gab Vertrauen in Performance-Optimierungen; um die Zugänglichkeit für Entwickler zu erhöhen, wurden jedoch zusätzlich Werkzeuge wie die Programmiersprache P und PObserve eingeführt
• Das eigenschaftsbasierte Testen von S3 ShardStore, deterministische Simulationen und SQL-Fuzzing bei Aurora Limitless Database sind Beispiele dafür, wie formale Techniken näher an alltägliche Entwicklungs- und Integrationstests herangeführt wurden
• Fault Injection Service injiziert Ausfälle wie API-Fehler, I/O-Pausen und Instanzfehler, um Resilienzmechanismen zu überprüfen; Amazon.com führte im Vorfeld des Prime Day 2024 733 FIS-basierte Experimente aus
• In Bereichen, in denen Sicherheitsgrenzen und Performance-Optimierungen entscheidend sind, etwa bei Cedar, Firecracker und der RSA-Optimierung für Graviton 2, werden formale Beweise eingesetzt; die steile Lernkurve und die Zugänglichkeit der Tools bleiben jedoch weiterhin Hürden für die Einführung

---

Wie AWS Systemkorrektheit behandelt

• Um Services bereitzustellen, denen Kunden vertrauen können, muss AWS hohe Standards bei Sicherheit, Dauerhaftigkeit, Integrität und Verfügbarkeit einhalten; Systemkorrektheit stützt diese Ziele
• Der CACM-Artikel „How Amazon Web Services Uses Formal Methods“ aus dem Jahr 2015 stellte den Ansatz vor, mit dem AWS die Korrektheit zentraler Services absichert; seitdem sind diese Services bei AWS-Kunden weit verbreitet
• Das anfängliche zentrale Werkzeug war die von Leslie Lamport entwickelte formale Spezifikationssprache TLA+
  • Sie hilft dabei, subtile Fehler, die klassische Tests übersehen können, früh in der Entwicklung zu entdecken und zu beseitigen
  • Sie gibt die Gewissheit, aggressive Performance-Optimierungen umzusetzen, ohne die Systemkorrektheit zu gefährden
• Vor 15 Jahren stützten sich die Testpraktiken bei AWS vor allem auf Unit-Tests zur Build-Zeit und begrenzte Integrationstests zur Deployment-Zeit
• Seitdem hat AWS formale und semi-formale Techniken in den Entwicklungsprozess integriert
  • Theorembeweise, deduktive Verifikation, Model Checking
  • eigenschaftsbasiertes Testen, Fuzzing, Laufzeit-Monitoring

Die Programmiersprache P und PObserve

• Als AWS Anfang der 2010er-Jahre formale Techniken über die ersten Teams hinaus ausweitete, zeigte sich, dass viele Engineers Schwierigkeiten hatten, TLA+ zu lernen und produktiv einzusetzen
• Die Stärke von TLA+ liegt darin, eine mathematisch geprägte, hochabstrakte Sprache zu sein; für Entwickler, die an imperative Sprachen gewöhnt sind, entsteht dadurch jedoch eine Einstiegshürde
• Die zustandsmaschinenbasierte Sprache P für Modellierung und Analyse verteilter Systeme überbrückt diese Lücke
  • Entwickler modellieren das Systemdesign als kommunizierende Zustandsmaschinen
  • Dieses mentale Modell ist Amazon-Entwicklern vertraut, die viel mit Microservices und serviceorientierter Architektur (SOA) arbeiten
  • P wird seit 2019 bei AWS entwickelt und als strategisches Open-Source-Projekt gepflegt
• Mehrere führende AWS-Produktteams nutzen P, um die Korrektheit von Systemdesigns zu prüfen
  • Storage: Amazon S3, EBS
  • Datenbanken: Amazon DynamoDB, MemoryDB, Aurora
  • Compute: EC2, IoT
• S3 nutzte P beim Übergang von eventual consistency zu strong read-after-write consistency
  • Das S3-Index-Subsystem ist ein Speicher für Objektmetadaten, der schnelle Datenabfragen ermöglicht
  • Um starke Konsistenz zu erreichen, waren mehrere nichttriviale Änderungen am S3-Index-Protokollstack erforderlich
  • P ermöglichte es, das Protokolldesign formal zu modellieren und zu verifizieren, Designfehler früh zu beseitigen und riskante Optimierungen per Model Checking abzusichern
• 2023 baute das AWS-P-Team PObserve
  • Es verwendet strukturierte Logs aus der Ausführung verteilter Systeme
  • Es prüft nachträglich, ob die Logs mit dem Verhalten übereinstimmen, das die formale P-Spezifikation des Systems erlaubt
  • Es verkleinert die Lücke zwischen Produktionsimplementierungen in Sprachen wie Rust oder Java und der P-Spezifikation zur Designzeit
  • Es verbindet Verifikation zur Designzeit mit Laufzeit-Monitoring der Implementierung und erhöht so den Wert der Investition in formale Spezifikationen

Wie leichtgewichtige formale Techniken in den Entwicklungsfluss integriert werden

• AWS führt leichtgewichtige formale Techniken ein, um formale Methoden näher an die Entwicklungs- und Testabläufe der Engineering-Teams zu bringen

• Eigenschaftsbasiertes Testen

  • ShardStore von Amazon S3 nutzt eigenschaftsbasiertes Testen, um über den gesamten Entwicklungszyklus hinweg Korrektheitstests und höhere Entwicklungsgeschwindigkeit zu unterstützen
  • Mehrere Techniken werden kombiniert, damit Menschen erwartetes Verhalten spezifizieren und automatisierte Tests mehr Eingaben und Fehlerbedingungen erkunden können
    • vom Entwickler bereitgestellte Korrektheitsspezifikationen
    • Coverage-guided Fuzzing, das Eingabeverteilungen anhand von Code-Coverage-Metriken steuert
    • Fehlerinjektion, die Hardware- und andere Systemausfälle während Tests simuliert
    • Minimierung, die Gegenbeispiele automatisch verkleinert, damit Menschen sie leichter debuggen können

• Deterministische Simulation

  • Deterministische Simulationstests führen ein verteiltes System in einem Single-Thread-Simulator aus und kontrollieren alle Quellen von Zufälligkeit
    • Thread-Scheduling
    • Timing
    • Reihenfolge der Nachrichtenübermittlung
  • Entwickler können bestimmte Fehler- und Erfolgsszenarien schreiben, etwa Situationen, in denen Beteiligte in bestimmten Phasen eines verteilten Protokolls ausfallen
  • Da das Test-Framework Nichtdeterminismus kontrolliert, können interessante Ausführungsreihenfolgen vorgegeben werden, etwa eine Reihenfolge, die früher einen Bug ausgelöst hat
  • Der Scheduler kann um Reihenfolge-Fuzzing oder die Erkundung aller möglichen Reihenfolgen erweitert werden
  • Dadurch werden Tests von Systemeigenschaften bei Latenz- und Fehlersituationen näher an die Build-Zeit herangerückt als bei Integrationstests; das beschleunigt die Entwicklung und erweitert die Verhaltensabdeckung
  • Teile der AWS-Arbeit zu Build-Zeit-Tests von Thread-Reihenfolgen und Systemfehlern wurden als die Projekte shuttle und turmoil als Open Source veröffentlicht

• Kontinuierliches Fuzzing und zufällige Testeingabegenerierung

  • Kontinuierliches Fuzzing, insbesondere skalierbare, Coverage-guided Testeingabegenerierung, ist wirksam für Systemkorrektheitstests zur Integrationszeit
  • Bei der Entwicklung von Aurora Limitless Database, der Daten-Sharding-Funktion von Amazon Aurora, wurde Fuzzing umfassend eingesetzt, um zwei zentrale Eigenschaften zu verifizieren
  • SQL-Abfragen und ganze Transaktionen werden gefuzzt, um zu verifizieren, dass die logische Aufteilung der SQL-Ausführung über Shards hinweg korrekt ist
  • Große Mengen zufälliger SQL-Schemata, Datensätze und Abfragen werden synthetisiert, auf der zu testenden Engine ausgeführt und mit den Ergebnissen eines Orakels auf Basis einer nicht geshardeten Engine verglichen
  • Auch andere Verifikationsansätze, etwa von SQLancer geprägte Methoden, werden zusätzlich eingesetzt
  • Die Kombination aus Fuzzing und Fehlerinjektionstests ist auch für Korrektheitsaspekte von Datenbanken wie Atomarität, Konsistenz und Isolation nützlich
    • Transaktionen werden automatisch erzeugt
    • formal spezifizierte Korrektheitsorakel definieren das korrekte Verhalten
    • mögliche Interleavings von Transaktionen und Anweisungen innerhalb von Transaktionen werden auf dem zu testenden System ausgeführt
    • Eigenschaften wie Isolation werden nachträglich mit Ansätzen wie Elle verifiziert

Fault Injection Service und Verifikation von Fehlersituationen

• AWS brachte Anfang 2021 den Fault Injection Service (FIS) auf den Markt, um fehlerinjektionsbasierte Tests für eine Vielzahl von AWS-Kunden verfügbar zu machen
• FIS kann simulierte Ausfälle in Test- oder Produktions-Deployments auf AWS-Infrastruktur injizieren
  • API-Fehler
  • I/O-Pausen
  • ausgefallene Instanzen
• Fehlerinjektion ermöglicht zu überprüfen, ob in der Architektur eingebaute Resilienzmechanismen die Verfügbarkeit tatsächlich verbessern und keine neuen Korrektheitsprobleme erzeugen
  • Failover
  • Health Checks
• FIS-basierte Fehlerinjektionstests werden von AWS-Kunden und intern bei Amazon breit genutzt
• Amazon.com führte im Vorfeld des Prime Day 2024 733 FIS-basierte Fehlerinjektions-Experimente aus
• 2014 analysierten Yuan et al., dass 92 % der katastrophalen Ausfälle in den getesteten verteilten Systemen durch fehlerhafte Behandlung nichtkatastrophaler Fehler ausgelöst wurden
• Katastrophale Ausfälle auf dem Normalpfad sind selten, weil der Normalpfad häufig ausgeführt, besser getestet und deutlich einfacher ist als Fehlerpfade
• Fehlerinjektionstests und FIS erleichtern es, Systemverhalten bei Störungen und Ausfällen zu testen, und verringern so die Lücke in der Bug-Dichte zwischen Normal- und Fehlerpfaden
• Fehlerinjektion selbst gilt zwar nicht als formale Technik, kann aber mit formalen Spezifikationen kombiniert werden
  • Erwartetes Verhalten wird als formale Spezifikation definiert
  • Während und nach der Fehlerinjektion werden Ergebnisse mit dem spezifizierten Verhalten verglichen
  • So lassen sich mehr Bugs finden, als wenn man nur Metriken und Logfehler prüft oder Menschen visuell urteilen lässt

Metastabilität und emergentes Systemverhalten

• In den vergangenen zehn Jahren ist das Interesse an einer bestimmten Klasse von Systemausfällen gewachsen: metastabilen Fehlern (metastable failures)
• Metastabile Fehler sind Ausfälle, bei denen ein Trigger wie Überlast oder Cache-Leerung ein verteiltes System in einen Zustand drängt, aus dem es sich ohne Eingriff nicht erholt
  • Ein Beispiel für einen Eingriff ist, die Last unter das normale Niveau zu senken
• Diese Fehlerklasse ist einer der wichtigen Faktoren für Nichtverfügbarkeit in Cloud-Systemen
• Bei typischem metastabilem Verhalten steigt der Goodput mit wachsender Last zunächst, sättigt sich dann, geht in Überlastung über und fällt schließlich auf null oder nahezu null
• Danach kehrt das System nicht allein durch eine leichte Lastreduktion in einen gesunden Zustand zurück; für die Erholung muss die Last deutlich reduziert werden
• Dieses Verhalten kann selbst in einfachen Systemen auftreten und in den meisten Systemen auch durch Client-Logik mit Retries nach Timeouts ausgelöst werden
• Klassische formale Modellierung verteilter Systeme konzentriert sich üblicherweise auf Safety und Liveness; metastabile Fehler zeigen jedoch, dass es Verhalten gibt, das nicht sauber in diese Kategorien passt
• AWS nutzt verstärkt diskrete Ereignissimulation, um emergentes Systemverhalten zu verstehen
  • Investitionen in maßgeschneiderte Systemsimulationen
  • Investitionen in Tools, die bestehende Systemmodelle aus Sprachen wie TLA+ und P für Simulationen nutzbar machen
• Wenn vollständige explorative Model Checker wie TLC für TLA+ um probabilistische Simulation erweitert werden, können statistische Ergebnisse wie nachträgliche Latenzverteilungen erzeugt werden
• Solche Erweiterungen machen Model Checking für Aufgaben nutzbar, etwa um die Erreichbarkeit von Latenz-SLAs zu verstehen

Sicherheitsgrenzen, die formale Beweise erfordern

• Bei wichtigen Sicherheitsgrenzen wie Autorisierung und Virtualisierung reichen die genannten formalen Techniken möglicherweise nicht aus; Korrektheitsbeweise können dort eine große Investition wert sein

• Cedar-Berechtigungsrichtliniensprache

  • AWS führte 2023 die Cedar-Berechtigungsrichtliniensprache ein, um Policies für feingranulare Berechtigungen zu schreiben
  • Cedar wurde mit automatischem Schließen und formalen Beweisen im Blick entwickelt
  • Die Implementierung wurde in der verifikationsfreundlichen Programmiersprache Dafny gebaut
  • Mit Dafny wird bewiesen, dass die Implementierung mehrere Sicherheitseigenschaften erfüllt
  • Dieser Beweis ist ein mathematischer Beweis, der über Tests hinausgeht
  • Das Team verwendet außerdem differenzielles Testen, bei dem Dafny-Code als Korrektheitsorakel dient, um die Korrektheit der produktionsreifen Rust-Implementierung zu verifizieren
  • Zusammen mit der Cedar-Implementierung wurden Dafny-Code und Testverfahren als Open Source veröffentlicht, damit Nutzer die Korrektheitsarbeit prüfen können

• Firecracker VMM

  • Der Firecracker Virtual Machine Monitor nutzt ein Low-Level-Protokoll namens virtio, um emulierte Hardwaregeräte wie Netzwerkkarten oder SSDs dem Gast-Kernel innerhalb einer VM bereitzustellen
  • Da diese emulierten Geräte die komplexesten Interaktionen zwischen einem nicht vertrauenswürdigen Gast und einem vertrauenswürdigen Host darstellen, sind sie eine wichtige Sicherheitsgrenze
  • Das Firecracker-Team nutzt Kani, mit dem sich Rust-Code formal untersuchen lässt, um zentrale Eigenschaften dieser Sicherheitsgrenze zu beweisen
  • Dieser Beweis garantiert, dass wichtige Eigenschaften der Grenze erhalten bleiben, egal was der Gast versucht
  • AWS unterstützt die Entwicklung grundlegender Tools wie Kani, Dafny und Lean sowie der SMT-Solver, die sie antreiben
  • Formale Modelle und Spezifikationen werden auf verschiedene Weise wiederverwendet
    • Model Checking zur Designzeit
    • als Korrektheitsorakel im Laufzeit-Monitoring
    • Simulation emergenten Systemverhaltens
    • Aufbau von Beweisen für zentrale Eigenschaften

Performance- und Kosteneffekte über Korrektheit hinaus

• Formale Techniken sind auch wichtig, um die Performance von Cloud-Systemen sicher zu verbessern
• Durch die Modellierung des zentralen Commit-Protokolls der relationalen Datenbank-Engine Aurora mit P und TLA+ wurde eine Möglichkeit gefunden, die Kosten verteilter Commits von 2 Netzwerk-Roundtrips auf 1,5 Netzwerk-Roundtrips zu reduzieren, ohne Safety-Eigenschaften zu opfern
• Solche Ergebnisse sind bei Teams, die formale Techniken einführen, häufig
  • Der Prozess, verteilte Protokolle gründlich zu durchdenken und formal aufzuschreiben, erzwingt strukturiertes Denken
  • Er liefert tiefere Einsichten in die Protokollstruktur und das zu lösende Problem
  • Wenn vorgeschlagene Designoptimierungen formal überprüft oder bewiesen werden können, können Engineers verteilter Systeme mutigere Designs wählen, ohne das Risiko zu erhöhen
• Produktivitäts- und Kosteneffekte beschränken sich nicht auf Designoptimierungen auf hoher Ebene
• AWS-Teams konnten auf ARM-basierten Graviton-2-Prozessoren eine Optimierung der Implementierung von RSA-Public-Key-Kryptografie finden, die den Durchsatz um bis zu 94 % verbessern kann
• Die Korrektheit dieser Optimierung wurde mit dem interaktiven Theorembeweiser HOL Light bewiesen
• Da ein hoher Anteil der Cloud-CPU-Zyklen für Kryptografie verwendet wird, können solche Optimierungen zu niedrigeren Infrastrukturkosten, mehr Nachhaltigkeit und spürbaren Performance-Verbesserungen für Kunden beitragen

Verbleibende Herausforderungen und künftige Chancen

• AWS hat in den vergangenen 15 Jahren die Skalierung formaler und semi-formaler Testmethoden erfolgreich vorangetrieben, doch für die industrielle Einführung bleiben Herausforderungen
• Eine zentrale Hürde bei Tools für formale Techniken sind die steile Lernkurve und der Bedarf an spezialisiertem Domänenwissen
• Viele Tools haben weiterhin einen akademischen Charakter und es fehlt ihnen an benutzerfreundlichen Oberflächen
• Auch bei gut etablierten semi-formalen Ansätzen gibt es Einführungshürden
  • Deterministische Simulation ist eine zentrale Testtechnik für verteilte Systeme, die bei AWS und Projekten wie FoundationDB erfolgreich eingesetzt wird, ist aber selbst erfahrenen Entwicklern verteilter Systeme, die zu AWS kommen, mitunter unbekannt
  • Ähnliche Lücken gibt es bei bewährten Methoden wie Fehlerinjektionstests, eigenschaftsbasiertem Testen und Fuzzing
• Entwickler verteilter Systeme müssen in diesen Testmethoden und Tools geschult werden, und es ist nötig, strenges Denken zu vermitteln
• Die Bildungslücke beginnt auf akademischer Ebene
  • Selbst grundlegende Ansätze formaler Schlussfolgerung werden selten gelehrt
  • Auch Absolventen führender Einrichtungen haben Schwierigkeiten, solche Tools einzuführen
  • Formale Techniken und automatisches Schließen sind für industrielle Anwendungen wichtig, gelten aber weiterhin als Nischengebiete
• Metastabilität und andere emergente Eigenschaften großer Systeme sind wichtige Forschungsbereiche mit ähnlichen Wahrnehmungsproblemen
  • Praktiken, die metastabiles Systemverhalten auslösen können, etwa „bei Timeout N-mal erneut versuchen“, werden trotz bekannter Probleme weiterhin breit empfohlen
  • Die heutigen Tools und Techniken zum Verständnis emergenten Systemverhaltens stehen noch am Anfang
  • Die Modellierung von Systemstabilität ist teuer und komplex
• AWS geht davon aus, dass große Sprachmodelle und AI-Assistenten erheblich dazu beitragen werden, die praktischen Einführungsprobleme formaler Techniken zu lindern
  • So wie AI-gestützte Unit-Tests populär geworden sind, können sie Entwicklern beim Erstellen formaler Modelle und Spezifikationen helfen
  • Fortgeschrittene Techniken könnten einer breiteren Entwickler-Community zugänglich werden

AWS' fortgesetzte Investition in Korrektheitsverfahren

• Um vertrauenswürdige und sichere Software zu bauen, sind vielfältige Ansätze erforderlich, mit denen sich über Systemkorrektheit schließen lässt
• AWS setzt neben branchenüblichen Tests wie Unit- und Integrationstests mehrere Techniken ein
  • Model Checking
  • Fuzzing
  • eigenschaftsbasiertes Testen
  • Fehlerinjektionstests
  • deterministische Simulation
  • ereignisbasierte Simulation
  • Laufzeitverifikation von Ausführungstraces
• Formale Spezifikationen spielen in vielen Testpraktiken bei AWS eine wichtige Rolle als Testorakel, das die korrekte Antwort liefert
• Korrektheitstests und formale Techniken bleiben auf Grundlage der bereits erzielten Rendite ein zentraler Investitionsbereich für AWS