Arbeiten an fehlerfreier, sicherer Software

Forscher von NICTA (National ICT Australia), dem australischen Kompetenzzentrum für Informations- und Kommunikationstechnologie, versuchen, Fehler aus der Software zu entfernen:

"Fast jedes Papier zur formalen Verifizierung beginnt mit der Beobachtung, dass die Komplexität der Software zunimmt, dass dies zu Fehlern führt und dass dies ein Problem für unternehmens- und sicherheitskritische Software darstellt. Wir sind uns einig, wie die meisten."

Mein erster Gedanke: Auf keinen Fall. Wie können Sie jeden einzelnen Fehler beseitigen? Einige der komplexeren Softwarepakete müssen mindestens eine Million Codezeilen enthalten.

Die NICTA-Leute sind sich der Komplexität bewusst. Aus diesem Grund konzentrieren sie sich zunächst auf kleine eingebettete Systemsoftware.

Wie Autos

Jedes Mal, wenn mein Vater mit einem Computerproblem anruft, weist er darauf hin, dass es kriminell ist, wie wir fehlerhafte Software akzeptieren: "Es wird ein kalter Tag in der Hölle, bevor ich so ein Auto kaufe."

Schneller Vorlauf zu einem kürzlichen Anruf meines Vaters. Ich wusste nicht, ob ich lachen oder weinen sollte. Sein Auto wurde für ein Software-Update zurückgerufen.

NICTAs Suche

NICTA-Forscher erwähnten:

"Das muss nicht so sein. Ihr Unternehmen gibt eine neue Verkaufssoftware in Betrieb ... Sie schreiben in einem Vertrag genau auf, was die Software tun soll.

Und dann - tut es. Immer. Und die Entwickler können es Ihnen beweisen - mit einem tatsächlichen mathematisch maschinengeprüften Beweis. "

Klingt zu schön um wahr zu sein, nicht wahr? Dennoch machen Akademiker keine unbegründeten Ansprüche geltend. Also, was haben die NICTA-Teammitglieder gemeinsam im Ärmel? Ich kontaktierte NICTA und Dr. June Andronick erklärte freiwillig, was sie gelernt hatten.

Kassner : Wie sind Sie zum ersten Mal auf die Codeüberprüfung aufmerksam geworden? Und ist es so entmutigend, wie es scheint? Andronick : Ich komme aus der Mathematik. Ich habe angefangen, Code mit der Einstellung zu schreiben, in der Sie darüber nachdenken, warum sich Ihr Programm so verhalten sollte, wie Sie es erwarten. Zum Beispiel: "Warum genau sollte es enden?"

Ich fand die formale Codeüberprüfung eine faszinierende Möglichkeit, die beiden Welten zu kombinieren ... genau das zu schreiben, was Sie vom Programm erwarten ... und dann zu beweisen, dass dies der Fall ist.

Einiges davon ist intuitiv: Programmierer haben normalerweise das Gefühl, warum ihr Programm tut, was sie wollen. Die Codeüberprüfung formalisiert diese Argumentation nur und lässt sie maschinell überprüfen, ohne dass Zweifel bestehen.

Es mag entmutigend klingen, aber es macht tatsächlich viel Spaß und macht süchtig. Es ist wie ein Spiel zwischen Ihnen und dem Proof-Tool - Sie versuchen, es davon zu überzeugen, warum Sie denken, dass etwas wahr ist.

Kassner : Sie haben den seL4-Mikrokernel verwendet, um Ihre Theorien zu testen. Warum hast du diesen Kernel ausgewählt? Andronick : Das Ziel des L4.verified-Projekts unter der Leitung von Professor Gerwin Klein war die formelle Überprüfung von seL4, einem neuen Mikrokernel, der von Dr. Kevin Elphinstone entworfen wurde. Dies ist der erste Schritt in Richtung der langfristigen Vision unserer Gruppe unter der Leitung von Professor Gernot Heiser, wirklich vertrauenswürdige Software zu entwickeln, für die Sie eine starke Garantie für ihre Sicherheit und Zuverlässigkeit bieten können.

