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. Technischer Leiter (m/w)
    wenglor sensoric gmbh, Tettnang
  2. IT-Senior Consultant CRM (m/w)
    Media-Saturn IT Services GmbH, Ingolstadt
  3. Softwareentwickler (m/w)
    ZF Friedrichshafen AG, Passau
  4. IT-Teamleitungen (m/w) für Betreute Lokale Netze an beruflichen Schulen
    Landeshauptstadt München, München

 

Detailsuche


Folgen Sie uns
       


  1. Verbraucherzentrale

    Auf Schreiben wegen Rundfunkbeitrag reagieren

  2. Filmstreaming

    Erste Preise für Netflix Deutschland sichtbar

  3. Alone in the Dark

    Atari setzt auf doppelten Horror

  4. LMDE

    Linux Mint wechselt zu Debian Stable neben Ubuntu

  5. Preisvergleich

    Ergebnisse in Preissuchmaschinen nicht zuverlässig

  6. Akoya P2213T

    Medion stellt Windows-Convertible für 400 Euro vor

  7. Hacker

    Lizard Squad offenbar verhaftet

  8. Lennart Poettering

    Systemd und Btrfs statt Linux-Distributionen mit Paketen

  9. Dircrypt

    Ransomware liefert Schlüssel mit

  10. Wegen Computerabstürzen

    Nasa will Speicher eines Marsroboters neu formatieren



Haben wir etwas übersehen?

E-Mail an news@golem.de



Qnap QGenie im Test: Netzwerkspeicher fehlt's an Speicher
Qnap QGenie im Test
Netzwerkspeicher fehlt's an Speicher
  1. Qnap QGenie NAS-System für die Hosentasche
  2. HS-251 Qnap beschleunigt lüfterloses NAS-System
  3. QNAP TS-EC1080 Pro Erweiterbares NAS-System im Tower mit mSATA-Plätzen

Kinkobox angeschaut: E-Mail-Verschlüsselung leicht gemacht
Kinkobox angeschaut
E-Mail-Verschlüsselung leicht gemacht
  1. IT-Sicherheitsgesetz Telekomfirmen müssen Nutzer über Cyberangriffe informieren
  2. IT-Sicherheitsgesetz Unternehmen dürfen ungefährliche Angriffe anonym melden
  3. Cryptophone Telekom mit Ende-zu-Ende-Verschlüsselung für Smartphones

Neues Instrument Holometer: Ist unser Universum zweidimensional?
Neues Instrument Holometer
Ist unser Universum zweidimensional?
  1. Gehirnforschung Licht programmiert Gedächtnis um
  2. Audio aus Video Gefilmte Topfpflanze verrät Gespräche
  3. Nahrungsmittel Trinken statt Essen

    •  / 
    Zum Artikel