Überprüfung auf Korrektheit: Wie eine Problemstellung aus der theoretischen Informatik die Welt verändern kann

Hi…

ich habe vor Jahren in einem Projekt mitgearbeitet bei dem es um eine Überprüfung der Funktion von Software ging. In meinem Falle ging es um die Genehmigung Kernkraftwerke steuern zu dürfen. Klingt erstmal dramatisch, ist aber technisch nicht so kompliziert wie zum Beispiel ein Flugzeug. Wenn die Steuerung bei dieser Art von Kernkraftwerk versagt, geht der Meiler automatisch aus. Das kostet viel Geld, aber keine Menschenleben. Flugzeuge sind da unter Umständen anders…

Jedenfalls habe ich damals einen intensiven Geschmack für das Thema “Korrektheit” bekommen.  

Ein wenig Informatik – Der Hintergrund

Was ist denn nun Korrektheit? Wir kommen hier in ein Gebiet, das man durchaus als mathematisch bezeichnen darf. Wikipedia sagt “Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu genügen” (https://de.wikipedia.org/wiki/Korrektheit_(Informatik)). Es gibt verschiedene Unterarten (total korrekt oder partial korrekt als Beispiel) aber wir lassen das mal im Rahmen dieses Artikels.

Um es grob zu beschreiben, führt man einen mathematischen Beweis, dass ein Programm sich an bestimmte Vorgaben hält. Dies ist sehr spannend, wenn man das Thema Software Security und Reliability sich ansieht. In diesen Feldern ist es ja so, dass irgendwas (ein Hacker oder ein Fehler in den Daten oder im Code) das Programm dazu verleitet etwas zu tun, was eben so nicht in den Vorgaben beschrieben ist. Daher findet man in Artikeln zu Korrektheit in der Informatik auch gleich Verweise auf IT Security Standards.

Solche Beweise werden geführt, indem man Vor- und Nachbedingungen definiert und diese überprüft. Da es sich um einen mathematischen Beweis handeln soll, reicht es aus auch nur ein einziges gegenteiliges Beispiel zu finden, um die generelle Aussage zu verneinen.

Sagen wir eine Funktion initialisiert ein Speicherbereich, so kann die Vorbedingung sein, dass der Speicherbereich angefordert und gültig zugewiesen ist. Die Nachbedingung ist, dass der Speicherbereich verändert wurde und nun vollständig mit Nullen gefüllt ist. Wenn nun aufgrund eines Index-Fehlers zum Beispiel die erste Speicherstelle (die berühmte nullte Speicherstelle) nicht mit Null beschrieben ist, so ist die Funktion formal nicht korrekt, da man ein Beispiel nennen kann, bei dem die allgemeine Aussage nicht gilt.

Problem bisher ist, dass es super aufwendig bis unmöglich formal eine solchen Beweis zu führen. Verwendet ein Programm Bibliotheken und/oder ein Betriebssystem so müsste diese in die Beweisführung mit eingebaut werden. Weiterhin alles was neben dem eigentlichen Programm sonst noch sich am Laufen befindet. Wie man sich leicht ausdenken kann, wird das extrem umfangreich.

Umgekehrt gewinnt man natürlich eine ganze Menge an Qualität innerhalb der Software. Wegen des enormen Aufwands geht man jedoch zumeist andere Wege und testet mit vielen verschiedenen Tricks.

Warum HyperV ein gutes Beispiel ist

Wie man sich leicht vorstellen kann, hat Microsoft großes Interesse an der Korrektheit seiner Software. Zusammen mit der Universität des Saarlandes hat Microsoft Research und das EMIC an einem Projekt teilgenommen, das auch durch den deutschen Staat gefördert wird. Ziel war es die formale Beweisführung der Korrektheit von Software an einem nicht trivialen Beispiel mal durchzuspielen. Wer sich mal tiefer damit beschäftigen will, sei auf diese Webseite hingewiesen https://vcc.codeplex.com/. Hier findet man alle Tools (auch im Source-Code) und eine Menge Artikel rund um das Thema.

Das Stück Software, dass man ausgesucht hat, ist HyperV https://www.microsoft.com/windowsserver2008/en/us/hyperv-main.aspx. HyperV hat den Vorteil, dass es sicherlich nicht trivial ist und trotzdem noch überschaubar in der Menge des Source-Codes. Weiterhin hat es als Hypervisor keine darunerliegende Software-Schicht mehr. Will heißen, wenn ich HyperV betrachte, kann ich eine Aussage für HyperV auch wirklich treffen.

Man ist also durch den Source-Code von HyperV gegangen und hat Funktion für Funktion annotiert. Viel Arbeit, keine Frage. Umgekehrt muss ich sagen, wäre ich sehr froh gewesen, wir hätten damals bei unserem Projekt solche Tools gehabt.

Was hat jetzt die Welt davon

Nach Aussagen der Forscher wurden wenige Fehler durch diesen Vorgang in HyperV entdeckt. Für ein Produkt, dass bereits Marktreife hat, sollte das jetzt nicht überraschen. Umgekehrt kann man jetzt den formalen Beweis der Korrektheit führen. Und das ist schon fantastisch.

HyperV kann damit einen hohen Grad an Qualität beweisen. Vorallem aus Sicherheitsaspekten macht das extrem Sinn. Für HyperV kann es damit ein Start in Richtung wirklich hoher Qualitätszertifikate geben. Was der Rest der Welt davon hat, kann man leicht hier sehen https://www.verisoftxt.de/PresseSpiegel.html

CU

0xff