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 Smart Living: VDE-Institut entwickelt Cloud-basierte interoperable Testplattform
15.02.2017 | VDE Verband der Elektrotechnik Elektronik Informationstechnik e.V.

nachricht Saarbrücker Informatiker machen „Augmented Reality“ fotorealistisch
15.02.2017 | Universität des Saarlandes

Alle Nachrichten aus der Kategorie: Informationstechnologie >>>

Die aktuellsten Pressemeldungen zum Suchbegriff Innovation >>>

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

Im Focus: Innovative Antikörper für die Tumortherapie

Immuntherapie mit Antikörpern stellt heute für viele Krebspatienten einen Erfolg versprechenden Ansatz dar. Weil aber längst nicht alle Patienten nachhaltig von diesen teuren Medikamenten profitieren, wird intensiv an deren Verbesserung gearbeitet. Forschern um Prof. Thomas Valerius an der Christian Albrechts Universität Kiel gelang es nun, innovative Antikörper mit verbesserter Wirkung zu entwickeln.

Immuntherapie mit Antikörpern stellt heute für viele Krebspatienten einen Erfolg versprechenden Ansatz dar. Weil aber längst nicht alle Patienten nachhaltig...

Im Focus: Durchbruch mit einer Kette aus Goldatomen

Einem internationalen Physikerteam mit Konstanzer Beteiligung gelang im Bereich der Nanophysik ein entscheidender Durchbruch zum besseren Verständnis des Wärmetransportes

Einem internationalen Physikerteam mit Konstanzer Beteiligung gelang im Bereich der Nanophysik ein entscheidender Durchbruch zum besseren Verständnis des...

Im Focus: Breakthrough with a chain of gold atoms

In the field of nanoscience, an international team of physicists with participants from Konstanz has achieved a breakthrough in understanding heat transport

In the field of nanoscience, an international team of physicists with participants from Konstanz has achieved a breakthrough in understanding heat transport

Im Focus: Hoch wirksamer Malaria-Impfstoff erfolgreich getestet

Tübinger Wissenschaftler erreichen Impfschutz von bis zu 100 Prozent – Lebendimpfstoff unter kontrollierten Bedingungen eingesetzt

Tübinger Wissenschaftler erreichen Impfschutz von bis zu 100 Prozent – Lebendimpfstoff unter kontrollierten Bedingungen eingesetzt

Im Focus: Sensoren mit Adlerblick

Stuttgarter Forscher stellen extrem leistungsfähiges Linsensystem her

Adleraugen sind extrem scharf und sehen sowohl nach vorne, als auch zur Seite gut – Eigenschaften, die man auch beim autonomen Fahren gerne hätte. Physiker der...

Alle Focus-News des Innovations-reports >>>

Anzeige

Anzeige

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

Die Welt der keramischen Werkstoffe - 4. März 2017

20.02.2017 | Veranstaltungen

Schwerstverletzungen verstehen und heilen

20.02.2017 | Veranstaltungen

ANIM in Wien mit 1.330 Teilnehmern gestartet

17.02.2017 | Veranstaltungen

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

Innovative Antikörper für die Tumortherapie

20.02.2017 | Medizin Gesundheit

Multikristalline Siliciumsolarzelle mit 21,9 % Wirkungsgrad – Weltrekord zurück am Fraunhofer ISE

20.02.2017 | Energie und Elektrotechnik

Wie Viren ihren Lebenszyklus mit begrenzten Mitteln effektiv sicherstellen

20.02.2017 | Biowissenschaften Chemie