Press Releases

PikeOS entspricht den Anforderungen der funktionalen Sicherheit (Safety) und wird bereits in großen sicherheitskritischen Projekten eingesetzt. Das Systemdesign von PikeOS entspricht zusätzlich dem MILS Standard (Multiple Level of Security) und berücksichtigt so gleichzeitig die Anforderungen an die Security von embedded Systemen. Der Common Criteria Standard schreibt für hohe Security Levels eine formale Verifikation der Betriebssystem-Schicht(en) vor, die in komplexen Systemen die Anwendungen mit der Hardware verbinden. Die Korrektheit dieser Softwarekomponenten ist eine der größten Herausforderungen, mit denen sich Anbieter von embedded Systemen in zunehmendem Maße konfrontiert sehen.

Lange Zeit war es eher eine akademische Übung, über die Korrektheit von Betriebssystemen nachzudenken. Dies ändert sich heutzutage mit der zunehmenden Verwendung von sogenannten Separation-Kernels, wo die Analyse der Partitionen eine häufige geübte Praxis ist. Die Präsentation zeigt, wie sich das von der Universität Saarbrücken entwickelte Framework CVM "concurrent virtual machines" als Checkliste für die Korrektheit von PikeOS anwenden lässt.

Für den formalen Beweis der Korrektheit des Mikrokernels wird zunächst ein Simulationstheorem zwischen einem abstrakten Modell und dem aus einem Kernel und Benutzerprogrammen bestehenden System beschrieben, die abwechselnd auf einer realen Maschine laufen. Dann werden am Beispiel eines typischen Code Trace, die Korrektheitseigenschaften für alle Komponenten des Trace identifiziert.

Die berücksichtigten Korrektheitskriterien beinhalten nicht nur Eigenschaften funktionaler Korrektheit, d.h. dass die Funktionalitäten des Kernels der Spezifikation entsprechen. Sie umfassen ebenfalls die Invarianten der Kernel-Implementierung wie z.B. die Speichertrennung. Da sich die Verifikation kritischer Sicherheitsanforderungen durch herkömmliche Testverfahren nicht einfach erreichen lässt, können formale Methoden den mathematischen Beweis liefern, dass die Kernkonzepte einer Kernel-Implementierung geeignet sind, eine sichere Virtualisierung zu garantieren.

Der formale Beweis der Korrektheit von PikeOS wird unter Verwendung von VCC geführt, einem von Microsoft Research entwickelt automatisierten C-Verifikationswerkzeugs. Diese Arbeit erfolgt in Zusammenarbeit mit dem europäischen Microsoft Innovation Center in Aachen sowie den Universitäten Koblenz und Saarbrücken und ist Teil des vom BMBF finanzierten Projekts Verisoft XT.

Christoph Baumann, Universität Saarbrücken, hält die Präsentation "Ingredients of Operating System Correctness - Lessons Learned in the Formal Verification of PikeOS" während der embedded world conference 2010 in Nürnberg. Die Präsentation ist Teil des Konferenzprogramms, Sitzung 1.4, Test und Verifikation II. Sie findet am Dienstag, dem 2. März, 15:00 - 15:30 Uhr statt.

Das Verisoft XT Projekt

Verisoft XT ist ein über drei Jahre angelegtes Forschungsprojekt, das vom Bundesministerium für Bildung und Forschung (BMBF) gefördert wird. Projektträger ist das Deutsche Zentrum für Luft- und Raumfahrttechnik (DLR). Ehrgeiziges Projektziel ist die durchgängige, formale Verifikation von Computersystemen: die korrekte Funktionsweise von Systemen, wie sie beispielsweise im Automobilbau, in der Sicherheitstechnologie und auf dem medizinischtechnischen Sektor zum Einsatz kommen, soll mathematisch bewiesen werden. Die Beweise werden dabei computergestützt geführt, um menschliches Versagen der beteiligten Wissenschaftler nach Möglichkeit auszuschließen. Die gewonnenen Erkenntnisse und erzielten Fortschritte sollen dabei helfen, deutschen Unternehmen aus diesen Sparten dauerhafte internationale Wettbewerbsvorteile zu schaffen.

Die Leitvorstellung des Vorhabens Verisoft XT besteht darin:

• die Methoden und Werkzeuge zu schaffen, die es gestatten, das Design von integrierten Computersystemen durchgehend formal zu verifizieren,
• dadurch einen Produktivitäts- und Qualitätshub für die Industrie zu generieren, und
• dieses an vier konkreten, industriellen Anwendungsszenarien prototypisch zu realisieren.

Verisoft XT ist das Nachfolgeprojekt von Verisoft. Es ist über drei Jahre angelegt und durch das BMBF bewilligt. Weitere Information sind erhältlich unter www.verisoft.de

Über PikeOS

PikeOS ist Virtualisierungsplattform und Betriebssystem für embedded Systeme zugleich, die mehrere virtuelle Maschinen simultan in einer geschützten Umgebung ermöglicht. Die SSV Technologie (Safe and Secure Virtualization) bietet mehrere Betriebssystemschnittstellen, sogenannte "Personalities", die gleichzeitig auf einer Hardware laufen können, z.B. eine sicherheitskritische ARINC-653 Anwendung zusammen mit Linux. Durch seine Mikrokernel Architektur kann PikeOS sowohl in preis sensitiven Geräten mit beschränkten Ressourcen als auch in großen, komplexen Systemen eingesetzt werden. Die Kompaktheit und Klarheit des Systemdesigns von PikeOS bietet eine Echtzeitperformanz, die konventionellen Echtzeitbetriebssystemen entspricht. PikeOS ist MILS konform und zertifizierbar nach Sicherheitsstandards wie DO-178B, IEC 61508 oder EN 50128.

Mehr Informationen unter www.sysgo.com/pikeos