Formale Spezifikation und Verifikation wesentlicher Sicherheitseigenschaften eines Mikrokerns

• Applicant: Dr.-Ing. Michael Hohmuth, since 3/2006
• Subject Area: Theoretical Computer Science
• Term: from 2000 to 2007
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants
• Participating Persons: Professor Dr. Hermann Härtig; Dr. Hendrik Tews
• Ehemaliger Antragsteller: Professor Dr. Horst Reichel, until 3/2006