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 Volle Konzentration am Steuer
25.11.2016 | Leibniz-Institut für Arbeitsforschung an der TU Dortmund

nachricht Warum Reibung von der Zahl der Schichten abhängt
24.11.2016 | Karlsruher Institut für Technologie

Alle Nachrichten aus der Kategorie: Informationstechnologie >>>

Die aktuellsten Pressemeldungen zum Suchbegriff Innovation >>>

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

Im Focus: Gravitationswellen als Sensor für Dunkle Materie

Die mit der Entdeckung von Gravitationswellen entstandene neue Disziplin der Gravitationswellen-Astronomie bekommt eine weitere Aufgabe: die Suche nach Dunkler Materie. Diese könnte aus einem Bose-Einstein-Kondensat sehr leichter Teilchen bestehen. Wie Rechnungen zeigen, würden Gravitationswellen gebremst, wenn sie durch derartige Dunkle Materie laufen. Dies führt zu einer Verspätung von Gravitationswellen relativ zu Licht, die bereits mit den heutigen Detektoren messbar sein sollte.

Im Universum muss es gut fünfmal mehr unsichtbare als sichtbare Materie geben. Woraus diese Dunkle Materie besteht, ist immer noch unbekannt. Die...

Im Focus: Significantly more productivity in USP lasers

In recent years, lasers with ultrashort pulses (USP) down to the femtosecond range have become established on an industrial scale. They could advance some applications with the much-lauded “cold ablation” – if that meant they would then achieve more throughput. A new generation of process engineering that will address this issue in particular will be discussed at the “4th UKP Workshop – Ultrafast Laser Technology” in April 2017.

Even back in the 1990s, scientists were comparing materials processing with nanosecond, picosecond and femtosesecond pulses. The result was surprising:...

Im Focus: Wie sich Zellen gegen Salmonellen verteidigen

Bioinformatiker der Goethe-Universität haben das erste mathematische Modell für einen zentralen Verteidigungsmechanismus der Zelle gegen das Bakterium Salmonella entwickelt. Sie können ihren experimentell arbeitenden Kollegen damit wertvolle Anregungen zur Aufklärung der beteiligten Signalwege geben.

Jedes Jahr sind Salmonellen weltweit für Millionen von Infektionen und tausende Todesfälle verantwortlich. Die Körperzellen können sich aber gegen die...

Im Focus: Shape matters when light meets atom

Mapping the interaction of a single atom with a single photon may inform design of quantum devices

Have you ever wondered how you see the world? Vision is about photons of light, which are packets of energy, interacting with the atoms or molecules in what...

Im Focus: Greifswalder Forscher dringen mit superauflösendem Mikroskop in zellulären Mikrokosmos ein

Das Institut für Anatomie und Zellbiologie weiht am Montag, 05.12.2016, mit einem wissenschaftlichen Symposium das erste Superresolution-Mikroskop in Greifswald ein. Das Forschungsmikroskop wurde von der Deutschen Forschungsgemeinschaft (DFG) und dem Land Mecklenburg-Vorpommern finanziert. Nun können die Greifswalder Wissenschaftler Strukturen bis zu einer Größe von einigen Millionstel Millimetern mittels Laserlicht sichtbar machen.

Weit über hundert Jahre lang galt die von Ernst Abbe 1873 publizierte Theorie zur Auflösungsgrenze von Lichtmikroskopen als ein in Stein gemeißeltes Gesetz....

Alle Focus-News des Innovations-reports >>>

Anzeige

Anzeige

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

Wie aus reinen Daten ein verständliches Bild entsteht

05.12.2016 | Veranstaltungen

Von „Coopetition“ bis „Digitale Union“ – Die Fertigungsindustrien im digitalen Wandel

02.12.2016 | Veranstaltungen

Experten diskutieren Perspektiven schrumpfender Regionen

01.12.2016 | Veranstaltungen

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

Weiterbildung zu statistischen Methoden in der Versuchsplanung und -auswertung

06.12.2016 | Seminare Workshops

Bund fördert Entwicklung sicherer Schnellladetechnik für Hochleistungsbatterien mit 2,5 Millionen

06.12.2016 | Förderungen Preise

Innovationen für eine nachhaltige Forstwirtschaft

06.12.2016 | Agrar- Forstwissenschaften