PRAVDA - Parametrisierte Verifikation Fehlertoleranter Verteilter Algorithmen

Da unsere Gesellschaft in vielen Bereichen vom Funktionieren von Computersystemen abhängig ist, müssen wir Computersystemen auf eine Art und Weise entwickeln, die Fehler systematisch ausschließt. Wir stehen vor zwei Herausvorderungen: Erstens müssen wir Systeme so entwerfen, dass sie Fehler tolerieren die nicht unter der Kontrolle der Entwickler stehen, z.B. teilweiser Stromausfall. Zweitens müssen wir frühzeitig Fehler in der Systemimplementierung (Bugs) finden und eliminieren. Die erste Herausforderung kann mit fehlertoleranten verteilten Algorithmen, die zweite mit formaler Verifikation, z.B. durch Model Checking, angegangen werden. Traditionellerweise werden diese beiden Herangehensweisen allerdings getrennt betrachtet. Diese Projekt zielt auf deren Kombination, d.h. die formale Verifikation fehlertoleranter verteilter Algorithmen. Üblicherweise benutzt man mathematische Beweise um die Korrektheit fehlertoleranter verteilter Algorithmen zu zeigen. Da verteilte Systeme aber inherent kompliziert sind, und die Argumentationen von denen der klassischen Informatik abweichen, ist dieser Zugang fehleranfällig. Wenn wir also kein Vertrauen in die Korrektheit fehlertoleranter verteilter Algorithmen haben können, ist es fragwürdig ob diese ihr Ziel der Steigerung der Verlässlichkeit tatsächlich erreichen. Wir brauchen daher zusätzliche Mittel um das Vertrauen in die Algorithmen zu erhöhen. In diesem Projekt studieren wir dazu Model Checking, da es einen hohen Automatisierungsgrad verspricht und bereits sehr erfolgreich in der Verifikation von Hardware und Software eingesetzt wird. Speziel untersucht dieses Projekt das Problem der Parametrisierung fehlertoleranter verteilter Algorithmen. Fehlertolerante verteilte Algorithmen sind üblicherweise durch die Anzahl der Prozesse n sowie durch die angenommene Maximalzahl an Fehlern t parametrisiert. Zusätzlich gibt es Bedingungen, die die Parameter in Beziehung setzen, z.B. die Bedingung, dass eine Mehrheit der Prozesse Fehlerfrei ist, d.h. n > 2t. Daraus folgt das Verifikationsproblem das eine unendliche Familie von endlichen Systeminstanzen mit fixierten n und t verifiziert werden müssen, die n > 2t erfüllen. Ähnliche Probleme wurden unter dem Begriff parametrisiertes Model Checking untersucht. Parametrisiertes Model Checking ist für viele Systemtypen immer noch ein herausforderndes Problem, und im speziellen fehlertolerante verteilte Algorithmen weisen Charakteristiken auf die in der Literatur noch nicht untersucht wurden. Im Zuge des PRAVDA Projektes werden wir neue Methoden für parametrisiertes Model Checking entwickeln, die uns erlauben werden die Korrektheit fehlertoleranter verteilter Algorithmen automatisch zu zeigen.

Bei der Entwicklung zuverlässiger Computersysteme steht man vor zwei Herausforderungen: Einerseits muss man Protokolle entwerfen, die Teilausfälle, die außerhalb der Kontrolle der Systementwicklerinnen liegen (z. B. teilweise Stromausfälle) tolerieren können. Andererseits muss man Designfehler (Bugs) finden, um sie zu beheben. Das Erstere wird mittels Replikation und fehlertoleranter verteilter Algorithmen (FTDAs) erzielt, und letzteres durch rigorose System- und Software-Engineering-Methoden, wie Model Checking. Während in der Vergangenheit diese FTDAs nur in sicherheitskritischen Systemen Anwendung fanden, gibt es jetzt Implementierung von FTDAs für immer mehr Anwendungsbereiche. Der klassische Ansatz zur Überprüfung der Korrektheit von FTDAs sind mathematische Beweise. Das Verfassen solcher Beweise ist fehleranfällig weil die Argumentation oft von der in der Mainstream-Informatik abweicht. Infolgedessen enthalten sogar veröffentlichte verteilte Algorithmen Fehler. Es ist daher fraglich ob FTDAs, die die Zuverlässigkeit des Systems erhöhen sollen dieses Ziel tatsächlich erreichen. Daher benötigen wir zusätzliche Maßnahmen um das Vertrauen in die Korrektheit von FTDAs zu erhöhen. Das PRAVDA Projekt hat zu diesem Zweck neue automatisierte Verifikationstechniken entwickelt, z.B. neue parameterisierte Model-Checking- oder deduktive Verifikationsmethoden. Diese Methoden versprechen einen höheren Grad an Automatisierung und sind daher weniger fehleranfällig als der klassische Ansatz. Wir haben erhebliche Fortschritte auf dem Gebiet der automatischen Verifikation Verteilter Systeme erzielt. Während sich klassische automatisierte Verifikationstechniken auf Sicherheitseigenschaften ("nie passiert etwas schlechtes") konzentrieren, motivierten uns fehlertolerante verteilte Algorithmen, uns gezielt auch mit Lebendigkeitseigenschaften ("irgendwann wird etwas gutes passieren") zu befassen. Ein weiterer Schwerpunkt lag darauf, die Beziehung zwischen asynchroner Semantik (die erfasst, wie sich ein reales System verhält) und synchroner Semantik (die abstrakter ist und einfacheres Argumentieren erlaubt) zu erforschen. Die Anpassung klassischer Reduktionsmethoden an die Besonderheiten der FTDAs haben uns mehrere Durchbrüche für ihre Verifikation ermöglicht. Unabhängig vom (und außerhalb der Forschungsfragen des) PRAVDA Projektes haben Blockchainprojekte wie Tendermint oder Facebooks Libra, byzantinisch fehlertolerante verteilte Algorithmen für hunderte von beteiligten Computern implementiert. Prinzipiell stellen parametrisierte Verifikationsmethoden eine solide Grundlage dar, um die Korrekheit solcher Systeme überprüfen zu können. Angesichts der Vermögenswerte, die in solchen Blockchainsystemen verwaltet werden, findet sich die automatisierte Verifikation der Fehlertoleranz verteilter Systeme plötzlich im Mainstream der Informatik. Obwohl die Lücke zwischen der Verifikation von Protokollen und deren Implementierungen immer noch beträchtlich is (und mehr Forschung auf diesem Gebiet verlangt) bildet die Forschung von PRAVDA eine solide Grundlage dafür.