Die Entscheidung, zuerst den Kernel in Angriff zu nehmen, hängt von einem Hauptgrund ab: Es ist der kritischste Teil des Systems, der sich zwischen der Hardware und dem Rest der Software befindet. Es hat vollen Zugriff auf alle Ressourcen und steuert, auf welche andere Software zugegriffen werden kann.

Jedes Verhalten des Systems hängt von allen Aspekten der Kernelfunktionalität ab. Jede Garantie für das System muss also damit beginnen, dass der Kernel funktionell korrekt ist.

Da es keinen Schutz gegen Fehler im Kernel gibt, kann jeder Fehler dort möglicherweise willkürlichen Schaden verursachen. Das Konzept des Mikrokernels besteht darin, die Menge dieses kritischen Codes auf ein Minimum zu reduzieren und die "vertrauenswürdige Computerbasis" zu reduzieren.

Das Ergebnis des Projekts war ein formaler Beweis für die funktionale Korrektheit von seL4. Dies bedeutet, dass der Kernel unter den Annahmen des Beweises niemals abstürzen oder sich auf andere Weise unerwartet verhalten kann.

Dies war der erste formale Beweis für die funktionale Korrektheit eines Allzweck-Betriebssystemkerns und allgemeiner für jede reale Anwendung von erheblicher Größe.

Kassner : 8700 Zeilen C und 600 Zeilen Assembler scheinen viel zu überprüfender Code zu sein. Ist es das, was die folgende Folie zeigt? Könnten Sie bitte erklären, was wir sehen?

Andronick: Dieses Bild zeigt das sogenannte Funktionsaufrufdiagramm von seL4. Jede C-Funktion im Kernel ist ein Punkt. Wenn Funktion A Funktion B aufruft, gibt es einen Pfeil von A nach B.

Die Grafik zeigt, dass seL4 eine hochkomplexe Software mit stark miteinander verbundenen Teilen ist. Dies ist typisch für leistungsoptimierte Mikrokerne.

Ausgereifte Software auf Anwendungsebene würde Gruppen oder Inseln mit stark verwandten Punkten aufweisen, die durch eine kleine Anzahl von Pfeilen verbunden sind, die zwischen den Inseln eine Brücke schlagen.

Kassner : Sie verwenden die Begriffe formale Verifikation und funktionale Korrektheit. Können Sie beschreiben, was sie jeweils bedeuten und welche Rollen sie spielen? Andronick : Die formale Verifikation bezieht sich auf die Anwendung mathematischer Beweisverfahren, um Eigenschaften von Programmen festzustellen. Es kann nicht nur alle Codezeilen oder alle Entscheidungen in einem Programm abdecken, sondern alle möglichen Verhaltensweisen für alle möglichen Eingaben.

Diese umfassende Abdeckung aller möglichen Szenarien unterscheidet sie von Tests, bei denen nur Fehler gefunden werden können, nicht das Fehlen von Fehlern.

Funktionale Korrektheit bedeutet, dass sich der Kernel in seiner Spezifikation wie erwartet verhält. Diese Eigenschaft ist stärker und präziser als dies mit automatisierten Techniken wie Modellprüfung oder statischer Analyse möglich ist.

Wir analysieren nicht nur bestimmte Aspekte des Kernels, wie z. B. die sichere Ausführung, sondern liefern auch eine vollständige Spezifikation und einen Beweis für das genaue Verhalten des Kernels.

Der Ansatz, den wir verwenden, ist der Beweis eines interaktiven Theorems . Es erfordert menschliches Eingreifen und Kreativität, um den Beweis zu konstruieren und zu leiten, hat jedoch den Vorteil, dass es nicht auf bestimmte Eigenschaften oder endliche, realisierbare Zustandsräume beschränkt ist.

