Microsoft steigt in deutsches Forschungsprojekt ein

Wenn bewiesen wird, dass Computersysteme ihre mathematisch exakten Vorgaben korrekt erfüllen, spricht man von formaler Verifikation. Die Methoden für die formale Verifikation von komplexen Computersystemen umfassen Soft- und Hardware. Sie werden im Rahmen des Forschungsprojekts Verisoft seit 2001 entwickelt.

Das Ziel von Verisoft XT ist es jetzt, ein Qualitätssiegel „Verified in Germany“ zu erarbeiten und die Verifikation auf existierende Industrieprojekte anzuwenden. Für diese soll der mathematische und maschinell überprüfte Beweis erbracht werden, dass die betrachteten Computersysteme im Entwurf null Fehler enthalten.

In den Forschungsarbeiten, mit denen Microsoft die Saarbrücker Informatikforschung beauftragt hat, geht es um mehr Sicherheit für Betriebssysteme. Da Betriebssysteme heute einfach zu bedienen sind, aber gleichzeitig eine Fülle von Funktionen enthalten, entstehen Sicherheitslücken. Kleinere Betriebssysteme sind zwar überschaubarer und damit vertrauenswürdiger. Sie bieten jedoch nicht den heute erforderlichen Komfort.

Der „Hypervisor“ soll eine Lösung für dieses Dilemma darstellen. Vereinfacht gesagt handelt es sich um ein Betriebssystem für Betriebssysteme. Er soll sicherstellen, dass es keinen unerlaubten Speicherzugriff zwischen einzelnen Betriebssystemen gibt. Mit Verisoft XT soll an einem konkreten Beispiel gezeigt werden, dass auch böswillige Anwender keine Chance haben, den verifizierten Hypervisor zu überlisten.

An dem Informatik-Projekt sind neben der Universität des Saarlandes weitere Universitäten, Forschungsinstitute und Unternehmen beteiligt. Die Konsortialführung liegt beim Deutschen Forschungszentrum für Künstliche Intelligenz (DFKI). Das Projekt wird vom BMBF mit rund zwölf Millionen Euro gefördert. (dsc)