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. Junior Systemingenieur/in oder Techniker/in für die Weiterentwicklung vernetzter Infotainmentfunktionen
    ESG Elektroniksystem- und Logistik-GmbH, Ingolstadt
  2. Software Verification Engineer (FSW Testing) (m/w)
    Magna Powertrain, Lannach (Österreich)
  3. Softwareentwickler für modellbasierte Entwicklung und Embedded Systeme (m/w)
    MBtech Group GmbH & Co. KGaA, Mannheim, Sindelfingen bei Stuttgart, Ulm/Neu-Ulm, Rüsselsheim (Home-Office möglich)
  4. Softwareentwickler (m/w)
    FVA GmbH über generic.de software technologies AG, München

 

Detailsuche


Blu-ray-Angebote
  1. VORBESTELLBAR: Der Tatortreiniger - Böse Dose (limitierte Sonderedition) [3 BDs & 1 DVD] Folge 1-18 [Blu-ray]
    59,95€ (Vorbesteller-Preisgarantie) - Release 13.03.
  2. Game of Thrones - Die komplette 4. Staffel [Blu-ray]
    38,99€
  3. X-Men Zukunft ist Vergangenheit [Blu-ray]
    12,90€

 

Weitere Angebote


Folgen Sie uns
       


  1. VLC-Hauptentwickler

    "Appstores machen Kopfschmerzen"

  2. Torrent

    The Pirate Bay ist zurück - zumindest ein bisschen

  3. Freier Videocodec

    Daala muss Technik patentieren

  4. Android-Konsole

    Alibaba investiert zehn Millionen US-Dollar in Ouya

  5. Andrea Voßhoff

    Datenschutzbeauftragte jetzt gegen Vorratsdatenspeicherung

  6. Breitbandausbau

    "Wer Bauland will, fragt heute erst nach schnellem Internet"

  7. Dying Light

    Performance-Patch reduziert Sichtweite

  8. Project Tango

    Googles 3D-Sensor-Konzept verlässt Experimentierstatus

  9. Messenger

    Telefoniefunktion für Whatsapp erreicht erste Nutzer

  10. iTunes Connect

    Hallo, fremdes Benutzerkonto



Haben wir etwas übersehen?

E-Mail an news@golem.de



Fehlender Cache verursacht Ruckler: Nvidias beschnittene Geforce GTX 970 stottert messbar
Fehlender Cache verursacht Ruckler
Nvidias beschnittene Geforce GTX 970 stottert messbar
  1. IMHO Juhu, DirectX 12 gibt's auch für Windows-7-Besitzer
  2. Geforce GTX 965M Sparsamere Alternative zur GTX 870M
  3. MFAA Nvidias temporale Kantenglättung kann mehr

Glibc: Ein Geist gefährdet Linux-Systeme
Glibc
Ein Geist gefährdet Linux-Systeme
  1. Tamil Driver Freier Treiber für ARMs Mali-T-GPUs entsteht
  2. Red Star ausprobiert Das Linux aus Nordkorea
  3. Linux-Jahresrückblick 2014 Umbauarbeiten, Gezanke und Container

Onlinehandel: Welche Versand-Flatrates sich nicht lohnen
Onlinehandel
Welche Versand-Flatrates sich nicht lohnen
  1. Quartalsbericht Amazons Ausgaben steigen auf 28,7 Milliarden US-Dollar
  2. Amazon Original Movies Amazon will eigene Kinofilme kurz nach der Premiere streamen
  3. Ultra-HD Amazons 4K-Videos vorerst nur für Smart-TVs

    •  / 
    Zum Artikel