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. Entwicklungsingenieur/-in Funktionale Sicherheit Fahrerassistenzsysteme
    Daimler AG, Immendingen
  2. Informatikerin / Informatiker / Bauinformatikerin / Bauinformatiker für zentrales Daten- und Prozessmanagement
    Ed. Züblin AG, Stuttgart
  3. Software Projektleitung (m/w)
    Daimler AG, Kirchheim
  4. Produktmanager (m/w) Netzwerksicherheit
    ROHDE & SCHWARZ SIT GmbH, Berlin

 

Detailsuche


Hardware-Angebote
  1. PCGH-Extreme-PC GTX980Ti-Edition
    (Core i7-5820K + Geforce GTX 980 Ti)
  2. Marshall STANMOREBLACK stanmore Bluetooth-Lautsprecher
    285,00€ statt 329,00€
  3. Samsung-UHDTV kaufen und Sommer-Bonus erhalten
    100,00€ bis 1.000,00€ Cashback

 

Weitere Angebote


Folgen Sie uns
       


  1. Sony

    Schwarze Zahlen dank Playstation 4 und Fotosensoren

  2. Rocket League im Test

    Fantastische Tore mit der Heckklappe

  3. Neuer Windows Store

    Windows 10 erlaubt deutlich weniger Parallelinstallationen

  4. Schwache Mobilsparte

    Samsung plant Preisreduzierung der Galaxy-S6-Modelle

  5. Angry Birds 2

    Vogelauswahl im Schweinekampf

  6. Windows 10 im Tablet-Test

    Ein sinnvolles Windows für Tablets

  7. Elon Musk

    Tesla-Fahrer sollen neue Tesla-Fahrer werben

  8. Minecraft

    Beta mit nutzbarer Zweithand

  9. Schwachstelle

    MKV-Dateien können Android einfrieren

  10. National Strategic Computing Initiative

    Präsident Obama fordert den Exascale-Supercomputer



Haben wir etwas übersehen?

E-Mail an news@golem.de



Neue WLAN-Router-Generation: Hohe Bandbreiten mit zweifelhaftem Nutzen
Neue WLAN-Router-Generation
Hohe Bandbreiten mit zweifelhaftem Nutzen
  1. EA8500 Linksys' MU-MIMO-Router kostet 300 Euro
  2. Aruba Networks 802.11ac-Access-Points mit integrierten Bluetooth Beacons
  3. 802.11ac Wave 2 Neue Chipsätze für die zweite Welle von ac-WLAN

Simulus QR-X350.PRO im Test: Der Quadcopter, der vom Himmel fiel
Simulus QR-X350.PRO im Test
Der Quadcopter, der vom Himmel fiel
  1. Flugverkehrskontrolle Amazon will Drohnenverkehr regeln
  2. Paketzustellung Google will Flugverkehrskontrolle für Drohnen entwickeln
  3. Luftzwischenfall Beinahekollision zwischen Lufthansa-Flugzeug und Drohne

OCZ Trion 100 im Test: Macht sie günstiger!
OCZ Trion 100 im Test
Macht sie günstiger!
  1. PM863 Samsung packt knapp 4 TByte in ein flaches Gehäuse
  2. 850 Evo und Pro Samsung veröffentlicht erste Consumer-SSDs mit 2 TByte
  3. TLC-Flash Samsung plant SSDs mit 2 und 4 TByte

  1. Re: Mit Windows 10.1 werden's dann 101

    pod4711 | 16:06

  2. Re: warum überhaupt den Store benutzen?

    Manga | 16:06

  3. Re: SD-Karte raus...

    FreiGeistler | 16:05

  4. Re: Man sollte oefter Sony kaufen

    Tzven | 16:05

  5. Re: Es gibt zu viele Idioten in diesem Land

    DY | 16:04


  1. 14:58

  2. 14:44

  3. 13:07

  4. 12:48

  5. 12:11

  6. 12:05

  7. 11:57

  8. 11:02


  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