Abo
  • Services:
Anzeige
Der Microkernel Sel4 im Einsatz
Der Microkernel Sel4 im Einsatz (Bild: Nicta)

Sel4: Fehlerloser Microkernel unter der GPL freigegeben

Der von der National ICT Australia mitentwickelte Microkernel Sel4 steht ab sofort unter der GPL. Er wurde durch mehrere Testverfahren als vollständig fehlerfrei eingestuft.

Anzeige

Der Microkernel Sel4 gilt als vollkommen fehlerfrei und daher als sicher. Er wurde von der National ICT Australia (Nicta) zusammen mit dem US-Unternehmen General Dynamics C4 im Rahmen des Darpa-Programs High-Assurance Cyber Military Systems entwickelt. Jetzt steht der gesamte Code unter der GPLv2 sowie der BSD-Lizenz und kann auf Github eingesehen werden.

Das Besondere an Sel4 ist das ausgiebige Testverfahren, dem der Code unterzogen wurde. Der Verifizierungsprozess umfasste 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. Auch die Inter-Process Communication (IPC) sowie die Zugriffsrechte wurden untersucht. Letztere wurden auch im Rahmen der Zugriffe aus dem User-Space getestet.

Der Microkernel wurde bewusst klein gehalten, er kümmert sich ausschließlich um die Verwaltung von Interrupts, virtuellen Adressräumen, Threadverwaltung, IPC, besitzt eine Speicherverwaltung und regelt die Zugriffsrechte. Sämtliche Treiber oder Systemdienste laufen im User-Space. Dadurch soll zum einen die Stabilität des Systems gewährleistet werden - stürzt eine Komponente ab, können die anderen weiterlaufen. Zum anderen sorgen die Zugriffsrechte dafür, dass das System nicht von außen angegriffen werden kann. In den ausgiebigen Tests wurden auch Worst-Case-Szenarios durchprobiert.

Für ARM und x86

Sel4 wird deshalb für den Einsatz in hochsensiblen Umgebungen empfohlen. Er läuft auf ARMv6- (ARM11), ARMv7- (Cortex A8, A9, A15) und x86-Kernen, kann also auf Entwicklerplatinen wie Beagleboards oder Odroid ausprobiert werden. Auf entsprechender Hardware lässt sich Linux in einer virtuellen Maschine auf Sel4 einrichten und nutzen, etwa mit Intels VT-x samt EPT. Die Virtualisierung auf ARMs A7- beziehungsweise A15-Kernen soll später implementiert werden.

Das australische Forschungszentrum Nicta demonstrierte den Einsatz des Microkernels unter anderem in Drohnen, die nunmehr nicht mehr von Hackern vom Himmel geholt werden können sollen. Auch der Einsatz in der zivilen Luftfahrt, in Navigationsgeräten, in Robotern oder in Automobilen ist angedacht.


eye home zur Startseite
Hello_World 31. Jul 2014

Ob ein Parameter null sein darf oder nicht ist Teil des Vertrags der betreffenden...

gadthrawn 31. Jul 2014

Sorry, aber das sehe ich anders. Ich kenne recht viel Code, auch aus...

frostbitten king 30. Jul 2014

Ok, ja das ist wohl wahr der Mischmasch ist in der Tat grauslich (ich kotz bei so nem...

Hello_World 30. Jul 2014

_Alle_ NP-vollständigen Probleme sind Entscheidungsprobleme, damit erklärst Du also...

Hello_World 29. Jul 2014

Linux verifizieren? *rofl*, das kann nur von jemandem kommen, der keine Ahnung hat, wovon...



Anzeige

Stellenmarkt
  1. azh Abrechnungs- und IT-Dienstleistungszentrum für Heilberufe GmbH, Aschheim Raum München
  2. KEB Automation KG, Barntrup
  3. Dentsply Sirona, The Dental Solutions Company, Bens­heim
  4. Uhlmann Pac-Systeme GmbH & Co. KG, Laupheim


Anzeige
Top-Angebote
  1. 279€
  2. 99,90€ + 4,99€ Versand (Vergleichspreis 128€)
  3. 190,01€

Folgen Sie uns
       


  1. Counter-Strike Go

    Bei Abschuss Ransomware

  2. Hacking

    Microsoft beschlagnahmt Fancy-Bear-Infrastruktur

  3. Die Woche im Video

    Strittige Standards, entzweite Bitcoins, eine Riesenkonsole

  4. Bundesverkehrsministerium

    Dobrindt finanziert weitere Projekte zum autonomen Fahren

  5. Mobile

    Razer soll Smartphone für Gamer planen

  6. Snail Games

    Dark and Light stürmt Steam

  7. IETF

    Netzwerker wollen Quic-Pakete tracken

  8. Surface Diagnostic Toolkit

    Surface-Tool kommt in den Windows Store

  9. Bürgermeister

    Telekom und Unitymedia verweigern Open-Access-FTTH

  10. Layton's Mystery Journey im Test

    Katrielle, fast ganz der Papa



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Gaming-Monitor Viewsonic XG 2530 im Test: 240 Hertz, an die man sich gewöhnen kann
Gaming-Monitor Viewsonic XG 2530 im Test
240 Hertz, an die man sich gewöhnen kann
  1. LG 43UD79-B LG bringt Monitor mit 42,5-Zoll-Panel für vier Signalquellen
  2. SW271 Benq bringt HDR-Display mit 10-Bit-Panel
  3. Gaming-Bildschirme Freesync-Displays von Iiyama und Viewsonic

Moto Z2 Play im Test: Bessere Kamera entschädigt nicht für kürzere Akkulaufzeit
Moto Z2 Play im Test
Bessere Kamera entschädigt nicht für kürzere Akkulaufzeit
  1. Modulares Smartphone Moto Z2 Play kostet mit Lautsprecher-Mod 520 Euro
  2. Lenovo Hochleistungs-Akku-Mod für Moto Z
  3. Moto Z Schiebetastatur-Mod hat Finanzierungsziel erreicht

Razer Lancehead im Test: Drahtlose Symmetrie mit Laser
Razer Lancehead im Test
Drahtlose Symmetrie mit Laser
  1. Razer Blade Stealth 13,3- statt 12,5-Zoll-Panel im gleichen Gehäuse
  2. Razer Core im Test Grafikbox + Ultrabook = Gaming-System
  3. Razer Lancehead Symmetrische 16.000-dpi-Maus läuft ohne Cloud-Zwang

  1. Re: 2,5k auf 27" sollten reichen... oder?

    Sicaine | 17:08

  2. Re: Unsere Steuergelder zur Generierung...

    madMatt | 17:02

  3. Re: Solange Porsche Autos teurer sind als...

    Berner Rösti | 17:02

  4. Re: E-Autos sind das falsche Produkt

    elektroroadster | 17:00

  5. Selbstbedienungsladen für Superreiche.

    madMatt | 16:58


  1. 12:43

  2. 11:54

  3. 09:02

  4. 16:55

  5. 16:33

  6. 16:10

  7. 15:56

  8. 15:21


  1. Themen
  2. A
  3. B
  4. C
  5. D
  6. E
  7. F
  8. G
  9. H
  10. I
  11. J
  12. K
  13. L
  14. M
  15. N
  16. O
  17. P
  18. Q
  19. R
  20. S
  21. T
  22. U
  23. V
  24. W
  25. X
  26. Y
  27. Z
  28. #
 
    •  / 
    Zum Artikel