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. Datenmanager / Analyst (m/w)
    RATIONAL AG, Landsberg am Lech
  2. Leiterin / Leiter des Fachbereichs Standard-Arbeitsplatz Service
    ITDZ Berlin, Berlin
  3. Softwareentwickler / Softwareentwicklerin Java Produktkonfigurator
    CAS Software AG, Karlsruhe
  4. IT Manager (m/w)
    Kavlico GmbH, Minden

 

Detailsuche


Folgen Sie uns
       


  1. Sony

    Smartwatch mit Armband aus E-Paper geplant

  2. Samsung SDC

    Displays werden bunter, biegsamer und fast durchsichtig

  3. Mozilla

    Ein-Klick-Suche im Firefox

  4. EU-Richtlinien beschlossen

    Recht auf Vergessen soll weltweit gelten

  5. Rekord

    Apple kommt Börsenwert von einer Billion US-Dollar näher

  6. Systemd und Launchd

    FreeBSD-Gründer sieht Notwendigkeit für modernes Init-System

  7. Internet und Energie

    EU will 315 Milliarden Euro für Netze mobilisieren

  8. Mobile Bürosuite

    Dropbox mit Microsoft-Office-Anschluss

  9. High Bandwith Memory

    SK Hynix liefert schnelleren Grafikkartenspeicher aus

  10. Streaming

    Wuaki lockt mit 4K-Filmen für Smart-TVs



Haben wir etwas übersehen?

E-Mail an news@golem.de



Next-Gen-Geburtstag: Xbox One und Playstation 4 sind eins
Next-Gen-Geburtstag
Xbox One und Playstation 4 sind eins
  1. Big Fish Games Bis zu 885 Millionen US-Dollar für Casualgames-Anbieter
  2. This War of Mine Das traurigste Spiel des Jahres
  3. Qbert & Co 901 Spielhallenklassiker im Onlinearchiv

NSA-Ausschuss: Meisterschule für Geheimniskrämer
NSA-Ausschuss
Meisterschule für Geheimniskrämer
  1. Kanzlerhandy Bundesanwaltschaft will NSA-Ermittlungsverfahren einstellen
  2. NSA und Co. US-Geheimdienste melden viele Zero-Day-Lücken vertraulich
  3. IT-Sicherheitsgesetz BSI soll Sicherheitslücken nicht geheim halten

Panasonic Lumix DMC-LX100 im Test: Kamera zum Begeistern und zum Verzweifeln
Panasonic Lumix DMC-LX100 im Test
Kamera zum Begeistern und zum Verzweifeln
  1. Systemkamera Sony Alpha 7 II mit 5-Achsen-Bildstabilisierung
  2. Canon PowerShot G7 X im Test Canons Konkurrenz zu Sonys 1-Zoll-Kamera
  3. Interne Dokumente Neuer Sony-Sensor könnte Kameras kraftvoller machen

    •  / 
    Zum Artikel