Sicherer Microkernel seL4 jetzt Open Source

29.07.2014

Der formal verifizierte Microkernel seL4 wurde jetzt unter einer Open-Source-Lizenz veröffentlicht.

Auf der seLE4-Homepage ist ab sofort der Quellcode eines Microkernels zu finden, dessen Korrektheit formal verifiziert wurde. Mit Hilfe des Theorembeweisers Isabelle/HOL haben die Entwickler bewiesen, dass die Implementierung der Spezifikation des Systems entspricht. seL4 basiert auf dem L4 Microkernel, der auch die Basis für den OKL4-Microkernel ist, der in mehr als einer Milliarde Mobilgeräten eingesetzt wird.

In seL4 sind nur die nötigsten Features als Kernel-Code umgesetzt, der mit höherer Priorität läuft, etwa Prozessorzugriff, Timer und Interrupt-Handling. Andere Betriebssystemfunktionen sind im Userspace implementiert und mit entsprechend weniger Rechten ausgestattet, beispielsweise auch die Device-Treiber. seL4 kann zur Virtualisierung auch als Hypervisor verwendet werden, auf dem beispielsweise Linux als Gastsystem zum Einsatz kommt. 

Nach Meinung der Entwickler ist seL4 nicht auf einen spezifischen Einsatzzweck beschränkt, sondern eignet sich für alle Anwendungen, die Subsysteme voneinander isolieren möchten. Der Schwerpunkt liegt dabei zwar auf Embedded-Systemen, etwa im Automobil- oder Luftfahrt-Sektor, denkbar sind aber beispielsweise auch Finanzanwendungen.

Auch die formale Verifikation des Systems garantiert letztlich keine hundertprozentige Sicherheit oder Zuverlässigkeit, denn sie stellt nur sicher, dass die Implementation des Kernels der Spezifikation entspricht. Bugs etwa im Compiler könnten dennoch noch zu Fehlern im resultierenden Kernelcode führen. Außerdem ist nicht gesichert, dass die Spezifikation als solche fehlerfrei ist.

seL4 läuft x86- und ARM-Prozessoren (v6/7), um die Device-Treiber müssen sich Anwender des Betriebssystems selber kümmern. Freigegeben wurde der Code vom australischen Forschungszentrum NICTA und der Rüstungsfirma General Dynamics C4 Systems. Der Kernel und die Beweise sind unter der GPLv2-Lizenz verfügbar, die User-Libraries unter einer BSD-Lizenz.

Ähnliche Artikel

comments powered by Disqus
Mehr zum Thema

News

Artikel der Woche

Eigene Registry für Docker-Images

Wer selber Docker-Images herstellt, braucht auch eine eigene Registry. Diese gibt es ebenfalls als Docker-Image, aber nur mit eingeschränkter Funktionalität. Mit einem Auth-Server wird daraus ein brauchbares Repository für Images. (mehr)
Einmal pro Woche aktuelle News, kostenlose Artikel und nützliche ADMIN-Tipps.
Ich habe die Datenschutzerklärung gelesen und bin einverstanden.

Konfigurationsmanagement

Ich konfiguriere meine Server

  • von Hand
  • mit eigenen Skripts
  • mit Puppet
  • mit Ansible
  • mit Saltstack
  • mit Chef
  • mit CFengine
  • mit dem Nix-System
  • mit Containern
  • mit anderer Konfigurationsmanagement-Software

Google+

Ausgabe /2019