Forum für Wissenschaft, Industrie und Wirtschaft

Hauptsponsoren:     3M 
Datenbankrecherche:

 

Sicherheits-Beweis für Betriebssystem-Kernel

17.08.2009
Forscher melden mathematischen Nachweis für fehlerfreien Code

Forscher am australischen IKT-Forschungsinstitut NICTA haben nach eigenen Angaben den weltweit ersten formellen maschinell geprüften Beweis dafür geliefert, dass ein Betriebssystem-Kernel frei von vielen gängigen Fehlern ist.

Dabei wurden 7.500 Zeilen C-Quellcode geprüft. Der so verifizierte Mikrokernel "Secure Embedded L4" (seL4) könnte den Wissenschaftlern zufolge in diversen sicherheitskritischen Embedded-Anwendungen zum Einsatz kommen. "Die Prüfung bietet einen schlüssigen Nachweis, dass fehlerfreie Software möglich ist. Weniger als das sollte in Zukunft in kritischen Bereichen nicht akzeptabel sein", meint Gernot Heiser, CTO bei Open Kernel (OK) Labs, einem Spezialisten für Virtualisierungslösungen im Embedded-Bereich. Dieser will ein Produkt realisieren, dem ein derart geprüfter Kernel zugrunde liegt.

Es habe bereits formale Prüfungen einzelner Eigenschaften von kleineren Kernels gegeben, heißt es am NICTA. "Was wir gemacht haben ist aber ein allgemeiner Beweis der funktionellen Fehlerfreiheit, was nie zuvor für reale, hochleistungsfähige Software dieser Komplexität oder Größe gelungen ist", meint Gerwin Klein, Forschungsleiter des NICTA-Teams. Mithilfe eines Computerprogramms wurden 7.500 Code-Zeilen geprüft und in mehr als 200.000 Zeilen formelle Beweise für über 10.000 Theoreme erbracht. Damit wurde gezeigt, dass der Quellcode korrekt gestaltet ist, was hohe Zuverlässigkeit und Sicherheit verspricht. Dem NICTA zufolge wurde nachgewiesen, dass seL4 immun gegen sogenannte Buffer Overflows ist, die Hackern das Einschleusen von Schadcode ermöglichen. OK Labs zufolge können unter anderem auch Zeigerfehler sowie Speicherlecks und -überläufe ausgeschlossen werden.

Das NICTA betont, dass sich nun die Möglichkeit zum mathematischen Nachweis eröffne, dass kritische Software beispielsweise in Sicherheitssystemen in Flugzeugen oder Autos weitgehend fehlerfrei ist, bevor das Verkehrsmittel zum Einsatz kommt. Der seL4-Kernel selbst habe Anwendungspotenzial unter anderem in der Verteidigungsindustrie. Der NICTA-Kernel ist nur ein Vertreter der Mikrokernel-Familie L4 http://www.l4hq.org , die auf den 2001 verstorbenen deutschen Informatiker Jochen Liedtke zurückgeht. Ein L4-Kernel liegt auch OKL4 zugrunde, einer kommerziellen mobilen Virtualisierungsplattform von OK Labs. Als enger Partner des NICTA will OK Labs die Methode des Forschungsinstituts nun nutzen, eine vergleichbare Prüfung für OKL4 durchzuführen. In weiterer Folge soll ein vollständig verifiziertes kommerzielles Produkt entstehen.

Thomas Pichler | pressetext.austria
Weitere Informationen:
http://nicta.com.au
http://www.ok-labs.com

Weitere Nachrichten aus der Kategorie Informationstechnologie:

nachricht Warnsystem KATWARN startet international vernetzten Betrieb
27.06.2017 | FOKUS - Fraunhofer-Institut für Offene Kommunikationssysteme

nachricht Überschwemmungen genau in den Blick nehmen
27.06.2017 | Technische Universität Chemnitz

Alle Nachrichten aus der Kategorie: Informationstechnologie >>>

Die aktuellsten Pressemeldungen zum Suchbegriff Innovation >>>

Die letzten 5 Focus-News des innovations-reports im Überblick:

Im Focus: Schnelles und umweltschonendes Laserstrukturieren von Werkzeugen zur Folienherstellung

Kosteneffizienz und hohe Produktivität ohne dabei die Umwelt zu belasten: Im EU-Projekt »PoLaRoll« entwickelt das Fraunhofer-Institut für Produktionstechnologie IPT aus Aachen gemeinsam mit dem Oberhausener Fraunhofer-Institut für Umwelt-, Sicherheit- und Energietechnik UMSICHT und sechs Industriepartnern ein Modul zur direkten Laser-Mikrostrukturierung in einem Rolle-zu-Rolle-Verfahren. Ziel ist es, mit Hilfe dieses Systems eine siebartige Metallfolie als Demonstrator zu fertigen, die zum Sonnenschutz von Glasfassaden verwendet wird: Durch ihre besondere Geometrie wird die Sonneneinstrahlung reduziert, woraus sich ein verminderter Energieaufwand für Kühlung und Belüftung ergibt.

