Automatischer Sicherheitsnachweis für Betriebssystemkern

Forscher entwickeln Methode, um Fehlerfreiheit nachzuweisen

Am australischen Forschungsinstitut Nicta haben Mitarbeiter ein Verfahren entwickelt, um die Sicherheit von Programmcode zu beweisen. Die Methode basiert auf mathematischen Berechnungen. Die Forscher haben ihre Methode am Mikrokernel "Secure Embedded L4" erprobt.

Anzeige

Mit ihrem Verfahren wollen die Forscher des Nicta die Sicherheit von Programmcode nachweisen. Die mathematischen Berechnungen sollen verschiedene Fehlerklassen wie Pufferüberläufe ausschließen können. Somit lasse sich beweisen, dass eine Anwendung für kritische Einsatzgebiete wie in Flugzeugen und Autos geeignet sei.

Ausgetestet wurde die Methode am Secure-Embedded-L4-Mikrokernel (seL4). Während frühere Tests nur einzelne Bereiche unter die Lupe nahmen, gelang so der Nachweis über die Korrektheit des kompletten, 7.500 Zeilen langen C-Codes. Die Prüfung erfolgt automatisiert mit einer Software. So soll der seL4 immun gegen gängige Angriffe sein. Pufferüberläufe beispielsweise seien nicht möglich. Mittels der mathematischen Berechnungen sollen sich auch Speicherlecks, Zeigerfehler und weitere Probleme wie arithmetische Überlaufe ausschließen lassen.

Die vom Nicta neu entwickelten Techniken sollen bald an die am Nicta entstandene Firma Open Kernel Labs weitergereicht werden. Die Open Kernel Labs wollen dann ein Produkt auf Basis der mathematischen Methoden entwickeln.

Eine wissenschaftliche Publikation über die Technik soll zum 22. ACM Symposium on Operating Systems Principles im Oktober vorgestellt werden.


Siga9876 20. Aug 2009

Wenn ich es nicht beweisen kann, darf ich es bei Banken usw. nicht einsetzen. Wäre mal...

Name 20. Aug 2009

Genau den Punkt meinte ich. Eine Zahl ist eine Zahl und der Algorithmus wird wohl nicht...

Name 20. Aug 2009

Wenn Du Pech hast, dann hast Du jetzt eine Patentklage am Hals;-)

Siga9876 20. Aug 2009

Vom Doppelposting bitte eines Löschen. polipo hängt schon mal :-( Danke und Sorry.

DerAkademiker 20. Aug 2009

LISA ist jetzt aber der Roboter an der Uni-Koblenz der im RoboCafe Cola, Fanta und Saft...

Kommentieren



Anzeige

  1. Senior Softwaredeveloper Java (m/w)
    NEXMO solutions GmbH & Co. KG, Hamburg
  2. CMS-Architekt (m/w) mit dem Schwerpunkt Enterprise Web-CMS
    adesso AG, Berlin, Dortmund, Stuttgart
  3. Softwareentwickler (m/w)
    MAHA Maschinenbau Haldenwang GmbH & Co. KG, Haldenwang
  4. IT Account Manager (m/w)
    European Space Agency (ESA), Noordwijk (Netherlands)

 

Detailsuche


Spiele-Angebote
  1. TOPSELLER: Titanfall Origin-Code
    9,99€
  2. FINAL FANTASY X/X-2 HD Remaster PS4
    49,99€ - Release 15.05.
  3. Cities: Skylines [PC/Mac Steam Code]
    27,99€

 

Weitere Angebote


Folgen Sie uns
       


  1. Gigaset

    Ex-Siemens-Sparte bringt eigene Smartphones heraus

  2. Legacy of the Void

    Starcraft 2 geht in die Beta

  3. Streaming

    Fernbedienungen bekommen Netflix-Taste

  4. DNS/AXFR

    Nameserver verraten Geheim-URLs

  5. Lizenzklage

    "VMware wollte sich nicht an die GPL halten"

  6. Kabelnetzbetreiber

    Routerwahl soll zu Bruch des Fernmeldegeheimnisses führen

  7. Ineffiziente Leuchtmittel

    Erweitertes Lampenverbot tritt in Kraft

  8. Mini-PCs unter Linux

    Installation schwer gemacht

  9. Game Development

    Golem.de lädt zum Tech Summit ein

  10. Khronos Group

    Grafik-API Vulkan erscheint für die Playstation 4



Haben wir etwas übersehen?

E-Mail an news@golem.de



HTC One (M9) im Test: Endlich eine gute Kamera
HTC One (M9) im Test
Endlich eine gute Kamera
  1. Lollipop Erstes HTC-One-Smartphone erhält kein Android 5.1

Mini-Business-Rechner im Test: Erweiterbar, sparsam und trotzdem schön klein
Mini-Business-Rechner im Test
Erweiterbar, sparsam und trotzdem schön klein
  1. Shuttle DS57U Passiver Mini-PC mit Broadwell und zwei seriellen Com-Ports
  2. Broadwell-Mini-PC Gigabytes Brix ist noch kompakter als Intels NUC
  3. Mouse Box Ein Mini-PC in der Maus

Jugendliche und soziale Netzwerke: Geh sterben, Facebook!
Jugendliche und soziale Netzwerke
Geh sterben, Facebook!
  1. Nuclide Facebook stellt quelloffene IDE vor
  2. 360-Grad-Videos und neuer Messenger Facebook zeigt seinen Nutzern Rundumvideos
  3. Urheberrecht Bild-Fotograf zieht Abmahnung zum Facebook-Button zurück

  1. Re: Wenn man meckert kriegt man ein Modem.

    Tuxraxer007 | 08:26

  2. Re: Router ungleich Modem

    patrickrocker83 | 08:24

  3. Re: Ungelernte Paketknechte ...

    dreamtide11 | 08:19

  4. Re: Typisch bei der Firmenpolitik

    Psy2063 | 08:12

  5. Re: wenn die jetzt schlau wären...

    KönigSchmadke | 08:10


  1. 19:04

  2. 17:03

  3. 16:09

  4. 15:47

  5. 15:02

  6. 13:23

  7. 13:13

  8. 12:00


  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