Formale Spezifikation und Verifikation wesentlicher Sicherheitseigenschaften eines Mikrokerns

Fortschritte auf dem Gebiet der formalen Verifikation führen zu immer umfangreicheren, erfolgreich abgeschlossenen Verifikationsprojekten realer Hard- und Software. Die Forschung auf dem Gebiet der Betriebssysteme hat mit den Mikrokernen der neuesten Generation sehr kompakte Betriebssysteme mit minimaler Funktionalität hervorgebracht. Die Antragsteller wollen die Fortschritte auf beiden Gebieten zusammenführen. Ziel des Projektes ist die Spezifikation der sicherheitsrelevanten Eigenschaften eines Mikrokerns, die Implementierung des Mikrokerns und die formale Verifikation der Korrektheit der Implementation. In der Weiterführung des Projektes sollen die technischen Voraussetzungen für eine Zertifizierung E6 des Bundesamtes für Sicherheit in der Informationstechnik geschaffen werden. Die Verifikation des Mikrokerns ermöglicht die Verifikation und sicherheitstechnische Überprüfung von Computeranwendungen auf neuem Niveau: die Sicherheitsmodelle von Anwendungen sind nicht mehr von unbewiesenen Annahmen über das Verhalten des Betriebssystemes abhängig.

DFG-Verfahren Sachbeihilfen

Beteiligte Personen Professor Dr. Hermann Härtig; Dr. Hendrik Tews

Ehemaliger Antragsteller Professor Dr. Horst Reichel, bis 3/2006