Das Fraunhofer IPT ist im Projekt »PoLaRoll« für die Prozessentwicklung der Laserstrukturierung sowie für die Mess- und Systemtechnik zuständig. Von den...

Im Focus: Das Auto lernt vorauszudenken

Ein neues Christian Doppler Labor an der TU Wien beschäftigt sich mit der Regelung und Überwachung von Antriebssystemen – mit Unterstützung des Wissenschaftsministeriums und von AVL List.

Wer ein Auto fährt, trifft ständig Entscheidungen: Man gibt Gas, bremst und dreht am Lenkrad. Doch zusätzlich muss auch das Fahrzeug selbst ununterbrochen...

Im Focus: Vorbild Delfinhaut: Elastisches Material vermindert Reibungswiderstand bei Schiffen

Für eine elegante und ökonomische Fortbewegung im Wasser geben Delfine den Wissenschaftlern ein exzellentes Vorbild. Die flinken Säuger erzielen erstaunliche Schwimmleistungen, deren Ursachen einerseits in der Körperform und andererseits in den elastischen Eigenschaften ihrer Haut zu finden sind. Letzteres Phänomen ist bereits seit Mitte des vorigen Jahrhunderts bekannt, konnte aber bislang nicht erfolgreich auf technische Anwendungen übertragen werden. Experten des Fraunhofer IFAM und der HSVA GmbH haben nun gemeinsam mit zwei weiteren Forschungspartnern eine Oberflächenbeschichtung entwickelt, die ähnlich wie die Delfinhaut den Strömungswiderstand im Wasser messbar verringert.

Delfine haben eine glatte Haut mit einer darunter liegenden dicken, nachgiebigen Speckschicht. Diese speziellen Hauteigenschaften führen zu einer signifikanten...

Im Focus: Kaltes Wasser: Und es bewegt sich doch!

Bei minus 150 Grad Celsius flüssiges Wasser beobachten, das beherrschen Chemiker der Universität Innsbruck. Nun haben sie gemeinsam mit Forschern in Schweden und Deutschland experimentell nachgewiesen, dass zwei unterschiedliche Formen von Wasser existieren, die sich in Struktur und Dichte stark unterscheiden.

Die Wissenschaft sucht seit langem nach dem Grund, warum ausgerechnet Wasser das Molekül des Lebens ist. Mit ausgefeilten Techniken gelingt es Forschern am...

Im Focus: Hyperspektrale Bildgebung zur 100%-Inspektion von Oberflächen und Schichten

„Mehr sehen, als das Auge erlaubt“, das ist ein Anspruch, dem die Hyperspektrale Bildgebung (HSI) gerecht wird. Die neue Kameratechnologie ermöglicht, Licht nicht nur ortsaufgelöst, sondern simultan auch spektral aufgelöst aufzuzeichnen. Das bedeutet, dass zur Informationsgewinnung nicht nur herkömmlich drei spektrale Bänder (RGB), sondern bis zu eintausend genutzt werden.

Das Fraunhofer IWS Dresden entwickelt eine integrierte HSI-Lösung, die das Potenzial der HSI-Technologie in zuverlässige Hard- und Software überführt und für...

Alle Focus-News des Innovations-reports >>>

Anzeige

Anzeige

IHR
JOB & KARRIERE
SERVICE
im innovations-report
in Kooperation mit academics
Veranstaltungen

Willkommen an Bord!

28.06.2017 | Veranstaltungen

Internationale Fachkonferenz IEEE ICDCM - Lokale Gleichstromnetze bereichern die Energieversorgung

27.06.2017 | Veranstaltungen

Internationale Konferenz zu aktuellen Fragen der Stammzellforschung

27.06.2017 | Veranstaltungen

 
VideoLinks
B2B-VideoLinks
Weitere VideoLinks >>>
Aktuelle Beiträge

Willkommen an Bord!

28.06.2017 | Veranstaltungsnachrichten

Fraunhofer-Forscher entwickeln Hochdrucksensoren für Extremtemperaturen

28.06.2017 | Energie und Elektrotechnik

Zeolith-Katalysatoren ebnen den Weg für dezentrale chemische Prozesse: Biosprit aus Abfällen

28.06.2017 | Verfahrenstechnologie