PikeOS

Merkmale

Microkernel

3Generation ???, Verifikation in Arbeit [hersteller]
[ElphinstoneHeiser2013]: Beruht auf unabhängiger L4-Implementierung P4 und wurde weiter optimiert, zertifizert und in Avionik Anwendungen eingesetzt.

Partitionierung

(para-)Virtualisierung von verschiedenen Systemen/APIs,

Echtzeit - Rechenzeit und Speicherdeterminismus [Hersteller]

Teil von SeSaM

Kommentar: Die Architektur entspricht den Hoffnungen der Microkernel-Architektur: Ein Microkern kann verschiedene Systeme paravirtualisieren, in dem Sinne dass die Resourcen sauber partioniert sind (Ein Subsystem darf die anderen nicht beeinflussen). Sicherheitskritische Subsysteme können im Sinne der Nizza-Architektur isoliert und verifiziert werden.

Normierungen/Zertifizierung

• Normen: DO178B,IEC 61508 EN50128
• MILS separation kernel architecture ???

Links

Hersteller SysGO

"SeSaM für sichere Umgebung - Forschungsschwerpunkte der IT-Sicherheit",Behördenspiegel 9/2011

[Wikipedia über PikeOS]