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 Software Engineer iOS (m/w)
    hmmh multimediahaus AG, Bremen
  2. Fachinformatiker/in für Systemintegration
    netzorange IT-Dienstleistungen GmbH & Co. KG, Köln-Mülheim
  3. SAP BI Inhouse Projektmanager (m/w)
    über Jobware Personalberatung, Braunschweig
  4. Wissenschaftliche Mitarbeiterin / Wissenschaftlicher Mitarbeiter am Lehrstuhl für Informatik
    Universität Passau, Passau

 

Detailsuche


Blu-ray-Angebote
  1. NEU: One - Leben am Limit [Blu-ray]
    7,97€
  2. NEU: True Blood - Die komplette sechste Staffel [Blu-ray]
    22,97€ FSK 18
  3. TIEFPREIS: Jurassic Park - Steelbook [Blu-ray] [Limited Edition]
    9,90€

 

Weitere Angebote


Folgen Sie uns
       


  1. Übernahme

    SAP wollte Salesforce für 37 Milliarden US-Dollar kaufen

  2. Router-Hersteller

    Cisco bekommt einen neuen Chef

  3. Nicht mehr pleite

    Dotcom erhält 115.000 Dollar für monatliche Ausgaben

  4. Head-mounted Smartphone

    Einige neue Apps laufen nicht auf dem älteren Gear VR

  5. Microsofts Konferenzsystem

    Was Entwickler beim Surface Hub beachten müssen

  6. Sky-Engine

    Dart könnte Android-Apps deutlich beschleunigen

  7. Verschlüsselung

    Mozillas HTTP-Abschied wird konkreter

  8. Windows 10 IoT Core angetestet

    Windows auf dem Raspberry Pi 2

  9. Taxi-App

    Mytaxi gewährt 50 Prozent Rabatt auf Taxifahrten

  10. Drohnen

    Airmap zeigt, wo Drohnen fliegen dürfen



Haben wir etwas übersehen?

E-Mail an news@golem.de



Schöpfung 2.0: Bis zum Designerbaby ist es nicht mehr weit
Schöpfung 2.0
Bis zum Designerbaby ist es nicht mehr weit
  1. Luftfahrt Nasa testet verformbare Tragflächen
  2. Vorbild Tintenfisch Tarnmaterial ändert seine Farbe
  3. Keine Science-Fiction Mit dem Laser gegen Weltraumschrott

Voiceprint: Stimmenerkennung ist die neue Gesichtserkennung
Voiceprint
Stimmenerkennung ist die neue Gesichtserkennung
  1. Unsicheres Plugin Googles Passwort-Warnung lässt sich leicht aushebeln
  2. Security Die Makroviren kehren zurück
  3. Android Tausende Apps akzeptieren gefälschte Zertifikate

The Ocean Cleanup: Ein Müllfänger für die Meere
The Ocean Cleanup
Ein Müllfänger für die Meere
  1. Maglev Magnetschwebebahn erreicht in Japan 590 km/h
  2. NailO Künstlicher Fingernagel als Maussteuerung
  3. 3D-Scanner Mini-Bildsensor erzeugt 3D-Bilder mit Lidar

  1. Re: OT: Frage zu URL HTTPS allgemein

    ikhaya | 19:02

  2. Re: GUI-Entwicklung einfacher?

    Astorek | 19:02

  3. Re: 1000 Dollar

    thesmann | 18:59

  4. Re: Zwei Klassen Rechtssystem.

    Moe479 | 18:55

  5. Re: Als junger, aufstrebener Programmierer würde...

    Tzven | 18:50


  1. 18:12

  2. 16:53

  3. 16:08

  4. 15:50

  5. 15:17

  6. 13:30

  7. 12:45

  8. 12:03


  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