Abo
  • Services:

OKL4

Sicherer Microkernel für mobile Geräte

Open Kernel Labs (OK Labs) hat seinen sicheren Microkernel OKL4 Verified samt OKL4-Hypervisor für mobile Geräte zum Download freigegeben. Ein spezieller Verifizierungsprozess soll Pufferüberläufe oder Speicherlecks bei dessen Entwicklung verhindern.

Artikel veröffentlicht am ,
OKL4: Sicherer Microkernel für mobile Geräte

Das für die x86- und ARM11-basierte Plattformen gedachte Image des Microkernel OKL4 Verified hat einen Hypervisor, auf dem mobile Betriebssysteme laufen, darunter Linux, Windows Mobile und Symbian. Für die Sicherheit sorgt eine auf dem Sel4-Projekt aufgesetzte Infrastruktur, die den Code des Kernels und des Hypervisors verifiziert.

Stellenmarkt
  1. Daimler AG, Großraum Stuttgart
  2. Robert Bosch GmbH, Leonberg

Der Verifizierungsprozess umfasst aber nicht nur die von Werkzeugen wie Lint oder Coverity durchgeführten Prüfungen, die sich meist auf statische Codeanalyse beschränken, sondern auch die Fahndung nach möglichen Pufferüberläufen oder Speicherlecks. Damit soll sich OKL4 Verified vor allem für den Einsatz auf unternehmenskritischen Geräten eignen, über die beispielsweise finanzielle Transaktionen laufen sollen.

Unter dem Microkernel OS laufen sämtliche Anwendungen im Userspace, der schmale Hypervisor sorgt für eine Schicht, auf der das eigentliche Betriebssystem läuft. Zudem hat das OS eine minimale Posix-Umgebung, in der die Anwendungen, aber auch Treiber laufen können. Sie werden in voneinander getrennten Partitionen gespeichert.

Das Sel4-Projekt wurde von der NICTA (National Information and Communications Technology Australia) sowie von der University von New South Wales (UNSW) in Australien betrieben. Der Hypervisor basiert auf Technologie, die an der Technischen Universität Dresden unter dem Namen Nova-Projekt vorangetrieben wurde.

Die Forschungsergebnisse gingen an das Unternehmen OK Labs, das das Microkernel OS jetzt zum Download freigab. Die kostenlose Variante ist für die nichtkommerzielle Nutzung gedacht. In dem Download sind startbare Images für x86 und ARM11, entsprechende Userspace-Bibliotheken und weiterer Quellcode, um entsprechende Anwendungen zu erstellen. Zusätzlich enthält das Paket eine paravirtualisierte Linux-Distribution, die auf OKL4 Verified läuft, sowie eine Dokumentation und die Spezifikationen. Teile des Microkernels stehen unter proprietären Lizenzen.

Weitere Informationen zu Sel4 und dem Sicherheitskonzept haben die Entwickler in einem Whitepaper zusammengestellt.



Anzeige
Blu-ray-Angebote
  1. 4,25€
  2. (2 Monate Sky Ticket für nur 4,99€)
  3. 9,99€

Der Kaiser! 27. Jan 2011

Zum Thema "Pufferüberläufe und Speicherlecks verhindern" leisten PaX und KERNHEAP gute...


Folgen Sie uns
       


Volocopter auf der Cebit 2018 angesehen

Im autonomen Volocopter haben zwei Personen mit zusammen höchstens 160 Kilogramm Platz - wir haben uns auf der Cebit 2018 trotzdem reingesetzt.

Volocopter auf der Cebit 2018 angesehen Video aufrufen
Jurassic World Evolution im Test: Das Leben findet einen Weg
Jurassic World Evolution im Test
Das Leben findet einen Weg

Ian Malcolm hatte recht: Das Leben wird ausgegraben und gebrütet, es frisst und stirbt oder es bricht aus und macht Jagd auf die Besucher. Nur leider haben die Entwickler von Jurassic World Evolution ein paar kleine Design-Fehler begangen, so wie Henry Wu bei der Dino-DNA.
Ein Test von Marc Sauter

  1. Vampyr im Test Zwischen Dracula und Doktor
  2. Fe im Test Fuchs im Farbenrausch
  3. Thaumistry: In Charm's Way im Test Text-Adventure der ganz alten Schule

K-Byte: Byton fährt ein irres Tempo
K-Byte
Byton fährt ein irres Tempo

Das Startup Byton zeigt zur Eröffnung der Elektronikmesse CES Asia in Shanghai das Modell K-Byte. Die elektrische Limousine basiert auf der Plattform des SUV, der vor fünf Monaten auf der CES in Las Vegas vorgestellt wurde. Unter deutscher Führung nimmt der Elektroautohersteller in China mächtig Fahrt auf.
Ein Bericht von Dirk Kunde

  1. Elektromobiltät UPS kauft 1.000 Elektrolieferwagen von Workhorse
  2. KYMCO Elektroroller mit Tauschakku-Infrastruktur
  3. Elektromobilität Niu stellt zwei neue Elektromotorroller vor

Business-Festival: Cebit verliert 70.000 Besucher und ist hochzufrieden
Business-Festival
Cebit verliert 70.000 Besucher und ist hochzufrieden

Cebit 2018 Zur ersten neuen Cebit sind deutlich weniger Besucher als im Vorjahr gekommen. Dennoch feiern Messe AG, Bitkom und Aussteller den Relaunch der Veranstaltung als Erfolg. Die Cebit 2019 wird erneut etwas verlegt.

  1. Festival statt Technikmesse "Die neue Cebit ist ein Proof of Concept"

    •  /