Hightech

HIGHTECH

14.12.2018 - 12:30 | pressetext.redaktion
14.12.2018 - 11:15 | TIMETOACT Software & Consulting GmbH
14.12.2018 - 06:15 | pressetext.redaktion

BUSINESS

14.12.2018 - 14:45 | Vogel Communications Group GmbH & Co. KG
14.12.2018 - 14:02 | pressetext.redaktion
14.12.2018 - 13:40 | VBV-Gruppe

MEDIEN

14.12.2018 - 11:30 | pressetext.redaktion
14.12.2018 - 06:05 | pressetext.redaktion
13.12.2018 - 13:31 | pressetext.redaktion

LEBEN

14.12.2018 - 11:45 | Zentrum für Vitalität und Hormon-Power®
14.12.2018 - 10:30 | pressetext.redaktion
14.12.2018 - 09:00 | JADEO Germany GmbH
pte20090817022 Computer/Telekommunikation, Forschung/Technologie

Sicherheits-Beweis für Betriebssystem-Kernel

Forscher melden mathematischen Nachweis für fehlerfreien Code


Quellcode: In Zukunft stets streng geprüft? (Foto: pixelio.de, Virgil)
Quellcode: In Zukunft stets streng geprüft? (Foto: pixelio.de, Virgil)

Eveleigh/Chicago (pte022/17.08.2009/11:50) - Forscher am australischen IKT-Forschungsinstitut NICTA http://nicta.com.au 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 http://www.ok-labs.com , 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.

(Ende)
Aussender: pressetext.austria
Ansprechpartner: Thomas Pichler
Tel.: +43-1-81140-303
E-Mail: pichler@pressetext.com
Website:
|
|
98.204 Abonnenten
|
168.070 Meldungen
|
66.612 Pressefotos

IR-NEWS

15.12.2018 - 10:22 | NABAG Anlage- und Beteiligungs-AG
14.12.2018 - 15:15 | DEWB
14.12.2018 - 10:30 | BAWAG Group AG
Top