Was ein Beweis versprechen kann

Software vertraut man meist, weil sie getestet wurde. Jemand hat überlegt, was schiefgehen könnte, hat es ausprobiert und zugesehen, wie sie damit zurechtkommt. Das funktioniert gut, bis zu dem Fall, an den niemand gedacht hat.

Ein Beweis fängt am anderen Ende an. Er probiert keine Fälle durch. Er zeigt mit den Mitteln der Mathematik, dass eine Aussage für alle Fälle gilt.

Jeder Fall, nicht nur die ausprobierten

Nehmen wir ein kleines Versprechen: Dieser Code liest nie über das Ende seines Puffers hinaus. Ein Test kann ihm tausend Eingaben geben oder eine Milliarde und melden, dass keine davon ihn aus dem Tritt gebracht hat. Ein Beweis sagt etwas anderer Art: Es gibt keine Eingabe, die das schafft. Es wurde keine gefunden, und es existiert keine.

Der Preis dafür ist Strenge. Ein Beweis braucht eine exakte Aussage darüber, was der Code tun soll, seine Spezifikation, und ein Argument, das jede Zeile des Codes mit ihr verbindet. Für echte Software ist dieses Argument viel zu lang, als dass ein Mensch es mit bloßem Auge prüfen könnte. Also prüft es ein Computer.

Von der Maschine geprüft

Das bedeutet „maschinengeprüft“. Der Beweis wird vollständig ausgeschrieben, in einer Sprache, die ein Programm namens Beweisassistent lesen kann, und das Programm prüft jeden Schritt gegen die Regeln der Logik. Es wird auf Seite neunhundert nicht müde, und es glaubt niemandem etwas aufs Wort.

Die Beweise von seL4 werden so geprüft, in einem Beweisassistenten namens Isabelle/HOL. Sie sind öffentlich, und jeder kann sie erneut durchlaufen lassen.

Was die Beweise von seL4 aussagen

seL4 ist der Kernel, auf dem jedes NoWayOS-System läuft: rund 10.000 Zeilen Code, und der einzige Code mit vollständiger Kontrolle über das Gerät. Auf die Größe kommt es an. Ein Argument über zehntausend Zeilen lässt sich zu Ende führen. Ein Argument über mehrere zehn Millionen noch nicht.

Die seL4 Foundation legt die Beweise in Schichten dar:

• Der Code tut, was die Spezifikation sagt, und nichts darüber hinaus. Daraus folgt eine Liste von Dingen, die der Kernel nicht tun kann: über einen Puffer hinausschreiben, einem Nullzeiger folgen, Speicher verlieren, durch null teilen.
• Das Programm, das läuft, entspricht dem Code, der bewiesen wurde. Dazwischen sitzt ein Compiler, also prüft ein weiterer Beweis dessen Ausgabe.
• Der Kernel kann die Teile eines Systems voneinander getrennt halten. Ein Teil kann die Daten eines anderen nicht ändern, nicht lesen und ihm die benötigten Ressourcen nicht nehmen, es sei denn, ihm wurde das Recht dazu gewährt.
• Ein System kann in dem Zustand starten, für den es entworfen wurde, mit genau den Rechten, die seine Beschreibung aufführt.

Nicht jede Schicht ist für jeden Prozessor und jede Konfiguration fertig. Das ist wichtig, und wir kommen darauf zurück.

Was ein Beweis voraussetzt

Ein Beweis ist genau so weit wie seine Aussage, und er steht auf seinen Annahmen. seL4 schreibt die eigenen auf: dass sich die Hardware so verhält, wie ihr Modell es beschreibt, dass einige hundert Zeilen des hardwarenächsten Codes stimmen, dass der Code, der vor dem Start des Kernels läuft, seine Arbeit getan hat. Der Beweis der Vertraulichkeit deckt das Zeitverhalten nicht ab.

Er sagt nichts darüber, ob die Spezifikation das Richtige verlangt, und nichts über die Software oberhalb des Kernels. Ein bewiesener Kernel isoliert zuverlässig auch ein Programm, das einen Fehler enthält. Der Fehler ist immer noch da. Er kommt nur an nichts anderes heran.

Das ist keine Schwäche der Beweise. Es macht sie erst wertvoll: Sie sagen genau, was sie abdecken, also wissen Sie genau, was übrig bleibt.

Wo NoWayOS steht

Hier ist der Stand, ohne Umschweife. NoWayOS läuft auf seL4, aber kein NoWayOS-Image liegt heute innerhalb der abgeschlossenen Beweise von seL4. NoWayOS nutzt die Mixed-Criticality-Konfiguration von seL4, deren Beweise für unsere Prozessoren in Arbeit sind. Und den eigenen Code von NoWayOS haben die Beweise von seL4 nie abgedeckt. Deshalb nennen wir NoWayOS nicht “formal verifiziert”, und wir werden es auch nicht tun.

Jedes Image sagt, wo es steht. Eine Datei daneben führt die Konfiguration seines Kernels auf, Option für Option, neben derjenigen, die seL4 bewiesen hat. Sicherheit zeigt eine echte.

Kleinere Beweise aus eigener Hand

Der Code von NoWayOS bekommt seine Absicherung auf anderem Weg: Rust, Isolation, Review, Tests und Beweise von bescheidenerer Art.

Jeder Decoder der Nachrichten, die zwischen den Teilen eines Systems fließen, hat beschränkte Beweise, erstellt mit einem Model Checker namens Kani. Ein beschränkter Beweis deckt jede Eingabe bis zu einer festgelegten Größe ab, hier den längsten Datensatz, den ein Decoder annimmt. Innerhalb dieser Schranke ist er ein echter Beweis: Keine Eingabe bringt den Decoder zum Panic, zum Überlauf oder dazu, außerhalb der Grenzen zu lesen. Jenseits der Schranke sagt er nichts, und deshalb ist die Schranke die längste Eingabe, die es gibt.

Dann machen wir die Decoder absichtlich kaputt, um sicherzugehen, dass die Beweise es merken. Ein Beweis, der nicht scheitern kann, ist nicht besser als ein Test, der es nicht kann.

Die ehrliche Größe der Sache

Ein Beweis macht nichts “unhackbar”. Er macht eine Aussage wahr, in jedem Fall, unter Annahmen, die Sie nachlesen können. Wer die Aussage und die Annahmen kennt, weiß, was er hat.

Deshalb baut NoWayOS auf dem Kernel auf, der solche Beweise hat, und sagt Ihnen, Image für Image, wie weit sie reichen.