2022 | VeritAS

Computer und Software, die in Flugzeugen Flugsteuerungsaufgaben umsetzen, müssen den höchsten Sicherheitsanforderungen genügen, da Menschenleben von deren korrekter Funktionsweise abhängen. Fehlerhafte Flugcomputer müssen innerhalb kürzester Zeit identifiziert und deaktiviert werden, um eine Fehlerausbreitung mit fatalen Folgen zu verhindern. Bisherige Lösungen zur Sicherstellung der Integrität solcher Systeme basieren auf Computerreplika:  Die Steuerungsfunktion wird auf mehreren Rechnern (Replikas) parallel ausgeführt, die sich gegenseitig vergleichen, um Unstimmigkeiten zu erkennen. Die Realisierung dieser Lösung ist technisch komplex: Die Rechner müssen aufwendig synchronisiert werden und müssen Konsensus zwischen Eingangs- und Zwischenergebnissen aufweisen. Dies wird durch aufwändige Algorithmen erzwungen, wobei viel Rechenzeit und Bandbreite verloren geht. Zudem müssen Rechner und Software meist ähnlich sein, damit sie vergleichbar sind. Damit sind Fehler, die in den replizierten Rechnern gleich vorhanden sind (Common-Mode-Fehler), wahrscheinlich. Insgesamt ist die Fehlertoleranz von Computersystemen und der Nachweis davon der Hauptkostentreiber fliegender Computersysteme. Kein Kleinflugzeug hat heute eine sicherheitskritische, ausschließlich digitale Flugsteuerung! Im Großflugzeugbereich werden etwa 100 M€ für die Entwicklung und Zulassung digitaler Flugsteuerung ausgegeben. 

Ein neuer Forschungszweig aus der Kryptographie lässt vermuten, dass eine disruptiv andere Lösung für sicherheitskritische Systeme möglich ist: Was ist, wenn ein Computer überprüfbar und nicht fälschbar nachweisen kann, dass er seine Aufgabe richtig erfüllt hat? Das heißt ein Computer erbringt zusätzlich zu dem Ergebnis der Steuerungsfunktion mittels eines Prover-Algorithmus einen schnell durch einen Verifier-Algorithmus zu überprüfenden Beweis, dass er die erwartete Aufgabe (ein in Software implementierter Algorithmus) richtig bearbeitet hat. Der Beweis ist fälschungssicher, das heißt ein fehlerhafter Rechner ist nicht in der Lage, für eine falsch durchgeführte Rechnung infolge eines Hardware- oder Softwarefehlers einen gültigen Beweis zu generieren. Die Überprüfung des Beweises ist so einfach, dass ein sehr kleiner Rechner ausreicht ihn auszuführen. Eine solche Lösung würde, falls anwendbar, einen radikalen Paradigmenwechsel für sicherheitskritischen Computersysteme bedeuten. Synchronisierung, Konsensus und andere Anforderungen, die bei der Replika-Methode gestellt werden, fallen weg. Es werden neue, kompaktere, leichtere sicherheitskritische Systemarchitekturen ermöglicht und der Nachweis der Korrektheit einfacher. Mehr noch könnten Funktionen sicherheitskritisch realisiert werden, bei denen das heute aufgrund Ihrer Komplexität nicht möglich ist, z.B. fortgeschrittene Algorithmen der künstlichen Intelligenz, wie Bilderkennung.

Möglich werden kann das vorgeschlagene Konzept durch enorme Fortschritte in den letzten 8 Jahren bei den Methoden des Verifiable Computing. Es wurde eine Reihe an Algorithmen entwickelt, die das Beweisen und Überprüfen der Korrektheit von Rechnungen ermöglichen, ohne diese selbst ausgeführt zu haben. Es gibt erste Anwendungen in den Bereichen Kryptowährungen und Blockchain. Die Möglichkeiten des Verifiable Computings für sicherheitskritische Echtzeitsysteme sind sehr vielversprechend aber bisher nicht untersucht worden. Diese Lücke möchten wir in VeritAS schließen und die folgenden Forschungsfragen beantworten:

1. Was ist das tatsächliche Potenzial heutiger Verifiable Computing Methoden hinsichtlich der Komplexität verifizierbarer Algorithmen (Prover) und des Aufwands der Verifizierung (Verifier)?
2. Welche neuen sicherheitskritischen Systemarchitekturen sind technisch umsetzbar, wie sehen sie aus und wie sind diese hinsichtlich des Aufwands und Vorteilen zu bewerten?
3. Gibt es Anforderungen für Verifiable Computing in Avioniksystemen, die noch nicht erfüllbar sind – sowohl im Hinblick auf die technische Machbarkeit als auch die geltenden Zulassungsvorschriften?

Zur Beantwortung wurde am ILS ein Demonstrator entwickelt, der den ersten in Echtzeit überprüfbaren Regelungsalgorithmus für eine vereinfachte Höhenrudersteuerung beinhaltet.