Formale Spezifikation und Verifikation wesentlicher Sicherheitseigenschaften eines Mikrokerns

• Antragsteller: Dr.-Ing. Michael Hohmuth, seit 3/2006
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2000 bis 2007
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5288276

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