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. Ingenieur (m/w) Informationstechnik
    Netze BW GmbH, Stuttgart
  2. SAP Business Process Expert (m/w)
    Brüel & Kjaer Vibro GmbH, Darmstadt
  3. IT-Projektleiter/in (SAP)
    Landeshauptstadt München, München
  4. Consultant Software Asset Management (SAM) für Microsoft (m/w)
    FRITZ & MACZIOL group, deutschlandweit

 

Detailsuche


Folgen Sie uns
       


  1. Gratiseinwilligung für Google

    Verlage knicken beim Leistungsschutzrecht ein

  2. John Riccitiello

    Ex-EA-Chef ist neuer Boss von Unity Technologies

  3. Android Wear

    Moto 360 und G Watch erhalten Update

  4. Digitale Dividende II

    Bundesnetzagentur will DVB-T ab April 2015 beenden

  5. Security

    Gefährliche Schwachstellen im UEFI-Bios

  6. Broadcom

    Chips für Router mit G.Fast sind fertig

  7. Canon Filmkamera

    EOS C100 Mark II mit Dual-Pixel-AF und besserem Sucher

  8. Samsung

    Galaxy-Geräte mit Knox für US-Regierung zertifiziert

  9. Sammelkarten

    Hearthstone erst 2015 auf Smartphones

  10. Netzangriffe

    DDoS-Botnetz weitet sich ungebremst aus



Haben wir etwas übersehen?

E-Mail an news@golem.de



Sony Alpha 7S im Test: Vollformater sieht auch bei Dunkelheit nicht schwarz
Sony Alpha 7S im Test
Vollformater sieht auch bei Dunkelheit nicht schwarz
  1. FPS 1000 Kamera soll 18.500 Frames pro Sekunde aufnehmen
  2. Bericht Sony will 4K-Superzoom-Kamera entwickeln
  3. Minikamera Ai-Ball Die WLAN-Kamera aus dem Überraschungsei

IT-Gipfel 2014: De Maizière nennt De-Mail "nicht ganz zufriedenstellend"
IT-Gipfel 2014
De Maizière nennt De-Mail "nicht ganz zufriedenstellend"
  1. Digitale Verwaltung 2020 E-Mail soll Briefe und Amtsbesuche ersetzen
  2. Digitale Agenda Ein Papier, das alle enttäuscht
  3. Webmail Web.de kritisiert langsame De-Mail-Einführung der Regierung

Retro-Netzwerk: Der Tilde.Club erstellt Webseiten wie in den Neunzigern
Retro-Netzwerk
Der Tilde.Club erstellt Webseiten wie in den Neunzigern

    •  / 
    Zum Artikel