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. Systemingenieur (m/w) für Netzwerktechnik
    DIEHL Informatik GmbH, Nürnberg
  2. IT-Service Mitarbeiter (m/w)
    DATAGROUP Köln GmbH, München
  3. IT Support Engineer Windows / Citrix (m/w)
    PIRONET NDH Datacenter AG & Co. KG, Köln
  4. Mitarbeiter (m/w) im Prozess- und Stammdatenmanagement
    UVEX WINTER HOLDING GmbH & Co. KG, Fürth

 

Detailsuche


Blu-ray-Angebote
  1. 3 3D-Blu-rays für 15 EUR
    (u. a. Dead Before Dawn, Neuseeland 3D, Abenteuer Karibik 3D)
  2. 3D-Blu-rays zum Aktionspreis
    (u. a. Hobbit 1+2 je 14,97€, Gravity 14,97€, Pacific Rim 12,99€, Der große Gatsby 12,99€)
  3. NEU: Batman - 25th Anniversary [Blu-ray]
    7,97€

 

Weitere Angebote


Folgen Sie uns
       


  1. CIA-Dokumente

    Wie man als Spion durch Flughafenkontrollen kommt

  2. Game Over

    Kein Game One mehr auf MTV

  3. Z1

    Samsung veröffentlicht endlich sein Tizen-Smartphone

  4. Zehn Jahre Entwicklung

    Network Manager 1.0 ist erschienen

  5. Star Citizen

    Galaktisches Update mit Lobby, Raketen und Cockpits

  6. Smrtgrips

    Die intelligenten Griffe fürs Fahrrad

  7. Messenger

    Whatsapp richtet Spam-Sperre ein

  8. Sony-Hack

    Die dubiose IP-Spur nach Nordkorea

  9. FreeBSD-Entwickler

    Linux-Foundation sponsert NTPD-Alternative

  10. Telefonabzocke

    Kaum weniger Beschwerden trotz hoher Bußgelder



Haben wir etwas übersehen?

E-Mail an news@golem.de



Circuitscribe ausprobiert: Stromkreise malen für Teenies
Circuitscribe ausprobiert
Stromkreise malen für Teenies
  1. Arduino Mit der Kraft der zwei Herzen
  2. Per FPGA Hardwarebasierter Zork-Interpreter
  3. Spark Photon Kleines und günstiges ARM-Board mit WLAN

Lehrreiche Geschenke: Stille Nacht, Bastelnacht
Lehrreiche Geschenke
Stille Nacht, Bastelnacht
  1. Arduino Vorgehen gegen unlizenzierte Nachahmer
  2. Arduino Neue Details zum 3D-Drucker Materia 101
  3. Microduino Kleine Bastlerboards zum Stapeln

Core M-5Y10 im Test: Kleiner Core M fast wie ein Großer
Core M-5Y10 im Test
Kleiner Core M fast wie ein Großer
  1. Hands on Asus Transformer Book T300FA Das günstigste Detachable mit Core M
  2. Benchmark Apple und Nvidia schlagen manchmal Intels Core M
  3. Core M-5Y70 im Test Vom Turbo zur Vollbremsung

    •  / 
    Zum Artikel