Kassner : Ich verstehe jetzt, wonach Sie suchen. Können Sie einen kurzen Überblick darüber geben, wie Sie versuchen, Probleme zu finden? Andronick : Ein Problem wird erkannt, wenn sich der Code nicht wie in der Spezifikation vorgeschrieben verhält.

Der Prozess beginnt mit dem Schreiben einer formalen Spezifikation dessen, was der Kernel tun soll. Beispielsweise können Sie verlangen, dass eine Sortierfunktion eine sortierte Liste mit denselben Elementen wie die Eingabeliste zurückgibt. Der Code beschreibt, wie diese Funktionalität implementiert wird, indem ein Sortieralgorithmus ausgewählt wird.

Dann müssen Sie nachweisen, dass das Ergebnis der Funktion immer den Spezifikationsanforderungen entspricht. Das entscheidende Unterscheidungsmerkmal beim Testen ist wiederum, dass wir über alle möglichen Eingaben nachdenken. Wenn die Spezifikation für einige Eingaben nicht gilt, wird dies durch den Beweis angezeigt. Der Fehler wird behoben und der Proofversuch wird fortgesetzt. Wenn der Beweis abgeschlossen ist, wissen Sie , dass keine Implementierungsfehler mehr vorhanden sind.

Kassner : Was ist der nächste Schritt für den Verifizierungsprozess? Kann dieses Verfahren verwendet werden, um Computer-Betriebssysteme zu testen, an die wir gewöhnt sind? Andronick : Der exakt gleiche Ansatz lässt sich nicht auf Systeme skalieren, die eine Million Codezeilen umfassen, wie z. B. moderne Betriebssysteme. Wir haben jedoch einen Plan für große komplexe Systeme.

Das erste, was zu beachten ist, ist, dass eine formale Überprüfung nicht billig ist. Wir haben erhebliche Anstrengungen unternommen, um etwa 10.000 Codezeilen zu überprüfen. Es erscheint immer noch kostengünstig und besser als andere Methoden, die ein geringeres Maß an Vertrauenswürdigkeit erreichen.

Die Hauptbotschaft ist, dass solch gründliche Methoden in kritischen Systemen (Medizin, Automobil, Verteidigung usw.) wirklich Sinn machen.

Unser Ansatz für große kritische Systeme basiert auf der Beobachtung, dass in solchen Systemen nicht der gesamte Code kritisch ist. Beispielsweise verfügen medizinische Geräte über große Benutzeroberflächen und Flugzeuge über Unterhaltungssoftware (Prof. Heiser hat einen relevanten Blog verfasst, in dem die Notwendigkeit eines verifizierten Kernels am Beispiel von Bordunterhaltungssystemen veranschaulicht wird).

Die Schlüsselidee unserer aktuellen Arbeit ist es , die unkritischen Teile von den kritischen zu isolieren . Dies erfolgt mithilfe von seL4 und seiner Zugriffskontrolle. Auf diese Weise können wir nachweisen, dass ein Fehler in den nicht kritischen Teilen nicht verhindern kann, dass sich die kritischen Teile korrekt verhalten. Auf diese Weise können wir den Überprüfungsaufwand auf die kritischen Teile des Systems konzentrieren.

Mit anderen Worten, wir zeigen, dass eine formale Überprüfung der Funktionskorrektheit für Betriebssystem-Mikrokerne praktisch möglich ist, und wir arbeiten nun daran, diese vertrauenswürdige Grundlage zu nutzen, um starke Garantien für große kritische Systeme zu geben.

Kassner : Lustig sollte man Unterhaltungssoftware für Fluggesellschaften erwähnen. Während eines kürzlichen roten Auges in Amsterdam rannten die Flugbegleiter die Gänge auf und ab und entschuldigten sich. Das Unterhaltungssystem war ausgefallen. "Es sollte bald auf sein." Sie sagten: "Der Kapitän startet einen Computer neu."

Abschließende Gedanken

Meine brennende Frage: "Was steuert dieser Computer noch?" Mir wurde versichert, dass alles unter Kontrolle war.

© Copyright 2020 | mobilegn.com