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. IT-Programmmanager/-in für komplexe Softwareeinführungsprojekte
    Dataport, Hamburg
  2. Business Intelligence Analyst Logistik (m/w)
    Home Shopping Europe GmbH, Ismaning (Raum München)
  3. Softwareentwickler (m/w)
    SEW-EURODRIVE GmbH & Co KG, Bruchsal
  4. Senior BI Solutions Architekt (m/w)
    SolarWorld AG, Bonn

 

Detailsuche


Folgen Sie uns
       


  1. Spähaffäre

    Snowden erklärt seine Frage an Putin

  2. CSA-Verträge

    Microsoft senkt Preise für Support von Windows XP

  3. Test Wyse Cloud Connect

    Dells mobiles Büro

  4. Globalfoundries-Kooperation mit Samsung

    AMDs Konsolengeschäft kompensiert schwache CPU-Sparte

  5. Verband

    "Uber-Verbot ruiniert Ruf der Startup-Stadt Berlin"

  6. Kabel Deutschland

    2.000 Haushalte zwei Tage von Kabelschaden betroffen

  7. Cridex-Trojaner

    Hamburger Senat bestätigt großen Schaden durch Malware

  8. Ubuntu 14.04 LTS im Test

    Canonical in der Konvergenz-Falle

  9. Überwachung

    Snowden befragt Putin in Fernsehinterview

  10. Bleichenbacher-Angriff

    TLS-Probleme in Java



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Test LG L40: Android 4.4.2 macht müde Smartphones munter
Test LG L40
Android 4.4.2 macht müde Smartphones munter

Mit dem L40 präsentiert LG eines der ersten Smartphones mit der aktuellen Android-Version 4.4.2, das unter 100 Euro kostet. Dank der Optimierungen von Kitkat überrascht die Leistung des kleinen Gerätes - und es dürfte nicht nur für Einsteiger interessant sein.

  1. LG G3 5,5-Zoll-Smartphone mit 1440p-Display und Kitkat
  2. LG L35 Smartphone mit Android 4.4 für 80 Euro
  3. Programmierbare LED-Lampe LG kündigt Alternative zur Philips Hue an

Vorratsdatenspeicherung: Totgesagte speichern länger
Vorratsdatenspeicherung
Totgesagte speichern länger

Die Interpretationen des EuGH-Urteils zur Vorratsdatenspeicherung gehen weit auseinander. Für einen endgültigen Abgesang auf die anlasslose Speicherung von Kommunikationsdaten ist es aber noch zu früh.

  1. Bundesregierung Vorerst kein neues Gesetz zur Vorratsdatenspeicherung
  2. Innenministertreffen Keine schnelle Neuregelung zur Vorratsdatenspeicherung
  3. Urteil zu Vorratsdatenspeicherung Regierung uneins über neues Gesetz

Windows 8.1 Update 1 im Test: Ein lohnenswertes Miniupdate
Windows 8.1 Update 1 im Test
Ein lohnenswertes Miniupdate

Microsoft geht wieder einen Schritt zurück in die Zukunft. Mit dem Update 1 baut der Konzern erneut Funktionen ein, die vor allem für Mausschubser gedacht sind. Wir haben uns das Miniupdate für Windows 8.1 pünktlich zur Veröffentlichung angesehen.

  1. Microsoft Installationsprobleme beim Windows 8.1 Update 1
  2. Windows 8.1 Update 1 Wieder mehr minimieren und schließen
  3. Microsoft Windows 8.1 Update 1 vorab verfügbar

    •  / 
    Zum Artikel