Login
Login-Name Passwort


 
Newsletter
Werbung

Di, 29. Juli 2014, 14:12

Software::Kernel

seL4-Mikrokernel im Quellcode veröffentlicht

National ICT Australia (NICTA) hat den Microkernel »seL4« unter eine Open-Source-Lizenz gestellt. Der Kernel zeichnet sich vor allem durch seine Sicherheit aus und wurde unter anderem formal auf Korrektheit geprüft.

Bei seL4 handelt es sich um einen Mikrokernel, der ursprünglich der L4-Familie entstammt und auf Konzepten von Jochen Liedtke basiert. Der Kernel bietet unter anderem eine synchrone IPC (Interprozesskommunikation), Interrupt- und Thread-Management sowie eine Speicherverwaltung. Dem modularen Prinzip des Kernels folgend können auf dem L4 Oberflächen oder weitere Kernel gestartet werden. Ein Beispiel der Funktionsweise liefert dabei »Motorola Evoke«. Während der OKL4 die Basis darstellt, kümmert sich Linux um die Benutzerführung und BREW von Qualcomm um die Modem-Funktionalität.

Bereits seit 2004 wird von dem National ICT Australia (NICTA) und General Dynamics C4 Systems eine eigene Variante unter dem Namen seL4 (secure embedded L4) entwickelt. Das System wurde speziell an sicherheitskritische Anwendungen im eingebetteten Bereich angepasst. Dazu wurde das System formal auf seine Korrektheit verifiziert. Unter anderem wurde von den Prüfern mathematisch bewiesen, dass die Implementierung die Spezifikation des Kernels erfüllt und der Kernel keinen der verbreiteten Entwurfsfehler (Speicherüberläufe, Zeigerfehler und Speicherlecks) enthält.

Wie NICTA nun bekannt gab, steht seL4 unter den Bedingungen der GNU General Public License Version 2 (GNU GPLv2) allen Nutzern zum Bezug bereit. seL4 läuft auf x86- und ARM-Prozessoren (v6/7) und fokussiert eingebettete Systeme, etwa in der Automobilbranche. Denkbar sind aber auch andere Einsatzgebiete. Im Gegensatz zu Linux müssen sich aber die Anwender in der Regel um Treiber selber kümmern, was vor allem eine Nutzung im privaten Bereich erheblich einschränken dürfte. Die Bibliotheken der Veröffentlichung stehen unter einer BSD-Lizenz. Der Quellcode kann ab sofort auf der GitHub-Plattform gefunden werden.

Werbung
Kommentare (Insgesamt: 3 || Alle anzeigen || Kommentieren )
Endlich HURD kommt doch nächstes Jahr! (olaf, Di, 29. Juli 2014)
Re: Bugfrei? (Bolitho, Di, 29. Juli 2014)
Bugfrei? (5 Minuten, Di, 29. Juli 2014)
Pro-Linux
Pro-Linux @Facebook
Neue Nachrichten
Werbung