- Amazon Web Services (AWS) betrachtet Korrektheit als einen zentralen Wert und integriert verschiedene Formen formaler Methoden in den Entwicklungsprozess
- Mit Werkzeugen für formale Spezifikationen wie TLA+ und der Sprache P lassen sich subtile Bugs früh erkennen und auch bei mutigen Optimierungen Zuverlässigkeit sicherstellen
- AWS setzt mit leichtgewichtigen formalen Methoden außerdem breit auf eigenschaftsbasiertes Testen, deterministische Simulation und kontinuierliches Fuzzing
- Mit Fehlerinjektions-Tools wie dem Fault Injection Service wird die Zuverlässigkeitsprüfung automatisiert – auch für Situationen, in denen tatsächlich Störungen auftreten
- Lernhürden und die Komplexität der Werkzeuge bestehen weiterhin, doch die Verbreitung von KI und Automatisierungstools dürfte die Einführung beschleunigen
AWS-Strategie zur Sicherstellung der Systemkorrektheit
Amazon Web Services (AWS) verfolgt das Ziel, hochzuverlässige Services bereitzustellen, denen Kunden vollständig vertrauen können.
Dafür will das Unternehmen die Maßstäbe für Sicherheit, Dauerhaftigkeit, Integrität und Verfügbarkeit einhalten und stellt dabei das Konzept der Systemkorrektheit in den Mittelpunkt.
Seit der 2015 in Communications of the ACM vorgestellten Anwendung formaler Methoden bei AWS spielt dieser Ansatz eine wichtige Rolle für den erfolgreichen Betrieb zentraler Services.
Im Zentrum steht TLA+, eine von Leslie Lamport entwickelte formale Spezifikationssprache.
Die Erfahrungen von AWS mit TLA+ haben gezeigt, dass sich damit bereits in frühen Entwicklungsphasen feine Bugs aufspüren lassen, die mit herkömmlichen Tests nicht gefunden werden.
Zudem konnte AWS selbst bei ambitionierten Performance-Optimierungen durch formale Verifikation Stabilität und Zuverlässigkeit absichern.
Vor 15 Jahren blieb AWS noch auf einem grundlegenden Niveau mit Unit-Tests zum Build-Zeitpunkt und begrenzten Integrationstests, führte danach jedoch formale und semi-formale Methoden umfassend ein.
Dieser Wandel trug nicht nur zur Korrektheit bei, sondern auch zur Verifikation von Optimierungen auf hoher und niedriger Ebene, zu höherer Entwicklungsgeschwindigkeit und zu geringeren Kosten.
Bei AWS werden nicht nur klassische formale Beweise und Model Checking, sondern auch eigenschaftsbasiertes Testen, Fuzzing und Runtime Monitoring in den Bereich formaler Methoden einbezogen.
Die Einführung der Programmiersprache P
Anfangs hatte TLA+ zwar den Vorteil einer starken abstrakten Beschreibung, doch für viele Entwickler war die mathematische Notation eine hohe Einstiegshürde.
Deshalb führte AWS die Sprache P ein, die einen zustandsmaschinenbasierten Ansatz bietet, der Entwicklern vertrauter ist.
Die Sprache P stellt ein Zustandsmaschinen-Modell für den Entwurf und die Analyse verteilter Systeme bereit.
Das ist ein Konzept, das Amazon-Entwicklern mit mikroservicebasierter SOA-Architektur vertraut ist.
Seit 2019 wird P bei AWS entwickelt und als strategisches Open-Source-Projekt gepflegt.
Wichtige Service-Teams wie Amazon S3, EBS, DynamoDB, Aurora, EC2 und IoT nutzen P, um die Korrektheit ihrer Systementwürfe zu verifizieren.
Bei der Umstellung von S3 auf starke Read-after-Write-Konsistenz wurden Protokolle mit P modelliert und verifiziert, sodass Bugs früh im Design entfernt und Optimierungen sicher übernommen werden konnten.
2023 entwickelte das AWS-P-Team das Tool PObserve, mit dem sich die Korrektheit verteilter Systeme sowohl in Tests als auch in realen Produktionsumgebungen prüfen lässt.
PObserve extrahiert Ausführungslogs und ermöglicht eine nachträgliche Verifikation, ob das Verhalten der Spezifikation entspricht. Damit verbindet es Spezifikationen aus der Entwurfsphase effektiv mit der realen Code-Implementierung.
Ausbau leichtgewichtiger formaler Methoden
Eigenschaftsbasiertes Testen
Die bekannteste leichtgewichtige formale Technik ist eigenschaftsbasiertes Testen.
So nutzt etwa das ShardStore-Entwicklungsteam von S3 über den gesamten Entwicklungszyklus hinweg eine Kombination aus eigenschaftsbasiertem Testen, code-coverage-basiertem Fuzzing, Fehlerinjektion und Minimierung von Gegenbeispielen.
Dieser Ansatz ist mit von Entwicklern direkt geschriebenen Korrektheitsspezifikationen verknüpft und verbessert zugleich die Effizienz beim Debugging deutlich.
Deterministische Simulation
Bei Tests mit deterministischer Simulation wird ein verteiltes System in einem Single-Thread-Simulator ausgeführt, sodass sich alle Zufallselemente wie Scheduling, Timing und Nachrichtenreihenfolge kontrollieren lassen.
Das wird auf verschiedene Weise eingesetzt, etwa für Tests bestimmter Fehler- und Erfolgsszenarien, zur Anpassung von bugauslösenden Abläufen oder zur Erweiterung von Fuzzing.
Dadurch lassen sich Verhalten wie Latenz und Ausfälle bereits früh in der Build-Phase prüfen, und die Testabdeckung wird erweitert.
AWS hat diesen Build-Time-Testcode als Open-Source-Projekte shuttle und turmoil veröffentlicht.
Kontinuierliches Fuzzing
Kontinuierliches Fuzzing, insbesondere großskalige Input-Generierung auf Basis von Code Coverage, ist in der Integrationstestphase wirksam für die Verifikation der Systemkorrektheit.
Bei der Entwicklung von Aurora Limitless Database wurden beispielsweise SQL-Abfragen und Transaktionen gefuzzt, um die Korrektheit der Partitionierungslogik mit einer großen Menge zufälliger Schemas, Datensätze und Queries zu prüfen.
Die Ergebnisse werden mit dem Verhalten der non-sharded Engine oder mit Ansätzen wie SQLancer verglichen.
Durch die Kombination von Fuzzing und Fehlerinjektion werden zentrale Datenbankeigenschaften wie Atomarität, Konsistenz und Isolation verifiziert.
Einige Eigenschaften wie automatisch generierte Transaktionen und Isolation werden über eine nachträgliche Verifikation auf Basis von Ausführungsverläufen abgesichert.
Fehlerinjektion mit dem Fault Injection Service
2021 brachte AWS den Fault Injection Service (FIS) auf den Markt, damit auch Kunden verschiedene Fehlerszenarien wie API-Fehler, I/O-Unterbrechungen und Instanzenausfälle schnell in realen oder Testumgebungen ausprobieren können.
Dadurch lassen sich Verfügbarkeit und Resilienz von Architekturen prüfen, die hohe Bug-Dichte in Fehlerfällen adressieren und schwerwiegende wahrscheinliche Probleme frühzeitig entdecken.
FIS wird nicht nur von AWS-Kunden, sondern auch intern bei Amazon breit genutzt; allein in den Vorbereitungen auf den Prime Day wurden 733 Experimente durchgeführt.
Fehlerinjektion ist in Kombination mit formalen Spezifikationen noch wirksamer.
Wenn das erwartete Verhalten formal spezifiziert und das tatsächlich durch Fehler ausgelöste Ergebnis dagegen geprüft wird, lassen sich mehr Fehler entdecken als mit einer bloßen Kontrolle von Logs und Metriken.
Metastabilität und emergentes Systemverhalten
In verteilten Systemen häufen sich Fälle, in denen durch übermäßige Last oder erschöpfte Caches anomale, nicht selbstständig behebbare Zustände entstehen, also metastabile Zustände.
In einem solchen Zustand reicht eine bloße Lastreduktion nicht aus, um zum Normalbetrieb zurückzukehren, und die Reaktion ist schwieriger als bei üblichen Fehlerfällen.
Auch die meisten Retry- und Timeout-Logiken sind Ursache solcher Phänomene.
Klassische formale Spezifikationen konzentrieren sich auf Sicherheit und Liveness, doch bei Metastabilität müssen darüber hinaus verschiedene emergente Verhaltensweisen berücksichtigt werden.
AWS führt auf Basis von Spezifikationsmodellen wie TLA+ und P diskrete Ereignissimulationen durch und analysiert damit systematisch auch probabilistische Eigenschaften wie die Erreichbarkeit von Performance-SLAs oder Latenzverteilungen.
Die Notwendigkeit formaler Beweise
In einigen Sicherheitsgrenzen (Berechtigungen, Virtualisierung usw.) sind mathematisch belastbare Beweise unverzichtbar und einfache Tests nicht ausreichend.
So ist etwa die 2023 von AWS eingeführte Berechtigungsrichtlinien-Sprache Cedar auf Basis von Dafny für automatische Beweise und formale Verifikation optimiert; durch den offenen Code und Korrekturverfahren können alle Nutzer dies selbst verifizieren.
Auch für zentrale Sicherheitseigenschaften der Firecracker-VMM werden mit Rust-Code-Analysetools wie Kani Beweise geführt.
Auf diese Weise werden formale Modelle und Spezifikationen an vielen Stellen breit genutzt – beim Entwurf, bei der Implementierung, im Betrieb und beim Beweis –, um Softwarekorrektheit sicherzustellen und den Wert für Unternehmen und Kunden zu steigern.
Zusätzliche Effekte über Korrektheit hinaus
Formale Methoden spielen sowohl für Zuverlässigkeit als auch für Performance-Verbesserungen eine wichtige Rolle.
So wurde etwa das Commit-Protokoll von Aurora mit P und TLA+ verifiziert, wodurch sich die Zahl der nötigen Netzwerk-Roundtrips senken ließ, ohne die Sicherheit zu gefährden.
Bei der Optimierung des RSA-Verschlüsselungsalgorithmus für ARM Graviton 2 wurde in HOL Light die mathematische Korrektheit der Transformation bewiesen, was zu einem praktischen Effekt führte: bessere Performance bei zugleich geringeren Infrastrukturkosten.
Künftige Herausforderungen und Chancen
In den vergangenen 15 Jahren hat AWS den industriellen Einsatz formaler und semi-formaler Methoden stark ausgebaut, doch praktische Einführungshürden wie Lernkurve, Bedarf an Experten und der akademische Charakter vieler Tools bestehen weiterhin.
Auch eigenschaftsbasiertes Testen und deterministische Simulation sind vielen Entwicklern noch immer wenig vertraut.
Da die pädagogische Einstiegshürde bereits im Hochschulstudium beginnt, schreiten Verbreitung und Praxiseinsatz der Werkzeuge und Methoden nur langsam voran.
Auch emergente Eigenschaften großer Systeme wie Metastabilität befinden sich noch in einem frühen Forschungsstadium.
Künftig dürften KI/große Sprachmodelle das Erstellen formaler Modelle und Spezifikationen unterstützen und so die Zugänglichkeit für Praktiker in kurzer Zeit deutlich verbessern.
Fazit
Für robuste und sichere Software sind vielfältige Mittel zur Sicherstellung von Systemkorrektheit notwendig.
AWS setzt neben klassischen Testverfahren auch umfassend auf Model Checking, Fuzzing, eigenschaftsbasiertes Testen, Fehlerinjektions-Tests, deterministische bzw. ereignisbasierte Simulationen und die Verifikation von Ausführungsverläufen.
Formale Spezifikationen und Methoden fungieren im Entwicklungsprozess von AWS als wichtiger Test-Orakel-Mechanismus und haben sich durch ihren praktischen und wirtschaftlichen Nutzen bereits als eigenständiger Investitionsbereich etabliert.
1 Kommentare
Hacker-News-Kommentare
Ich möchte über deterministische Simulationstests sprechen. Bei AWS werden verteilte Systeme in einem Single-Thread-Simulator ausgeführt, während alle nichtdeterministischen Faktoren wie Thread-Scheduling, Timing und die Reihenfolge der Nachrichtenübermittlung kontrolliert werden. Anschließend schreibt man Tests, die auf bestimmte Fehler- oder Erfolgsszenarien zugeschnitten sind, und die Nichtdeterministik innerhalb des Systems wird vom Test-Framework gesteuert. Entwickler können bestimmte Reihenfolgen festlegen, die in der Vergangenheit Bugs verursacht haben. Der Scheduler kann auf Fuzzing von Reihenfolgen oder sogar auf die Erkundung aller möglichen Reihenfolgen erweitert werden. Ich frage mich, ob es dafür eine sprachunabhängige Open-Source-Bibliothek gibt. Die Idee wäre ein Middleware-Tool, das auch Networking, Storage usw. innerhalb von Containern zum Testzeitpunkt „deterministisch“ macht. antithesis erfüllt fast genau diese Rolle, aber ich habe so etwas bisher nicht als Open Source gesehen. Mit gut geschriebenen Tests lässt sich ein Teil davon lösen, indem man etwa I/O stubbt, aber es ist nicht garantiert, dass alle gute Tests schreiben. Ich denke, es wäre hilfreich, Determinismus auf einer höheren Ebene oberhalb der Anwendung bereitzustellen. Andererseits hoffe ich, dass AI beim Testen wirklich glänzen kann. Prompt (Anforderung) – Testimplementierung – AI – ausführbarer Code: Diese drei Achsen könnten ideal ineinandergreifen. Ich hoffe, dass AI formale Verifikation einfacher macht und die Softwarewelt dadurch noch strenger und präziser wird
Bei der Verbreitung der Technik deterministischer Simulationstests (DST) gibt es zwei Schwierigkeiten. Erstens musste man bisher das gesamte System direkt auf ein bestimmtes Simulations-Framework setzen, ohne andere Abhängigkeiten. Zweitens sehen Tests bei schwacher Eingabegenerierung und Exploration so aus, als würden sie alle erfolgreich durchlaufen, ohne tatsächlich viel zu verifizieren. antithesis versucht, beide Probleme zu lösen, aber das bleibt schwierig. Es gibt kaum jemanden mit einer verlässlichen Methode, Determinismus auf beliebige Software anzuwenden. Das Hermit-Projekt von Facebook war ebenfalls ein Versuch mit deterministischem Linux-Userspace, wurde aber letztlich eingestellt. Deterministische Computer sind nicht nur für Tests eine sehr nützliche technische Grundlage, und ich denke, irgendwann wird das jemand als Open Source veröffentlichen
Ich denke, es ist vergleichsweise einfach, mit QEMU im 100-%-Emulationsmodus in einem Single-Thread eine deterministische Maschine zu erhalten. Was man aber wirklich will, ist eine „kontrollierte“ deterministische Ausführung, und das ist viel schwieriger. Mehrere Prozesse in einem vorgegebenen Szenario ablaufen zu lassen, ist besonders auf Ebene von CPU- und OS-Scheduler sehr anspruchsvoll. Es ist auch schwer, eine wirklich sprachunabhängige Umgebung zu bauen, und man verliert sich leicht in Details. Ich selbst habe einmal ein einfaches System gebaut, das mehrere JVM-Threads an bestimmten Ausführungspunkten im Lockstep laufen ließ, wobei I/O und Systemzeit durch Stubs und Kontrolle behandelt wurden. Damit konnte ich verschiedene Interaktionen zwischen asynchronen Komponenten, I/O-Ausfälle, Retries usw. testen und lästige Bugs vor dem Production-Rollout finden. Allerdings war das nur möglich, weil ich statt des gesamten Systems nur bestimmte Synchronisationspunkte vereinfacht habe. Allgemeine Data Races durch fehlerhafte Synchronisation sind mit diesem Ansatz schwer zu finden
Offizielle Dokumentation zu den Testmethoden von FoundationDB sowie ein YouTube-Vortrag
Für Sprachen, die sich mit gdb debuggen lassen, empfehle ich das Projekt https://rr-project.org/
Ich erinnere mich, vor langer Zeit einen Vortrag gesehen zu haben, in dem Joe Armstrong Dropbox mit Property Testing getestet hat
Ich halte S3 für eine der beeindruckendsten Software, die ich je gesehen habe. Dass dem gesamten S3-System vor einigen Jahren starke Read-after-Write-Konsistenz hinzugefügt wurde, ist für mich ebenfalls ein Höhepunkt echter Software-Engineering-Kunst Link zum Blogpost
Ich habe selbst direkt am Lifecycle von S3 gearbeitet, und das fiel in die Zeit, als das Index-Team die Struktur für diese Konsistenzgarantien neu entwarf. Schon von außen ist S3 beeindruckend, aber intern sind sowohl die Implementierung als auch die Organisationsstruktur noch weit eindrucksvoller, als man es sich vorstellen würde
Google Cloud Storage hatte diese Funktion starke Konsistenz im Gegenteil schon viel früher als S3. Insgesamt habe ich den Eindruck, dass GCS ein etwas systematischeres und sauberer gebautes Produkt ist
Ich stimme der Zahl von 92 % zu, also dass die meisten Cluster-Ausfälle mit trivialen Fehlern beginnen. Meistens sind es nicht spektakuläre Großstörungen, sondern „nichts Besonderes“ wirkende Retries, die Zustände aufsummieren und dann am Ende um 2 Uhr morgens zu einem großen Ausfall führen. Es ist wichtig, mehr Engineering-Zeit auf unscheinbare Fehler zu verwenden
Ich finde das einen wirklich interessanten Artikel. Der Einsatz von Zustandsmaschinen beim Aufbau von Infrastruktur-Control-Planes ist unverzichtbar. Ich bin mir nicht sicher, ob dafür unbedingt P nötig war. Wir haben ebenfalls über 13 Jahre lang Infrastruktur-Control-Planes in Ruby gebaut, und das hat hervorragend funktioniert Blog über entsprechende Erfahrungen
Ich hatte eine Frage zur Sprache P. Früher schien Microsoft für den Windows-USB-Stack zur Laufzeit C-Code aus P zu generieren und tatsächlich produktiv einzusetzen, aber inzwischen scheint man daraus keinen Betriebscode mehr zu erzeugen. Ich hatte dazu auch einmal eine Frage auf Hacker News gestellt Link zur Frage. Wenn generierter Code sogar im Kernel landen kann, müsste das erst recht auch in einer Cloud-Umgebung mit deutlich lockereren Anforderungen einsetzbar sein
Aus Sicht von jemandem, der nicht von AWS kommt und weder mit TLA+ noch mit P vertraut ist, wäre selbst ein „Hello World“-ähnliches Beispiel hilfreich gewesen, um es leichter zu verstehen. So wie der Text dasteht, wirkt es fast wie ein schmerzhafter Prozess, und man fragt sich, ob das nicht Probleme sind, die sich auch mit gutem Design und guten Tests ausreichend lösen lassen. Ein einfaches Beispiel hätte besser geholfen zu beurteilen, was konkret gemacht wird
Ich habe ein schnelles Demo-Beispiel für TLA+, das ich mag Gist-Link. Es modelliert mehrere Threads, die einen gemeinsamen Zähler nicht atomar erhöhen, und bei der Eigenschaftenprüfung wird eine Race Condition gefunden. Solche Bugs sind in der Praxis mit Tests allein sehr schwer zu entdecken. Die meisten TLA+-Spezifikationen sind deutlich komplexer, aber dieses Beispiel ist gut, um einfache Fehler sichtbar zu machen
Ich habe TLA selbst ausprobiert und war enttäuscht, dass das grafische Tool nicht gut zur Tutorial-Erfahrung passte. TLA selbst wollte ich gern verwenden, und ich mochte Lamports Arbeit schon lange, von LaTeX bis zu seinen Papers
Die Voraussetzung für den Einsatz formaler Methoden ist letztlich, dass man mit Tests allein nie absolut alle Probleme finden kann
Ich empfehle das offizielle TLA+-Examples-GitHub-Repository. Am besten beginnt man mit etwas Einfachem wie dem DieHard-Problem
Tests beweisen die Korrektheit einer Implementierung für bestimmte Instanzen eines Problems, während formale Verifikation sie für eine gesamte Klasse beweist. Bei einer Funktion, die etwa Anagramme zurückgibt, kann man mit Tests nur einige Wortpaare prüfen; um Korrektheit für alle Wortpaare zu beweisen, braucht man formale Verifikation. Auch Dinge wie undefined behavior oder Bibliotheks-Bugs werden oft nur im Rahmen formaler Verifikation entdeckt
Bei der Erwähnung von „leichtgewichtigen semiformellen Methoden wie Property-based Testing, Fuzzing und Runtime Monitoring“ habe ich das Gefühl, dass Property-based Testing und Fuzzing zwar Teilmengen formaler Methoden sind, es aber etwas weit geht, auch Runtime Monitoring zu den semiformellen Methoden zu zählen
Ich hatte früher einmal Kontakt zu Leslie Lamport, unter anderem wegen des Papers zum Buridan’s Principle. Heute habe ich auf seiner Website viel über TLA+ und PlusCal gelernt Peterson-Beispielseite. Dass jemand, der Mathematik in die Programmierung gebracht hat und als einer der Begründer des Bereichs nebenläufiger Systeme gilt, eine Systementwurfssprache wie TLA+ geschaffen hat, die bei AWS und anderswo eingesetzt wird, erscheint mir vollkommen natürlich. Ich wünschte, mehr Leute, die verteilte Systeme bauen, würden Lamports Werk nutzen. Bei großen Systemen ist ein Korrektheitsbeweis enorm wichtig
Für die Umwandlung bestehender Codebases in TLA+-Spezifikationen ist Claude Opus (Extended Thinking) ziemlich brauchbar. Ich habe damit in Rust-Projekten und bei der Verifikation zentraler C++-Komponenten mehrere Bugs gefunden. Andere Modelle scheitern oft an Syntax und Spezifikationslogik, während Opus deutlich reibungsloser funktioniert
Nicht nur für große Systeme, auch für kleine, aber kritische und weltweit verbreitete Werkzeuge wie SSH oder Terminals sind Korrektheitsbeweise sehr nützlich
Zur Aussage „Korrektheit des Systems beweisen“: Tatsächlich kann man nie alles beweisen. Ein Model Checker kann nur innerhalb eines begrenzten Zustandsraums feststellen, dass die angegebene Spezifikation die Eigenschaften erfüllt
Mich würde interessieren, ob jemand persönlich Erfahrungen damit hat, FIS für Experimente mit verteilten Services zu nutzen. Ich ziehe eine Einführung in Betracht, habe aber selbst noch keine groß angelegten Experimente damit gemacht
Ich frage mich, ob Promela und SPIN Sprachen auf einem höheren Abstraktionsniveau sind als das, was im Artikel behandelt wird