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. Software-Ingenieure (m/w) für Java-Technologien
    Zühlke Engineering GmbH, Hamburg, Hannover
  2. Anwendungs- / Softwareberater (m/w) für SAP PLM
    MAHLE International GmbH, Stuttgart
  3. Anwendungsentwickler (m/w)
    SCHOTT AG, Mainz
  4. IT-Projektleiter (m/w) in der Softwareentwicklung
    ADAC e.V., München

 

Detailsuche


Folgen Sie uns
       


  1. Soziale Netzwerke

    Offline-Freund bleibt wichtiger als Online-Freund

  2. Internet-Partei

    Kim Dotcom scheitert bei Wahl in Neuseeland

  3. SpaceX

    Privater Raumfrachter Dragon zur ISS gestartet

  4. NSA-Affäre

    Staatsanwaltschaft ermittelt nach Cyberangriff auf Stellar

  5. HP Elitepad 1000 G2 im Test

    Praktisches Arbeitsgerät dank Zubehör

  6. Spiele-API

    DirectX-11 wird parallel zu DirectX-12 weiterentwickelt

  7. Streaming-Box

    Netflix noch im Herbst für Amazons Fire TV

  8. Schnell, aber ungenau

    Roboter springt im Explosionsschritt

  9. Urteil

    Foxconn-Arbeiter wegen iPhone-6-Diebstahl verhaftet

  10. Weniger Consumer-Notebooks

    Toshiba baut 900 Arbeitsplätze in der PC-Sparte ab



Haben wir etwas übersehen?

E-Mail an news@golem.de



Streaming-Box im Kurztest: Fire TV läuft jetzt mit deutschen Amazon-Konten
Streaming-Box im Kurztest
Fire TV läuft jetzt mit deutschen Amazon-Konten
  1. Buchpreisbindung Buchhandel erzwingt höheren Preis bei Amazon
  2. Amazon-Tablet Neues Fire HD mit 6 Zoll für 100 Euro
  3. Online-Handel Bei externen Händlern mit Amazon-Konto einkaufen

Imsi-Catcher: Catch me if you can
Imsi-Catcher
Catch me if you can
  1. Spy Files 4 Wikileaks veröffentlicht Spionagesoftware von Finfisher
  2. Spiegel-Bericht BND hört Nato-Partner Türkei und US-Außenminister ab
  3. Bundestrojaner Software zu Online-Durchsuchung einsatzbereit

Test Hyrule Warriors: Gedrücke und Gestöhne mit Zelda
Test Hyrule Warriors
Gedrücke und Gestöhne mit Zelda
  1. Mario Kart 8 Rennen mit Link und Prinzessin Peach
  2. Nintendo Streit um Smartphone-Spiele und das Internet

    •  / 
    Zum Artikel