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 Diagnose per Computer: Gefährliche Krankheitserreger mithilfe maschinellen Lernens erkennen
23.05.2018 | Helmholtz-Zentrum für Infektionsforschung

nachricht Frühwarnsystem RAWIS in Katastrophenübung mit THW final getestet
23.05.2018 | Fraunhofer-Institut für Hochfrequenzphysik und Radartechnik FHR

Alle Nachrichten aus der Kategorie: Informationstechnologie >>>

Die aktuellsten Pressemeldungen zum Suchbegriff Innovation >>>

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

Im Focus: Mit Hilfe molekularer Schalter lassen sich künftig neuartige Bauelemente entwickeln

Einem Forscherteam unter Führung von Physikern der Technischen Universität München (TUM) ist es gelungen, spezielle Moleküle mit einer angelegten Spannung zwischen zwei strukturell unterschiedlichen Zuständen hin und her zu schalten. Derartige Nano-Schalter könnten Basis für neuartige Bauelemente sein, die auf Silizium basierende Komponenten durch organische Moleküle ersetzen.

Die Entwicklung neuer elektronischer Technologien fordert eine ständige Verkleinerung funktioneller Komponenten. Physikern der TU München ist es im Rahmen...

Im Focus: Molecular switch will facilitate the development of pioneering electro-optical devices

A research team led by physicists at the Technical University of Munich (TUM) has developed molecular nanoswitches that can be toggled between two structurally different states using an applied voltage. They can serve as the basis for a pioneering class of devices that could replace silicon-based components with organic molecules.

The development of new electronic technologies drives the incessant reduction of functional component sizes. In the context of an international collaborative...

Im Focus: GRACE Follow-On erfolgreich gestartet: Das Satelliten-Tandem dokumentiert den globalen Wandel

Die Satellitenmission GRACE-FO ist gestartet. Am 22. Mai um 21.47 Uhr (MESZ) hoben die beiden Satelliten des GFZ und der NASA an Bord einer Falcon-9-Rakete von der Vandenberg Air Force Base (Kalifornien) ab und wurden in eine polare Umlaufbahn gebracht. Dort nehmen sie in den kommenden Monaten ihre endgültige Position ein. Die NASA meldete 30 Minuten später, dass der Kontakt zu den Satelliten in ihrem Zielorbit erfolgreich hergestellt wurde. GRACE Follow-On wird das Erdschwerefeld und dessen räumliche und zeitliche Variationen sehr genau vermessen. Sie ermöglicht damit präzise Aussagen zum globalen Wandel, insbesondere zu Änderungen im Wasserhaushalt, etwa dem Verlust von Eismassen.

Potsdam, 22. Mai 2018: Die deutsch-amerikanische Satellitenmission GRACE-FO (Gravity Recovery And Climate Experiment Follow On) ist erfolgreich gestartet. Am...

Im Focus: Faserlaser mit einstellbarer Wellenlänge

Faserlaser sind ein effizientes und robustes Werkzeug zum Schweißen und Schneiden von Metallen beispielsweise in der Automobilindustrie. Systeme bei denen die Wellenlänge des Laserlichts flexibel einstellbar ist, sind für spektroskopische Anwendungen und die Medizintechnik interessant. Wissenschaftlerinnen und Wissenschaftler des Leibniz-Instituts für Photonische Technologien (Leibniz-IPHT) haben, im Rahmen des vom Bundesministerium für Bildung und Forschung (BMBF) geförderten Projekts „FlexTune“, ein neues Abstimmkonzept realisiert, das erstmals verschiedene Emissionswellenlängen voneinander unabhängig und zeitlich synchron erzeugt.

Faserlaser bieten im Vergleich zu herkömmlichen Lasern eine höhere Strahlqualität und Energieeffizienz. Integriert in einen vollständig faserbasierten...

Im Focus: LZH zeigt Lasermaterialbearbeitung von morgen auf der LASYS 2018

Auf der LASYS 2018 zeigt das Laser Zentrum Hannover e.V. (LZH) vom 5. bis zum 7. Juni Prozesse für die Lasermaterialbearbeitung von morgen in Halle 4 an Stand 4E75. Mit gesprengten Bombenhüllen präsentiert das LZH in Stuttgart zudem erste Ergebnisse aus einem Forschungsprojekt zur zivilen Sicherheit.

Auf der diesjährigen LASYS stellt das LZH lichtbasierte Prozesse wie Schneiden, Schweißen, Abtragen und Strukturieren sowie die additive Fertigung für Metalle,...

Alle Focus-News des Innovations-reports >>>

Anzeige

Anzeige

VideoLinks
Industrie & Wirtschaft
Veranstaltungen

Größter Astronomie-Kongress kommt nach Wien

24.05.2018 | Veranstaltungen

22. Business Forum Qualität: Vom Smart Device bis zum Digital Twin

22.05.2018 | Veranstaltungen

48V im Fokus!

21.05.2018 | Veranstaltungen

VideoLinks
Wissenschaft & Forschung
Weitere VideoLinks im Überblick >>>
 
Aktuelle Beiträge

Das große Aufräumen nach dem Stress

25.05.2018 | Biowissenschaften Chemie

APEX wirft einen Blick ins Herz der Finsternis

25.05.2018 | Physik Astronomie

Weltneuheit im Live-Chat erleben

25.05.2018 | Messenachrichten

Weitere B2B-VideoLinks
IHR
JOB & KARRIERE
SERVICE
im innovations-report
in Kooperation mit academics